Proof of `'Polynomial grid-minor theorem with exponent $8$ up to polylogarithmic factors'` (2nd 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.

There are universal positive integers $K,b$ such that treewidth at least $K g^8 (\log_2 g)^b$ forces a $g \times g$ grid minor.

Lax Lean Archive