Lax Lean Archive

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

Proof of `Exponent 8 (×\times Polylogarithmic) Bound for the Grid-Minor Theorem`

groundedproofs/Lax17Proofs/Final.lean · lax-17

What this proof establishes

thm✓Lax17.PolynomialGridMinor

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

There are positive integers KK and bb such that every finite simple graph of treewidth at least

Kg8(log⁡2g)bK g^8 (\log_2 g)^b

contains the g×gg \times g square grid as a minor.