Lax Lean Archive

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

Computing balanced light separators from registered flow-cut outputs

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

    Label each remaining vertex set in increasing order, construct its rational split network, and read the cut membership prefix of the registered Leighton–Rao solver's output. Orient the two projected shores by size. Repeat until the remainder has at most two thirds of the original vertices. The computed list has at most n cuts. Its separator has the stated cost, and its computed pieces form a balanced partition with no cross edges.

    Concept map
    57 concepts; 5 descendants hidden
    100%
    TreewidthTreewidth transfer through analmost-embeddingBalanced closed parts certify a balancedseparatorComputing balanced light separators fromregistered flow-cut outputsConditioning 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.LightSeparators
    2import Mathlib.Data.Finset.Sort
    3import Mathlib.Data.List.GetD
    4
    5/-!
    6---
    7title: Computing balanced light separators from registered flow-cut outputs
    8type: theorem
    9---
    10Label each remaining vertex set in increasing order, construct its rational
    11split network, and read the cut membership prefix of the registered
    12Leighton–Rao solver's output. Orient the two projected shores by size.
    13Repeat until the remainder has at most two thirds of the original vertices.
    14The computed list has at most n cuts. Its separator has the stated cost,
    15and its computed pieces form a balanced partition with no cross edges.
    16
    17# Formalization notes
    18
    19All labels, rational capacities, output decoding, shore choices, and the
    20bounded cut-list loop are computable. The solver retains its actual registered
    21RAM polynomial-time guarantee. This statement proves the wrapper's functional
    22correctness; the RAM implementation and time bound for its surrounding loops
    23remain separate obligations.
    24-/
    25
    26namespace Lax263307.ComputedSeparators
    27
    28open scoped NNRat
    29open Lax263307.VertexSplitting Lax455465.RationalEncoding
    30
    31def decodeCut (n : ℕ) (words : List ℕ) : Finset (Fin n) :=
    32 Finset.univ.filter fun v => words.getD v.val 0 = 1
    33
    34def label {n : ℕ} (R : Finset (Fin n)) : Fin R.card ↪o Fin n :=
    35 R.orderEmbOfFin rfl
    36
    37def restriction {n : ℕ} (G : SimpleGraph (Fin n)) (R : Finset (Fin n)) :
    38 SimpleGraph (Fin R.card) := G.comap (label R)
    39
    40instance {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (R : Finset (Fin n)) :
    41 DecidableRel (restriction G R).Adj := inferInstanceAs (DecidableRel (G.comap (label R)).Adj)
    42
    43def ratio (B n : ℕ) : ℚ := B * ((Nat.log2 (2 * n) : ℚ) + 1)
    44def scale (n ℓ k : ℕ) : ℚ := (ℓ : ℚ) * n ^ 2 / (3 * k)
    45
    46def largeCapacity (B n r ℓ k : ℕ) : ℚ≥0 :=
    47 (Nat.ceil (ratio B n * (2 * r : ℕ) ^ 2 / scale n ℓ k) + 1 : ℕ)
    48
    49def orient {n : ℕ} (A B : Finset (Fin n)) : Finset (Fin n) × Finset (Fin n) :=
    50 if B.card ≤ A.card then (A, B) else (B, A)
    51
    52def step {n : ℕ} (solve : List ℕ → List ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    53 (x : Fin n → ℚ≥0) (B ℓ k : ℕ) (R : Finset (Fin n)) :
    54 Finset (Fin n) × Finset (Fin n) :=
    55 let I := splitInstance (restriction G R) (fun v => x (label R v))
    56 (largeCapacity B n R.card ℓ k)
    57 let U := decodeCut (2 * R.card) (solve (encodeInput .directed I))
    58 let shores := orient (leftShore U) (rightShore U)
    59 (shores.1.image (label R), shores.2.image (label R))
    60
    61def cuts {n : ℕ} (cut : Finset (Fin n) → Finset (Fin n) × Finset (Fin n)) :
    62 ℕ → Finset (Fin n) → List (Finset (Fin n) × Finset (Fin n))
    63 | 0, _ => []
    64 | fuel + 1, R =>
    65 if 3 * R.card ≤ 2 * n then []
    66 else let s := cut R
    67 s :: cuts cut fuel (s.1 \ s.2)
    68
    69def separator {n : ℕ} (cs : List (Finset (Fin n) × Finset (Fin n))) : Finset (Fin n) :=
    70 cs.foldr (fun s S => (s.1 ∩ s.2) ∪ S) ∅
    71
    72def remaining {n : ℕ} (start : Finset (Fin n))
    73 (cs : List (Finset (Fin n) × Finset (Fin n))) : Finset (Fin n) :=
    74 if h : cs.length = 0 then start else
    75 let s := cs.get ⟨cs.length - 1, by omega⟩
    76 s.1 \ s.2
    77
    78def pieces {n : ℕ} (cs : List (Finset (Fin n) × Finset (Fin n))) :
    79 Option (Fin cs.length) → Finset (Fin n)
    80 | none => remaining Finset.univ cs
    81 | some i => (cs.get i).2 \ (cs.get i).1
    82
    83open Lax263307.GraphClasses Lax263307.PowerBagBounds
    84open Lax263307.Entropy Lax263307.RepeatedCutAccounting
    85
    86axiom light_separator (C : GraphClass) (hereditary : IsHereditary C)
    87 (a A : ℕ) (ha : 0 < a) (hA : 0 < A) (class_bound : HasPowerBagBound C a A) :
    88 ∃ (solve : List ℕ → List ℕ) (K B : ℕ), Lax759944.RamPolytime.RamPolytime solve ∧
    89 0 < K ∧ 0 < B ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    90 G ∈ C n → 0 < n → ∀ (x : Fin n → ℚ≥0) (k p ℓ : ℕ),
    91 0 < k → 0 < p → 0 < ℓ →
    92 (∀ v, (x v : ℝ) ≤ 1) → (∑ v, (x v : ℝ)) ≤ k →
    93 edgeCost G (fun v => (x v : ℝ)) ≤ (k : ℝ) ^ 2 / p →
    94 (K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ k →
    95 (2 * K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ p →
    96 let cs := cuts (step solve G x B ℓ k) n Finset.univ
    97 cs.length ≤ n ∧
    98 Lax263307.EdgeSublinearSeparators.IsBalancedSeparator G
    99 (Lax263307.ComputedSeparators.separator cs) ∧
    100 cost (fun v => (x v : ℝ)) (Lax263307.ComputedSeparators.separator cs) ≤
    101 12 * (ratio B n : ℝ) * k / ℓ ∧
    102 ∃ P : Lax263307.SeparatorComponents.Partition G
    103 (Lax263307.ComputedSeparators.separator cs) (Option (Fin cs.length)),
    104 (∀ i, P.vertices i = pieces cs i) ∧ ∀ i, 3 * (P.vertices i).card ≤ 2 * n
    105
    106end Lax263307.ComputedSeparators
    107
    Show Proof
    Formalization notes

    All labels, rational capacities, output decoding, shore choices, and the bounded cut-list loop are computable. The solver retains its actual registered RAM polynomial-time guarantee. This statement proves the wrapper's functional correctness; the RAM implementation and time bound for its surrounding loops remain separate obligations.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…