Lax Lean Archive

Proof of `'Polynomial grid-minor theorem with exponent 88 up to polylogarithmic factors'` (1st statement)

groundedproofs/Lax17Proofs/Final.lean · lax-17

What this proof establishes

thm✓Lax17.PolynomialGridMinor (1st statement)

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

For every positive real ε\varepsilon, a constant depending only on ε\varepsilon makes treewidth Cg8+εC g^{8+\varepsilon} sufficient for a g×gg \times g grid minor.