Proof of `A graph or its complement has diameter at most 3`

groundedproofs/Lax185574Proofs/ComplementDiameter.lean · lax-185574

What this proof establishes

no assumptions

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

In the paper

  • page 32 of this submission's paper

Description

If some two vertices uu, vv are not joined by a walk of length at most 22 in GG, then they are distinct, non-adjacent and have no common neighbor. In Ḡ they are adjacent, and every other vertex is adjacent to uu or to vv. So any two vertices are joined in Ḡ by a walk that goes to uu or vv, possibly crosses the edge uvuv, and leaves again, of length at most 33.