Lax Lean Archive

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

Sublinear bag bounds survive independent blow-ups

Lax263307.BlowUpBagBounds · concepts/Lax263307/BlowUpBagBounds.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 independent blow-up closure of a hereditary class with strongly edge-sublinear separators also has edge-sublinear decomposition bags. Restrict the original host to vertices used by the projection. Choosing one representative in each fibre embeds this host into the blow-up, so its edge count cannot exceed that of the blow-up. Optimize degree deletion and bounded-fibre lifting, then convert the resulting real exponent to an integer power bound.

    Concept map
    45 concepts; 2 descendants hidden
    100%
    TreewidthTreewidth transfer through analmost-embeddingSublinear bag bounds survive independentblow-upsIndependent blow-up classes are hereditaryLifting a tree decomposition through abounded blow-upDeleting high-degree vertices in anindependent blow-upIndependent sets lift and project through ablow-upConditioning 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 unionIndependent blow-ups and projectionA 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 blowup_power_bag_bound proven

    2 blowup_sublinear_bag_bound proven

    Lean source view on GitHub

    1import Lax263307.EdgeBagBounds
    2import Lax263307.BlowUpClasses
    3import Lax263307.BlowUpDeletion
    4
    5/-!
    6---
    7title: Sublinear bag bounds survive independent blow-ups
    8type: theorem
    9---
    10The independent blow-up closure of a hereditary class with strongly
    11edge-sublinear separators also has edge-sublinear decomposition bags.
    12Restrict the original host to vertices used by the projection. Choosing
    13one representative in each fibre embeds this host into the blow-up, so
    14its edge count cannot exceed that of the blow-up. Optimize degree deletion
    15and bounded-fibre lifting, then convert the resulting real exponent to
    16an integer power bound.
    17
    18# Formalization notes
    19
    20Arbitrary projection fibres, including empty fibres, are allowed. Relabel
    21used host vertices and enumerate each fibre to identify the graph with an
    22explicit copy graph. The original host need not have at most as many edges
    23until its unused vertices are removed. These existential constructions
    24are structural analysis; the algorithm does not build decomposition bags.
    25
    26# Attribution
    27
    28Bonnet–Chang, Lemma 16.
    29-/
    30
    31namespace Lax263307.BlowUpBagBounds
    32
    33open GraphClasses EdgeSublinearSeparators BlowUpClasses Lax228581.Treewidth
    34
    35axiom blowup_sublinear_bag_bound (C : GraphClass) (hereditary : IsHereditary C)
    36 (separators : HasStronglyEdgeSublinearSeparators C) :
    37 ∃ β c : ℝ, 0 ≤ β ∧ β < 1 ∧ 0 < c ∧ ∀ m (H : SimpleGraph (Fin m)), H ∈ blowUpClass C m →
    38 ∃ D : TreeDecomposition H, ∀ j,
    39 ((D.bag j).card : ℝ) ≤ c * Real.rpow ((H.edgeSet.ncard : ℝ) + 1) β
    40
    41axiom blowup_power_bag_bound (C : GraphClass) (hereditary : IsHereditary C)
    42 (separators : HasStronglyEdgeSublinearSeparators C) :
    43 ∃ a A : ℕ, 0 < a ∧ 0 < A ∧ Lax263307.PowerBagBounds.HasPowerBagBound (blowUpClass C) a A
    44
    45end Lax263307.BlowUpBagBounds
    46
    Show ProofShow Proof
    Formalization notes

    Arbitrary projection fibres, including empty fibres, are allowed. Relabel used host vertices and enumerate each fibre to identify the graph with an explicit copy graph. The original host need not have at most as many edges until its unused vertices are removed. These existential constructions are structural analysis; the algorithm does not build decomposition bags.

    Attribution

    Bonnet–Chang, Lemma 16.

    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…