Lax Lean Archive

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

Quantitative gaps for recursive component cuts

Lax263307.StrongComponentGaps · concepts/Lax263307/StrongComponentGaps.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 collected component normal has sum of absolute coefficients at most |C|+u, hence at most 2n for u≤n. A heavy part of conditioned cost at least deltak/(2n), queried at floor((1-delta)cost)+1, gives a feasible-point cut gap at least etadelta²k/(2n) whenever the conditioning moment is at least eta>0. Nearby queried centers retain a positive gap.

    Concept map
    4 concepts; 7 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 central_cut_buffer proven

    2 coefficient_l1 proven

    3 component_gap proven

    4 evaluation_stable proven

    5 query_gap proven

    Lean source view on GitHub

    1import Lax263307.ComponentCutEncoding
    2
    3/-!
    4---
    5title: Quantitative gaps for recursive component cuts
    6type: theorem
    7---
    8The collected component normal has sum of absolute coefficients at most
    9|C|+u, hence at most 2n for u≤n. A heavy part of conditioned cost at least
    10delta*k/(2n), queried at floor((1-delta)*cost)+1, gives a feasible-point
    11cut gap at least eta*delta²*k/(2n) whenever the conditioning moment is
    12at least eta>0. Nearby queried centers retain a positive gap.
    13
    14# Formalization notes
    15
    16The coordinate error radius eta*delta²/(8n²) leaves a query gap of at
    17least eta*delta²/(4n). A central cut with gap Delta retains an entire
    18coordinate cube of radius Delta/(4n) around every valid hull point.
    19This is the buffer needed for ellipsoid stopping even when the exact
    20independent-set hull has no ambient interior.
    21-/
    22
    23namespace Lax263307.StrongComponentGaps
    24
    25open LinearRelaxation ComponentCutEncoding
    26
    27axiom coefficient_l1 {n r : ℕ} (A C : Finset (Fin n)) (u : ℕ) :
    28 (∑ B : Coordinate n r, |(coefficient A C u B : ℝ)|) ≤ C.card + u
    29
    30axiom evaluation_stable {n r : ℕ} (A C : Finset (Fin n)) (u : ℕ)
    31 (x y : MomentVector n r) (ρ : ℝ) (hρ : 0 ≤ ρ)
    32 (near : ∀ B, |x B - y B| ≤ ρ) :
    33 |evaluate (coefficient A C u) x - evaluate (coefficient A C u) y| ≤ (C.card + u) * ρ
    34
    35axiom component_gap {n r : ℕ} (G : SimpleGraph (Fin n)) (k : ℕ)
    36 (y : MomentVector n r) (A C : Finset (Fin n)) (u : ℕ)
    37 (size : A.card ≤ r) (bound : IsIndependenceBound G C u)
    38 (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) (hn : 0 < n) (hk : 0 < k)
    39 (moment : η ≤ value y A)
    40 (heavy : δ * (k : ℝ) / (2 * n) ≤ ∑ v ∈ C, conditioned y A v)
    41 (rounded : (u : ℝ) ≤ (1 - δ) * ∑ v ∈ C, conditioned y A v) :
    42 (∀ z ∈ independentSetHull G k r, evaluate (coefficient A C u) z ≤ 0) ∧
    43 η * δ ^ 2 * (k : ℝ) / (2 * n) ≤ evaluate (coefficient A C u) y
    44
    45axiom query_gap {n r : ℕ} (G : SimpleGraph (Fin n)) (k : ℕ)
    46 (x y : MomentVector n r) (A C : Finset (Fin n)) (u : ℕ)
    47 (size : A.card ≤ r) (bound : IsIndependenceBound G C u) (upper : u ≤ n)
    48 (η δ : ℝ) (hη : 0 < η) (hδ : 0 < δ) (hn : 0 < n) (hk : 0 < k)
    49 (moment : η ≤ value y A)
    50 (heavy : δ * (k : ℝ) / (2 * n) ≤ ∑ v ∈ C, conditioned y A v)
    51 (rounded : (u : ℝ) ≤ (1 - δ) * ∑ v ∈ C, conditioned y A v)
    52 (near : ∀ B, |x B - y B| ≤ η * δ ^ 2 / (8 * (n : ℝ) ^ 2)) :
    53 (∀ z ∈ independentSetHull G k r, evaluate (coefficient A C u) z ≤ 0) ∧
    54 η * δ ^ 2 / (4 * n) ≤ evaluate (coefficient A C u) x
    55
    56axiom central_cut_buffer {n r : ℕ} (A C : Finset (Fin n)) (u : ℕ) (upper : u ≤ n)
    57 (x z : MomentVector n r) (Δ : ℝ) (positive : 0 < Δ) (hn : 0 < n)
    58 (valid : evaluate (coefficient A C u) z ≤ 0)
    59 (gap : Δ ≤ evaluate (coefficient A C u) x)
    60 (perturbed : MomentVector n r)
    61 (near : ∀ B, |perturbed B - z B| ≤ Δ / (4 * n)) :
    62 evaluate (coefficient A C u) perturbed ≤ evaluate (coefficient A C u) x - Δ / 2
    63
    64end Lax263307.StrongComponentGaps
    65
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Formalization notes

    The coordinate error radius etadelta²/(8n²) leaves a query gap of at least etadelta²/(4n). A central cut with gap Delta retains an entire coordinate cube of radius Delta/(4n) around every valid hull point. This is the buffer needed for ellipsoid stopping even when the exact independent-set hull has no ambient interior.

    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…