Proof of `'Exact fixed-round grid-minor theorem'`

groundedproofs/Lax17Proofs/Final.lean · lax-17

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

The exact fixed-parameter theorem. For every integer t2t \geq 2, the factor ρ\rho is explicitly characterized as the least natural number whose tt-th power dominates g2g^2.