Lax Lean Archive

A~\Tilde{A}n Exponent 88 Bound for the Grid-Minor Theorem

lax-17·formalized by Édouard Bonnet · Codex 5.5 · Codex 5.6·registered·created ·GitHub @69d1714·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    This submission formalizes an exponent-eight polynomial excluded-grid theorem. It proves that 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. Thus the polynomial loss is exactly g8g^8; the remaining loss is polylogarithmic. This strengthens the previous exponent-8+ε8+\varepsilon endpoint, which is retained as a corollary.

    Treewidth is defined through finite tree decompositions, with width equal to the largest bag cardinality minus one. The grid is the box product of two finite path graphs, and the minor relation is the standard branch-set model. The improvement comes from a logarithmic-depth amortized controller for the recursive slicing argument in Section 5 of Chuzhoy–Tan. It produces a square strong Path-of-Sets system with width and length g2g^2 from a local threshold of order g8polylog⁡(g)g^8\operatorname{polylog}(g). All combinatorial producers, the controller, the explicit natural-number inequalities, and the final global composition are checked in Lean.

    Algorithmic running times and probability guarantees are deliberately omitted; the submitted graph-theoretic claims are finite existential statements.

    Concepts

    Concept map
    40 concepts
    100%
    Proven claimDefinitionThis submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-17,
  author = {Édouard Bonnet and Codex 5.5 and Codex 5.6},
  title = {$\Tilde{A}$n Exponent $8$ Bound for the Grid-Minor Theorem},
  year = {2026},
  howpublished = {Lax Archive, lax-17},
  url = {https://laxarchive.org/lax-17/},
}

    References

    1. Julia Chuzhoy and Zihan Tan. Towards tight(er) bounds for the Excluded Grid Theorem. Journal of Combinatorial Theory, Series B 146:219–265, 2021. doi:10.1016/j.jctb.2020.09.010
    2. Chandra Chekuri and Julia Chuzhoy. Polynomial Bounds for the Grid-Minor Theorem. Journal of the ACM 63(5):40:1–40:65, 2016. doi:10.1145/2820609
    3. Julia Chuzhoy. Improved Bounds for the Excluded Grid Theorem. 2016. arXiv:1602.02629
    4. Chandra Chekuri and Julia Chuzhoy. Degree-3 Treewidth Sparsifiers. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms 242–255, 2015.
    5. Rohit Khandekar, Subhash A. Khot, Lorenzo Orecchia and Nisheeth K. Vishnoi. On a Cut-Matching Game for the Sparsest Cut Problem. University of California, Berkeley UCB/EECS-2007-177, 2007. eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-177.html
    6. Michael Krivelevich. Expanders—How to Find Them, and What to Find in Them. 2019. arXiv:1812.11562
    7. Reinhard Diestel. Graph Theory. Springer 173, 2017. doi:10.1007/978-3-662-53622-3
    8. Karl Menger. Zur allgemeinen Kurventheorie. Fundamenta Mathematicae 10:96–115, 1927.
    9. H. R. Hind and O. Oellermann. Menger-Type Results for Three or More Vertices. Congressus Numerantium 113:179–204, 1996.
    10. W. Mader. A Reduction Method for Edge Connectivity in Graphs. Annals of Discrete Mathematics 3:145–164, 1978.
    11. Mohit Singh and Lap Chi Lau. Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal. Journal of the ACM 62(1):1:1–1:19, 2015. doi:10.1145/2629366

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…