Lax Lean Archive

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

Edge-sublinear separators imply edge-sublinear decomposition bags

Lax263307.EdgeBagBounds · concepts/Lax263307/EdgeBagBounds.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

    In a hereditary graph class, recursively balanced separators build tree decompositions with a logarithmic factor. Removing isolated vertices first bounds the remaining order by twice the edge count. Absorb the logarithm into a positive fraction of the gap between the separator exponent and one. The resulting bag bound remains strongly sublinear in the edge count.

    An integer exponent then expresses this as ∣B∣a≤A(m+1)a−1|B|^a\le A(m+1)^{a-1}, which is precisely the class premise used by the routing contradiction.

    Concept map
    39 concepts; 8 descendants hidden
    100%
    TreewidthTreewidth transfer through analmost-embeddingConditioning graph routes on uniformendpointsBags meeting a connected vertex setTree-decomposition transfer throughconnected vertex representationsCoupled route sampling with shared verteximagesA good coupled sample with bounded totalroute sizeEdge-sublinear separators implyedge-sublinear decomposition bagsTreewidth loss under edge deletionStrongly edge-sublinear separatorsEntropy and adjacency massFinite product sampling and coordinatemarginalsHereditary graph classesRestricting an induced almost-embedding toits route unionA class width bound obstructs induced routesamplingFew edges in the graph induced by shortroutesAlmost-embedding transfer with isolatedsource verticesThe independent-set relaxation and its exacthullCollision and length bounds forindependently sampled pathsInteger power bounds on class decompositionbagsDepth and approximation loss of balancedrecursionGraph-route distributions from high-valuesplit flowsDiscarding long almost-embedding routesUniform endpoint normalization of finitepath flowsAn induced almost-embedding from a goodroute sampleChoosing a collision-free outcome withbounded total path lengthThe components left by deleting a separatorTree decompositions from recursive balancedseparatorsProjecting split paths and preservingendpoint loadsVertex splitting for the directed flow–cutalgorithmMaximum-weight independent set and itsencodingConcurrent fractional flowExact flow–cut output certificatesProduct multicommodity networks andsparsest cutsDeterministic directed uniform flow–cutalgorithmRational flow instances and certificatesBinary encoding of finite wordsPolynomial-time computation by a wordRAMThe word RAM
    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 power_bag_bound proven

    2 sublinear_bag_bound proven

    Lean source view on GitHub

    1import Lax263307.SeparatorDecompositions
    2import Lax263307.PowerBagBounds
    3
    4/-!
    5---
    6title: Edge-sublinear separators imply edge-sublinear decomposition bags
    7type: theorem
    8---
    9In a hereditary graph class, recursively balanced separators build tree
    10decompositions with a logarithmic factor. Removing isolated vertices first
    11bounds the remaining order by twice the edge count. Absorb the logarithm
    12into a positive fraction of the gap between the separator exponent and one.
    13The resulting bag bound remains strongly sublinear in the edge count.
    14
    15An integer exponent then expresses this as ∣B∣a≤A(m+1)a−1|B|^a\le A(m+1)^{a-1},
    16which is precisely the class premise used by the routing contradiction.
    17
    18# Formalization notes
    19
    20This supplies the class power bound from the original separator hypothesis.
    21It imposes no additional condition on the class and uses singleton leaf
    22bags to restore arbitrarily many isolated vertices. Constants are existential
    23class constants, as in the main theorem.
    24-/
    25
    26namespace Lax263307.EdgeBagBounds
    27
    28open GraphClasses EdgeSublinearSeparators Lax228581.Treewidth
    29
    30axiom sublinear_bag_bound (C : GraphClass) (hereditary : IsHereditary C)
    31 (separators : HasStronglyEdgeSublinearSeparators C) :
    32 ∃ β c : ℝ, 0 ≤ β ∧ β < 1 ∧ 0 < c ∧ ∀ n (G : SimpleGraph (Fin n)), G ∈ C n →
    33 ∃ D : TreeDecomposition G, ∀ j,
    34 ((D.bag j).card : ℝ) ≤ c * Real.rpow ((G.edgeSet.ncard : ℝ) + 1) β
    35
    36axiom power_bag_bound (C : GraphClass) (hereditary : IsHereditary C)
    37 (separators : HasStronglyEdgeSublinearSeparators C) :
    38 ∃ a A : ℕ, 0 < a ∧ 0 < A ∧ PowerBagBounds.HasPowerBagBound C a A
    39
    40end Lax263307.EdgeBagBounds
    41
    Show ProofShow Proof
    Formalization notes

    This supplies the class power bound from the original separator hypothesis. It imposes no additional condition on the class and uses singleton leaf bags to restore arbitrarily many isolated vertices. Constants are existential class constants, as in the main theorem.

    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…