Edge Expansion Forces Linear Treewidth

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

proven

Loading review…

Sign in with ORCID

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

    For a positive integer dd, every finite subcubic graph with edge expansion at least 1/(8d)1/(8d) satisfies ∣V∣≤(24d+1)(tw⁡(G)+1)|V|\le(24d+1)(\operatorname{tw}(G)+1).

    If every component after deleting XX has size at most ∣V∣/2|V|/2, summing the expansion inequalities over components gives ∣V∖X∣≤24d∣X∣|V\setminus X|\le24d|X|. Thus a smaller deletion leaves a component containing more than half the graph. These large connected sets form a bramble. A bag of every tree decomposition hits the bramble, giving the bound.

    Concept map
    3 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.EdgeExpansion
    2import Lax228581.Treewidth
    3
    4/-!
    5---
    6title: Edge Expansion Forces Linear Treewidth
    7type: lemma
    8---
    9For a positive integer dd, every finite subcubic graph with edge expansion
    10at least 1/(8d)1/(8d) satisfies
    11∣V∣≤(24d+1)(tw⁡(G)+1)|V|\le(24d+1)(\operatorname{tw}(G)+1).
    12
    13If every component after deleting XX has size at most ∣V∣/2|V|/2, summing the
    14expansion inequalities over components gives
    15∣V∖X∣≤24d∣X∣|V\setminus X|\le24d|X|. Thus a smaller deletion leaves a component
    16containing more than half the graph. These large connected sets form a
    17bramble. A bag of every tree decomposition hits the bramble, giving the bound.
    18
    19# Formalization notes
    20
    21Treewidth is the registered definition from `Lax228581.Treewidth`.
    22The additive one is necessary for graphs of treewidth zero. Empty graphs
    23are included. Natural-number multiplication avoids rounding conventions.
    24-/
    25
    26namespace Lax920634.ExpansionTreewidth
    27
    28open EdgeExpansion Lax228581.Treewidth
    29
    30/-- Uniform expansion in a subcubic graph gives a linear lower bound on treewidth. -/
    31axiom order_le_treewidth {n : ℕ} (G : SimpleGraph (Fin n)) (d : ℕ) (hd : 0 < d)
    32 (hdegree : IsSubcubic G)
    33 (hex : HasEdgeExpansionAtLeast G (1 / (8 * (d : ℚ)))) :
    34 n ≤ (24 * d + 1) * (treewidth G + 1)
    35
    36end Lax920634.ExpansionTreewidth
    37
    Show Proof
    Formalization notes

    Treewidth is the registered definition from Lax228581.TreewidthLax228581.Treewidth. The additive one is necessary for graphs of treewidth zero. Empty graphs are included. Natural-number multiplication avoids rounding conventions.

    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…