Lax Lean Archive

'Exact fixed-round grid-minor theorem'

Lax17.FixedRoundGridMinor · concepts/Lax17/FixedRoundGridMinor.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

    For every integer t≥2t \geq 2, let ρt(g)\rho_t(g) be the least natural number such that g2≤ρt(g)tg^2 \leq \rho_t(g)^t. There are positive integers KtK_t and btb_t, depending only on tt, such that treewidth at least Ktg8ρt(g)(log⁡2g)btK_t g^8 \rho_t(g)(\log_2 g)^{b_t} forces a g×gg \times g grid minor.

    This division-free natural-number theorem is the fixed-round combinatorial core used by the exponent-8+ε8+\varepsilon endpoint.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Log
    2import Lax17.GridMinor
    3import Lax17.PowerRoot
    4import Lax17.Treewidth
    5
    6/-!
    7---
    8title: 'Exact fixed-round grid-minor theorem'
    9type: theorem
    10---
    11For every integer t≥2t \geq 2, let ρt(g)\rho_t(g) be the least natural number
    12such that g2≤ρt(g)tg^2 \leq \rho_t(g)^t. There are positive integers KtK_t and
    13btb_t, depending only on tt, such that treewidth at least
    14Ktg8ρt(g)(log⁡2g)btK_t g^8 \rho_t(g)(\log_2 g)^{b_t} forces a g×gg \times g grid minor.
    15
    16This division-free natural-number theorem is the fixed-round combinatorial
    17core used by the exponent-8+ε8+\varepsilon endpoint.
    18-/
    19
    20namespace Lax17.FixedRoundGridMinor
    21
    22universe u
    23
    24/-- Exact natural-number theorem obtained from t−1t-1 recursive slicing
    25rounds. The transparent root relation determines the factor `rho`. -/
    26axiom polynomial_grid_minor_fixed_t :
    27 ∀ t : ℕ, 2 ≤ t →
    28 ∃ K b : ℕ, 0 < K ∧ 0 < b ∧
    29 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    30 (G : SimpleGraph V) {g rho : ℕ},
    31 2 ≤ g →
    32 Lax17.PowerRoot.IsCeilingPowerRoot t g rho →
    33 K * g ^ 8 * rho * (Nat.log 2 g) ^ b ≤
    34 Lax17.Treewidth.treewidth G →
    35 Lax17.GridMinor.ContainsGridMinor G g
    36
    37end Lax17.FixedRoundGridMinor
    38
    Show 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…