Draft — mutable and not usable as a dependency; its citation marks the draft state.

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.

Read the Lean proof on GitHub

Description

Apply the structural dichotomy to the complement of a P5P_5-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 κ\kappa. Finally, κ(G)max{α(G),ω(G)}2\kappa(G)\leq \max\{\alpha(G),\omega(G)\}^2 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.