Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Controlled-size subcubic source graphs of linear treewidth

Lax263307.SourceGraphs · concepts/Lax263307/SourceGraphs.lean · lax-263307

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

    The registered deterministic subcubic family supplies fixed positive constants for width and size overshoot. For every requested order, choose a source graph above the request and below a fixed multiple of the request plus one, with order bounded by the width constant times treewidth plus one. The upper size bound is needed to meet the route-sampling budgets.

    Concept map
    10 concepts; 9 descendants hidden
    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.ConstructionSize
    2import Lax920634.SubcubicConstruction
    3import Lax920634.ExplicitTreewidth
    4
    5/-!
    6---
    7title: Controlled-size subcubic source graphs of linear treewidth
    8type: theorem
    9---
    10The registered deterministic subcubic family supplies fixed positive
    11constants for width and size overshoot. For every requested order, choose a
    12source graph above the request and below a fixed multiple of the request
    13plus one, with order bounded by the width constant times treewidth plus one.
    14The upper size bound is needed to meet the route-sampling budgets.
    15
    16# Attribution
    17
    18Lax920634's registered subcubic construction, size bound, and explicit
    19linear-treewidth theorem; the source family used in Bonnet–Chang, Lemma 10.
    20-/
    21
    22namespace Lax263307.SourceGraphs
    23
    24open Lax920634.ZigZagConstruction Lax920634.GraphEncoding Lax920634.SeedSearch
    25open Lax920634.EdgeExpansion Lax228581.Treewidth
    26
    27axiom controlled_family : ∃ widthConstant sizeConstant : ℕ,
    28 0 < widthConstant ∧ 0 < sizeConstant ∧
    29 ∀ request : ℕ, ∃ n, ∃ H : SimpleGraph (Fin n), request ≤ n ∧
    30 n ≤ sizeConstant * (request + 1) ∧ IsSubcubic H ∧
    31 n ≤ widthConstant * (treewidth H + 1)
    32
    33end Lax263307.SourceGraphs
    34
    Show Proof

    Attribution

    Lax920634's registered subcubic construction, size bound, and explicit linear-treewidth theorem; the source family used in Bonnet–Chang, Lemma 10.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…