Lax Lean Archive

The Explicit Family Has Linear Treewidth

Lax920634.ExplicitTreewidth · concepts/Lax920634/ExplicitTreewidth.lean · lax-920634

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

    Lemma

    The specified graphs satisfy Nk≤(24d+1)(tw⁡(Hk)+1)N_k\le(24d+1)(\operatorname{tw}(H_k)+1), where d=D2d=D^2 is the fixed regular tower degree. Hence sufficiently large members have treewidth at least Nk/(48d+2)N_k/(48d+2).

    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 Lax920634.ZigZagConstruction
    2import Lax228581.Treewidth
    3
    4/-!
    5---
    6title: The Explicit Family Has Linear Treewidth
    7type: lemma
    8---
    9The specified graphs satisfy
    10Nk≤(24d+1)(tw⁡(Hk)+1)N_k\le(24d+1)(\operatorname{tw}(H_k)+1), where d=D2d=D^2 is the fixed
    11regular tower degree. Hence sufficiently large members have treewidth at
    12least Nk/(48d+2)N_k/(48d+2).
    13
    14# Formalization notes
    15
    16The expansion and treewidth claims refer to the same computable graph.
    17The existence theorem below absorbs the additive one by choosing a large
    18enough size request.
    19-/
    20
    21namespace Lax920634.ExplicitTreewidth
    22
    23open ZigZagConstruction Lax228581.Treewidth
    24
    25/-- The specified graph order is bounded linearly by treewidth plus one. -/
    26axiom linear_treewidth (k : ℕ) : order k ≤
    27 (24 * degree + 1) *
    28 (treewidth (graph k) + 1)
    29
    30end Lax920634.ExplicitTreewidth
    31
    Show Proof
    Formalization notes

    The expansion and treewidth claims refer to the same computable graph. The existence theorem below absorbs the additive one by choosing a large enough size request.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…