Lax Lean Archive

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

Repeated cuts yield a balanced light separator

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

    Record a cut sequence that removes its right shore at each step. Its separator is the union of shore intersections; its retained parts are the exclusive discarded pieces and the final remainder. The right shores are disjoint, each cut removes a nonempty shore, and no graph edge joins distinct retained parts. Once the final remainder has at most two thirds of the original order, the separator is balanced and its cost obeys the cumulative cut bound. There are at most nn cuts.

    A cut oracle on every remainder above that size threshold produces such a trace by induction on remainder cardinality.

    Concept map
    9 concepts; 7 descendants hidden
    100%
    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 light_separator_from_oracle proven

    2 trace_correct proven

    Lean source view on GitHub

    1import Lax263307.BalancedPartitions
    2import Lax263307.RepeatedCutAccounting
    3
    4/-!
    5---
    6title: Repeated cuts yield a balanced light separator
    7type: theorem
    8---
    9Record a cut sequence that removes its right shore at each step. Its
    10separator is the union of shore intersections; its retained parts are the
    11exclusive discarded pieces and the final remainder. The right shores are
    12disjoint, each cut removes a nonempty shore, and no graph edge joins distinct
    13retained parts. Once the final remainder has at most two thirds of the
    14original order, the separator is balanced and its cost obeys the cumulative
    15cut bound. There are at most nn cuts.
    16
    17A cut oracle on every remainder above that size threshold produces such a
    18trace by induction on remainder cardinality.
    19
    20# Formalization notes
    21
    22The small-piece condition bounds Bi∖AiB_i\setminus A_i, not the full discarded
    23shore BiB_i, which also contains the separator intersection. The final
    24parts form the concrete partition used by recursive rounding. These
    25statements analyze the finite cut sequence; its RAM implementation remains
    26part of the main algorithm assembly.
    27
    28# Attribution
    29
    30Bonnet–Chang, the repeated-cut construction of Lemma 8.
    31-/
    32
    33namespace Lax263307.CutTraces
    34
    35open Lax263307.SeparatorComponents Lax263307.EdgeSublinearSeparators
    36
    37structure Trace {n : ℕ} (G : SimpleGraph (Fin n)) (start : Finset (Fin n)) (steps : ℕ) where
    38 remaining : ℕ → Finset (Fin n)
    39 left : ℕ → Finset (Fin n)
    40 right : ℕ → Finset (Fin n)
    41 initial : remaining 0 = start
    42 cover : ∀ i < steps, left i ∪ right i = remaining i
    43 next : ∀ i < steps, remaining (i + 1) = left i \ right i
    44 nonempty : ∀ i < steps, (right i).Nonempty
    45 small_piece : ∀ i < steps, 2 * (right i \ left i).card ≤ (remaining i).card
    46 separated : ∀ i < steps, ∀ u ∈ left i \ right i, ∀ v ∈ right i \ left i, ¬G.Adj u v
    47
    48noncomputable def separator {n q : ℕ} {G : SimpleGraph (Fin n)} {start : Finset (Fin n)}
    49 (T : Trace G start q) : Finset (Fin n) := Finset.univ.biUnion fun i : Fin q => T.left i ∩ T.right i
    50
    51def parts {n q : ℕ} {G : SimpleGraph (Fin n)} {start : Finset (Fin n)}
    52 (T : Trace G start q) : Option (Fin q) → Finset (Fin n)
    53 | none => T.remaining q
    54 | some i => T.right i \ T.left i
    55
    56axiom trace_correct {n q : ℕ} (G : SimpleGraph (Fin n)) (T : Trace G Finset.univ q)
    57 (finished : 3 * (T.remaining q).card ≤ 2 * n)
    58 (x : Fin n → ℝ) (nonnegative : ∀ v, 0 ≤ x v) (ρ γ : ℝ) (hρ : 0 ≤ ρ) (hγ : 0 < γ)
    59 (each_cut : ∀ i < q, Lax263307.RepeatedCutAccounting.cost x (T.left i ∩ T.right i) ≤
    60 4 * ρ * (T.left i).card * (T.right i).card / γ) :
    61 q ≤ n ∧ IsBalancedSeparator G (separator T) ∧
    62 Lax263307.RepeatedCutAccounting.cost x (separator T) ≤ 4 * ρ * (n : ℝ) ^ 2 / γ
    63
    64axiom light_separator_from_oracle {n : ℕ} (G : SimpleGraph (Fin n))
    65 (x : Fin n → ℝ) (nonnegative : ∀ v, 0 ≤ x v) (ρ γ : ℝ) (hρ : 0 ≤ ρ) (hγ : 0 < γ)
    66 (oracle : ∀ R : Finset (Fin n), 2 * n < 3 * R.card →
    67 ∃ A B : Finset (Fin n), A ∪ B = R ∧ B.Nonempty ∧ 2 * (B \ A).card ≤ R.card ∧
    68 (∀ u ∈ A \ B, ∀ v ∈ B \ A, ¬G.Adj u v) ∧
    69 Lax263307.RepeatedCutAccounting.cost x (A ∩ B) ≤ 4 * ρ * A.card * B.card / γ) :
    70 ∃ q, ∃ T : Trace G Finset.univ q, q ≤ n ∧ IsBalancedSeparator G (separator T) ∧
    71 Lax263307.RepeatedCutAccounting.cost x (separator T) ≤ 4 * ρ * (n : ℝ) ^ 2 / γ
    72
    73end Lax263307.CutTraces
    74
    Show ProofShow Proof
    Formalization notes

    The small-piece condition bounds Bi∖AiB_i\setminus A_i, not the full discarded shore BiB_i, which also contains the separator intersection. The final parts form the concrete partition used by recursive rounding. These statements analyze the finite cut sequence; its RAM implementation remains part of the main algorithm assembly.

    Attribution

    Bonnet–Chang, the repeated-cut construction of Lemma 8.

    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…