Proof of `The unoptimized empty-hexagon bound`
groundedproofs/Lax570090Proofs/EmptyHexagon.lean · lax-570090
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The unoptimized Valtr argument, using the four-layer theorem interface so Lax records its dependency on the proof in . The minimum-polygon argument, consecutive-layer inequality, Erdős–Szekeres bound, shear, and cyclic-order bridge are all proved; no SAT solver or native decision axiom is used.