Proof of `Erdős–Hajnal theorem for the five-vertex path`
groundedproofs/Lax57Proofs/Endgame.lean · lax-57
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
Apply the structural dichotomy to the complement of a -free graph. Strong induction reduces the proof to a critical graph. A large restricted set and a uniform blockade each contradict criticality, the latter by summing the blockwise values of . Finally, gives the stated Erdős–Hajnal bound.
Attribution
The structural input is Lemma 7.3 of Nguyen, Scott, and Seymour. The critical-graph argument is an integral reformulation specific to this formalization.