∑ Math Proof Playground › WOWII › 143

WOWII Graph Conjecture 143

A complete modular Lean 4 proof of the exact current theorem.

six-module sorry-free proofproof bundle archived in CRLupstream PR #4442

Theorem

girth(G) + 1 ≤ largestInducedTreeSize(G) · secondSmallestDegree(G)

Proof decomposition

  1. Acyclic case.
  2. Cyclic case with second-smallest degree at least two.
  3. Exceptional second-smallest-degree-one case via two leaves, a maximum induced tree, and an external chord attachment.

Lean modules

CRL proof archive.