Lax Lean Archive

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

Combining recursive answers in round-or-cut

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

    Suppose conditioning gives costs of total mass kk, and the deleted separator has cost at most δk\delta k. Each remaining part returns an independent set of size at least (1−δ)huC(1-\delta)^h u_C, where uCu_C bounds the part's independence number. Either some conditioned part cost exceeds uCu_C, giving a valid violated cut, or the union of the returned sets is independent and has size at least (1−δ)h+1k(1-\delta)^{h+1}k.

    Concept map
    4 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 combine_independent proven

    2 round_or_cut proven

    Lean source view on GitHub

    1import Lax263307.SeparatorComponents
    2import Lax263307.ComponentCuts
    3
    4/-!
    5---
    6title: Combining recursive answers in round-or-cut
    7type: theorem
    8---
    9Suppose conditioning gives costs of total mass kk, and the deleted
    10separator has cost at most δk\delta k. Each remaining part returns an
    11independent set of size at least (1−δ)huC(1-\delta)^h u_C, where uCu_C bounds
    12the part's independence number. Either some conditioned part cost exceeds
    13uCu_C, giving a valid violated cut, or the union of the returned sets is
    14independent and has size at least (1−δ)h+1k(1-\delta)^{h+1}k.
    15
    16# Attribution
    17
    18Bonnet–Chang, equation (24) and the round-or-cut step in Lemma 14.
    19-/
    20
    21namespace Lax263307.RecursiveRounding
    22
    23open LinearRelaxation SeparatorComponents
    24
    25/-- Independent answers on different parts combine, and their sizes add. -/
    26axiom combine_independent {n : ℕ} {ι : Type} [Fintype ι]
    27 (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) (P : Partition G S ι)
    28 (I : ι → Finset (Fin n)) (inside : ∀ i, I i ⊆ P.vertices i)
    29 (independent : ∀ i, G.IsIndepSet (I i : Set (Fin n))) :
    30 G.IsIndepSet (combine I : Set (Fin n)) ∧ (combine I).card = ∑ i, (I i).card
    31
    32/-- One query returns a sufficiently large set or a valid separating inequality. -/
    33axiom round_or_cut {n r : ℕ} {ι : Type} [Fintype ι]
    34 (G : SimpleGraph (Fin n)) (k h : ℕ) (δ : ℝ)
    35 (δ_nonnegative : 0 ≤ δ) (δ_small : δ ≤ 1)
    36 (y : MomentVector n r) (A S : Finset (Fin n)) (P : Partition G S ι)
    37 (size : A.card ≤ r) (positive : 0 < value y A)
    38 (mass : (∑ v, conditioned y A v) = k)
    39 (light : ∑ v ∈ S, conditioned y A v ≤ δ * k)
    40 (I : ι → Finset (Fin n)) (u : ι → ℕ)
    41 (inside : ∀ i, I i ⊆ P.vertices i)
    42 (independent : ∀ i, G.IsIndepSet (I i : Set (Fin n)))
    43 (bounds : ∀ i, IsIndependenceBound G (P.vertices i) (u i))
    44 (approximation : ∀ i, (1 - δ) ^ h * (u i : ℝ) ≤ (I i).card) :
    45 (G.IsIndepSet (combine I : Set (Fin n)) ∧
    46 (1 - δ) ^ (h + 1) * (k : ℝ) ≤ (combine I).card) ∨
    47 ∃ i, (∀ z ∈ independentSetHull G k r,
    48 ∑ v ∈ P.vertices i, value z (insert v A) ≤ (u i : ℝ) * value z A) ∧
    49 (u i : ℝ) * value y A < ∑ v ∈ P.vertices i, value y (insert v A)
    50
    51end Lax263307.RecursiveRounding
    52
    Show ProofShow Proof

    Attribution

    Bonnet–Chang, equation (24) and the round-or-cut step in Lemma 14.

    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…