Lax Lean Archive

'Polynomial grid-minor theorem with exponent 88 up to polylogarithmic factors'

Lax17.PolynomialGridMinor · concepts/Lax17/PolynomialGridMinor.lean · lax-17

proven

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this concept

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

    No source line selected.

    Natural Language Statement

    Theorem

    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. In particular, the polynomial exponent is exactly eight; all remaining loss is polylogarithmic.

    The earlier exponent-8+ε8+\varepsilon formulation is retained below as a compatibility corollary.

    Treewidth is the parameter defined by the Lax17.TreewidthLax17.Treewidth concept. The minor conclusion uses the branch-set model in Lax17.GridMinorLax17.GridMinor.

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 polynomial_grid_minor_eight_add_epsilon proven

    2 polynomial_grid_minor_eight_polylog proven

    Lean source view on GitHub

    1import Mathlib.Analysis.SpecialFunctions.Log.Base
    2import Lax17.GridMinor
    3import Lax17.Treewidth
    4
    5/-!
    6---
    7title: 'Polynomial grid-minor theorem with exponent 88 up to polylogarithmic factors'
    8type: theorem
    9---
    10There are positive integers KK and bb such that every finite simple graph
    11of treewidth at least
    12
    13Kg8(log⁡2g)bK g^8 (\log_2 g)^b
    14
    15contains the g×gg\times g square grid as a minor. In particular, the
    16polynomial exponent is exactly eight; all remaining loss is polylogarithmic.
    17
    18The earlier exponent-8+ε8+\varepsilon formulation is retained below as a
    19compatibility corollary.
    20
    21Treewidth is the parameter defined by the `Lax17.Treewidth` concept. The
    22minor conclusion uses the branch-set model in `Lax17.GridMinor`.
    23-/
    24
    25namespace Lax17.PolynomialGridMinor
    26
    27universe u
    28
    29/-- Polynomial excluded-grid theorem with exact polynomial exponent eight
    30and an explicit natural-number polylogarithmic factor. The constants are
    31selected before the graph and grid order. -/
    32axiom polynomial_grid_minor_eight_polylog :
    33 ∃ K b : ℕ, 0 < K ∧ 0 < b ∧
    34 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    35 (G : SimpleGraph V) {g : ℕ},
    36 2 ≤ g →
    37 K * g ^ 8 * (Nat.log 2 g) ^ b ≤
    38 Lax17.Treewidth.treewidth G →
    39 Lax17.GridMinor.ContainsGridMinor G g
    40
    41/-- Polynomial excluded-grid theorem with exponent `8 + epsilon`.
    42
    43The exponent on `(g : ℝ)` is real exponentiation. The constant is selected
    44before the graph and grid order, so it depends only on `epsilon`. -/
    45axiom polynomial_grid_minor_eight_add_epsilon :
    46 ∀ epsilon : ℝ, 0 < epsilon →
    47 ∃ C : ℝ, 0 < C ∧
    48 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    49 (G : SimpleGraph V) {g : ℕ},
    50 2 ≤ g →
    51 C * (g : ℝ) ^ ((8 : ℝ) + epsilon) ≤
    52 (Lax17.Treewidth.treewidth G : ℝ) →
    53 Lax17.GridMinor.ContainsGridMinor G g
    54
    55end Lax17.PolynomialGridMinor
    56
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…