Lax Lean Archive

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

Recursive rounding after discarding light parts

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

    At most 2n parts whose conditioned cost is at most deltak/(4n) lose at most deltak/2 in total. Approximate answers at rounded targets on all heavier parts combine into an independent set, losing a factor at most 1-4delta per recursive level. A failed heavy query instead gives a valid component inequality with a uniform positive gap at the nearby queried moment vector.

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

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

    1 heavy_union_size proven

    2 ignored_cost proven

    3 strong_round_or_cut proven

    Lean source view on GitHub

    1import Lax263307.StrongComponentGaps
    2import Lax263307.ConditionedCosts
    3import Lax263307.RecursiveRounding
    4
    5/-!
    6---
    7title: Recursive rounding after discarding light parts
    8type: theorem
    9---
    10At most 2n parts whose conditioned cost is at most delta*k/(4n) lose
    11at most delta*k/2 in total. Approximate answers at rounded targets on
    12all heavier parts combine into an independent set, losing a factor
    13at most 1-4delta per recursive level. A failed heavy query instead gives
    14a valid component inequality with a uniform positive gap at the nearby
    15queried moment vector.
    16
    17# Formalization notes
    18
    19These are the mathematical answer-or-cut invariants for the recursive
    20oracle. They do not assume that every part receives a recursive query.
    21The explicit RAM loop and its running time remain separate obligations.
    22-/
    23
    24namespace Lax263307.HeavyRecursiveRounding
    25
    26open Lax263307.LinearRelaxation Lax263307.SeparatorComponents
    27open Lax263307.ComponentCutEncoding
    28
    29axiom ignored_cost {n : ℕ} {ι : Type} [Fintype ι] (c : ι → ℝ) (δ k : ℝ)
    30 (hn : 0 < n) (hδ : 0 ≤ δ) (hk : 0 ≤ k) (count : Fintype.card ι ≤ 2 * n) :
    31 (∑ i, if δ * k / (4 * n) < c i then 0 else c i) ≤ δ * k / 2
    32
    33axiom heavy_union_size {n : ℕ} {ι : Type} [Fintype ι]
    34 (G : SimpleGraph (Fin n)) (S : Finset (Fin n)) (P : Partition G S ι)
    35 (x : Fin n → ℝ) (k : ℕ) (h : ℕ) (δ : ℝ)
    36 (hn : 0 < n) (hδ : 0 ≤ δ) (small : δ ≤ 1 / 4)
    37 (count : Fintype.card ι ≤ 2 * n)
    38 (mass : (∑ v, x v) = k) (light : ∑ v ∈ S, x v ≤ δ * k)
    39 (I : ι → Finset (Fin n)) (targets : ι → ℕ)
    40 (inside : ∀ i, I i ⊆ P.vertices i)
    41 (independent : ∀ i, G.IsIndepSet (I i : Set (Fin n)))
    42 (rounded : ∀ i, δ * k / (4 * n) < ∑ v ∈ P.vertices i, x v →
    43 (1 - δ) * (∑ v ∈ P.vertices i, x v) < targets i)
    44 (answers : ∀ i, δ * k / (4 * n) < ∑ v ∈ P.vertices i, x v →
    45 (1 - 4 * δ) ^ h * (targets i : ℝ) ≤ (I i).card) :
    46 G.IsIndepSet (combine I : Set (Fin n)) ∧
    47 (1 - 4 * δ) ^ (h + 1) * (k : ℝ) ≤ (combine I).card
    48
    49axiom strong_round_or_cut {n r : ℕ} {ι : Type} [Fintype ι]
    50 (G : SimpleGraph (Fin n)) (k h : ℕ) (δ η : ℝ)
    51 (hn : 0 < n) (hk : 0 < k) (hδ : 0 < δ) (small : δ ≤ 1 / 4) (hη : 0 < η)
    52 (x y : MomentVector n r) (feasible : Lax263307.LinearRelaxation.IsFeasible G k r y)
    53 (A S : Finset (Fin n)) (P : Partition G S ι) (size : A.card ≤ r)
    54 (moment : η ≤ value y A) (count : Fintype.card ι ≤ 2 * n)
    55 (light : ∑ v ∈ S, conditioned y A v ≤ δ * k)
    56 (I : ι → Finset (Fin n)) (targets : ι → ℕ)
    57 (inside : ∀ i, I i ⊆ P.vertices i)
    58 (independent : ∀ i, G.IsIndepSet (I i : Set (Fin n)))
    59 (target_lower : ∀ i, δ * k / (4 * n) < ∑ v ∈ P.vertices i, conditioned y A v →
    60 (1 - δ) * (∑ v ∈ P.vertices i, conditioned y A v) < targets i)
    61 (target_upper : ∀ i, δ * k / (4 * n) < ∑ v ∈ P.vertices i, conditioned y A v →
    62 (targets i - 1 : ℕ) ≤ (1 - δ) * (∑ v ∈ P.vertices i, conditioned y A v))
    63 (queries : ∀ i, δ * k / (4 * n) < ∑ v ∈ P.vertices i, conditioned y A v →
    64 ((1 - 4 * δ) ^ h * (targets i : ℝ) ≤ (I i).card) ∨
    65 IsIndependenceBound G (P.vertices i) (targets i - 1))
    66 (near : ∀ B, |x B - y B| ≤ η * δ ^ 2 / (32 * (n : ℝ) ^ 2)) :
    67 (G.IsIndepSet (combine I : Set (Fin n)) ∧
    68 (1 - 4 * δ) ^ (h + 1) * (k : ℝ) ≤ (combine I).card) ∨
    69 ∃ i, (∀ z ∈ independentSetHull G k r,
    70 evaluate (coefficient A (P.vertices i) (targets i - 1)) z ≤ 0) ∧
    71 η * δ ^ 2 / (16 * n) ≤ evaluate (coefficient A (P.vertices i) (targets i - 1)) x
    72
    73end Lax263307.HeavyRecursiveRounding
    74
    Show ProofShow ProofShow Proof
    Formalization notes

    These are the mathematical answer-or-cut invariants for the recursive oracle. They do not assume that every part receives a recursive query. The explicit RAM loop and its running time remain separate obligations.

    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…