Lax Lean Archive

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

Balanced light separators from the registered flow-cut solver

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

    A hereditary class with strongly edge-sublinear separators has fixed positive integer constants a,K,B. A cost vector with coordinates in [0,1], total mass at most k, and edge cost at most k²/p admits a balanced separator of cost at most delta*k when k and p exceed the stated polynomial thresholds. The cut trace uses at most n calls and keeps its actual covering shores.

    Concept map
    56 concepts; 6 descendants hidden
    100%
    TreewidthTreewidth transfer through analmost-embeddingBalanced closed parts certify a balancedseparatorConditioning graph routes on uniformendpointsBags meeting a connected vertex setTree-decomposition transfer throughconnected vertex representationsA width obstruction from sparse costs andbounded route loadsCoupled route sampling with shared verteximagesA good coupled sample with bounded totalroute sizeRepeated cuts yield a balanced lightseparatorEdge-sublinear separators implyedge-sublinear decomposition bagsTreewidth loss under edge deletionStrongly edge-sublinear separatorsEntropy and adjacency massFinite product sampling and coordinatemarginalsThe split flow-cut certificate must give acheap separationHereditary 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 verticesBalanced light separators from the registeredflow-cut solverThe independent-set relaxation and its exacthullSparse bounded-load route distributions areimpossibleCollision and length bounds forindependently sampled pathsInteger power bounds on class decompositionbagsDepth and approximation loss of balancedrecursionCumulative separator cost over disjointdiscarded shoresGraph-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 balancedseparatorsControlled-size subcubic source graphs oflinear treewidthProjecting split paths and preservingendpoint loadsVertex splitting for the directed flow–cutalgorithmMaximum-weight independent set and itsencodingPolynomial order bound from the sampledwidth inequalityConcurrent 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 RAMThe Constructor Meets the Requested OrderEdge Expansion and Subcubic GraphsThe Explicit Family Has Linear TreewidthSelecting and Encoding the ConstructedGraphsRotation Map of the Fixed Powered SeedDeterministic Search for a Fixed ExpanderSeedThe Explicit Graphs Are SubcubicExplicit Zig-Zag Family and PathReplacement
    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 Lax263307.EdgeBagBounds
    2import Lax263307.ForcedSeparation
    3import Lax263307.CutTraces
    4
    5/-!
    6---
    7title: Balanced light separators from the registered flow-cut solver
    8type: theorem
    9---
    10A hereditary class with strongly edge-sublinear separators has fixed positive
    11integer constants a,K,B. A cost vector with coordinates in [0,1], total
    12mass at most k, and edge cost at most k²/p admits a balanced separator of
    13cost at most delta*k when k and p exceed the stated polynomial thresholds.
    14The cut trace uses at most n calls and keeps its actual covering shores.
    15
    16# Formalization notes
    17
    18The load parameter ell needs only a multiple of log n / delta. This theorem
    19instantiates the remainder oracle using the registered directed split solver:
    20restriction cannot increase costs, the larger remainder supplies the load
    21scale inequality, and a sufficiently large finite rational capacity excludes
    22expensive split arcs. Orienting the cut toward its smaller shore supplies
    23the exclusive-piece bound. The accumulated trace cost is at most delta*k.
    24Actual RAM construction and iteration costs remain separate obligations.
    25
    26# Attribution
    27
    28Bonnet–Chang, Lemmas 7–8 and 11.
    29-/
    30
    31namespace Lax263307.LightSeparators
    32
    33open scoped NNRat
    34open GraphClasses EdgeSublinearSeparators Entropy RepeatedCutAccounting
    35
    36axiom class_light_separator (C : GraphClass) (hereditary : IsHereditary C)
    37 (separators : HasStronglyEdgeSublinearSeparators C) :
    38 ∃ a K B : ℕ, 0 < a ∧ 0 < K ∧ 0 < B ∧
    39 ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    40 G ∈ C n → 0 < n → ∀ (x : Fin n → ℚ≥0) (k p δ : ℝ) (ℓ : ℕ),
    41 0 < k → 0 < p → 0 < δ → 0 < ℓ →
    42 (∀ v, (x v : ℝ) ≤ 1) → (∑ v, (x v : ℝ)) ≤ k →
    43 edgeCost G (fun v => (x v : ℝ)) ≤ k ^ 2 / p →
    44 12 * (B : ℝ) * ((Nat.log2 (2 * n) : ℝ) + 1) ≤ δ * ℓ →
    45 (K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ k →
    46 (2 * K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ p →
    47 ∃ q, ∃ T : Lax263307.CutTraces.Trace G Finset.univ q,
    48 q ≤ n ∧ IsBalancedSeparator G (Lax263307.CutTraces.separator T) ∧
    49 cost (fun v => (x v : ℝ)) (Lax263307.CutTraces.separator T) ≤ δ * k
    50
    51end Lax263307.LightSeparators
    52
    Show Proof
    Formalization notes

    The load parameter ell needs only a multiple of log n / delta. This theorem instantiates the remainder oracle using the registered directed split solver: restriction cannot increase costs, the larger remainder supplies the load scale inequality, and a sufficiently large finite rational capacity excludes expensive split arcs. Orienting the cut toward its smaller shore supplies the exclusive-piece bound. The accumulated trace cost is at most delta*k. Actual RAM construction and iteration costs remain separate obligations.

    Attribution

    Bonnet–Chang, Lemmas 7–8 and 11.

    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…