Computing the recursive answer-or-cut decision
Lax263307.ComputedRounding · concepts/Lax263307/ComputedRounding.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Round each part's rational cost to a target. Skip queries on light parts. Scan child answers in a fixed order: the first failed query determines the returned component inequality; if all required queries succeed, return the union of their independent sets. The selected inequality has the required positive gap and coefficient bound, and the returned union has the required approximation guarantee.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax263307.HeavyRecursiveRounding |
| 2 | import Mathlib.Data.Rat.Floor |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Computing the recursive answer-or-cut decision |
| 7 | type: theorem |
| 8 | --- |
| 9 | Round each part's rational cost to a target. Skip queries on light parts. |
| 10 | Scan child answers in a fixed order: the first failed query determines the |
| 11 | returned component inequality; if all required queries succeed, return the |
| 12 | union of their independent sets. The selected inequality has the required |
| 13 | positive gap and coefficient bound, and the returned union has the required |
| 14 | approximation guarantee. |
| 15 | |
| 16 | # Formalization notes |
| 17 | |
| 18 | The decision and target formulas are computable. Child-query correctness is |
| 19 | an explicit induction hypothesis for this one recursive step. This does not |
| 20 | assert correctness or a RAM bound for the complete recursive program. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax263307.ComputedRounding |
| 24 | |
| 25 | def target (δ cost : ℚ) : ℕ := ⌊(1 - δ) * cost⌋₊ + 1 |
| 26 | |
| 27 | def answer {n : ℕ} {ι : Type} (δ : ℚ) (k : ℕ) (cost : ι → ℚ) |
| 28 | (query : ι → ℕ → Option (Finset (Fin n))) (i : ι) : Option (Finset (Fin n)) := |
| 29 | if δ * k / (4 * n) < cost i then query i (target δ (cost i)) else some ∅ |
| 30 | |
| 31 | inductive Result (n : ℕ) |
| 32 | | found (vertices : Finset (Fin n)) |
| 33 | | cut (vertices : Finset (Fin n)) (bound : ℕ) |
| 34 | |
| 35 | def collect {n : ℕ} {ι : Type} [Fintype ι] (order : List ι) (parts : ι → Finset (Fin n)) |
| 36 | (δ : ℚ) (k : ℕ) (cost : ι → ℚ) (query : ι → ℕ → Option (Finset (Fin n))) : Result n := |
| 37 | match order.find? (fun i => (answer δ k cost query i).isNone) with |
| 38 | | some i => .cut (parts i) (target δ (cost i) - 1) |
| 39 | | none => .found (Lax263307.SeparatorComponents.combine (fun i => (answer δ k cost query i).getD ∅)) |
| 40 | |
| 41 | open Lax263307.LinearRelaxation Lax263307.SeparatorComponents |
| 42 | open Lax263307.ComponentCutEncoding |
| 43 | |
| 44 | axiom collect_correct {n r : ℕ} {ι : Type} [Fintype ι] |
| 45 | (G : SimpleGraph (Fin n)) (k h : ℕ) (δ : ℚ) (η : ℝ) |
| 46 | (hn : 0 < n) (hk : 0 < k) (hδ : 0 < δ) (small : δ ≤ 1 / 4) (hη : 0 < η) |
| 47 | (x y : MomentVector n r) (feasible : IsFeasible G k r y) |
| 48 | (A S : Finset (Fin n)) (P : Partition G S ι) (size : A.card ≤ r) |
| 49 | (moment : η ≤ value y A) (count : Fintype.card ι ≤ 2 * n) |
| 50 | (light : ∑ v ∈ S, conditioned y A v ≤ (δ : ℝ) * k) |
| 51 | (order : List ι) (complete : ∀ i, i ∈ order) |
| 52 | (c : ι → ℚ) (cost_cast : ∀ i, (c i : ℝ) = ∑ v ∈ P.vertices i, conditioned y A v) |
| 53 | (query : ι → ℕ → Option (Finset (Fin n))) |
| 54 | (queries : ∀ i, δ * k / (4 * n) < c i → |
| 55 | match query i (target δ (c i)) with |
| 56 | | some I => I ⊆ P.vertices i ∧ G.IsIndepSet (I : Set (Fin n)) ∧ |
| 57 | (1 - 4 * (δ : ℝ)) ^ h * (target δ (c i) : ℝ) ≤ I.card |
| 58 | | none => IsIndependenceBound G (P.vertices i) (target δ (c i) - 1)) |
| 59 | (near : ∀ B, |x B - y B| ≤ η * (δ : ℝ) ^ 2 / (32 * (n : ℝ) ^ 2)) : |
| 60 | match collect order P.vertices δ k c query with |
| 61 | | .found I => G.IsIndepSet (I : Set (Fin n)) ∧ |
| 62 | (1 - 4 * (δ : ℝ)) ^ (h + 1) * (k : ℝ) ≤ I.card |
| 63 | | .cut C u => u ≤ n ∧ IsIndependenceBound G C u ∧ |
| 64 | (∀ z ∈ independentSetHull G k r, evaluate (coefficient A C u) z ≤ 0) ∧ |
| 65 | η * (δ : ℝ) ^ 2 / (16 * n) ≤ evaluate (coefficient A C u) x ∧ |
| 66 | (∑ B : Coordinate n r, |(coefficient A C u B : ℝ)|) ≤ 2 * n |
| 67 | |
| 68 | end Lax263307.ComputedRounding |
| 69 |
Formalization notes
The decision and target formulas are computable. Child-query correctness is an explicit induction hypothesis for this one recursive step. This does not assert correctness or a RAM bound for the complete recursive program.
Builds on
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments