Infinity-distance projection LP and its separating dual
Lax263307.DistanceProjection · concepts/Lax263307/DistanceProjection.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Append one nonnegative distance variable t to a linear program and impose |y_j-center_j|≤t for every coordinate. Maximizing -t finds a nearest feasible point. A matching dual certificate supplies a separating normal whose sum of absolute coefficients is at most one, and its gap at the queried center is exactly t. Thus a distance threshold yields either a nearby feasible point for round-or-cut or a uniformly strong separation.
Concept map
Evidence
This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.
1 dual_normal proven
2 objective_bounded proven
3 optimal_gap proven
4 primal_characterization proven
5 projection_feasible_iff proven
6 strong_gap_dichotomy proven
Lean source view on GitHub
| 1 | import Lax109476.RationalCertificates |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Infinity-distance projection LP and its separating dual |
| 6 | type: theorem |
| 7 | --- |
| 8 | Append one nonnegative distance variable t to a linear program and impose |
| 9 | |y_j-center_j|≤t for every coordinate. Maximizing -t finds a nearest feasible |
| 10 | point. A matching dual certificate supplies a separating normal whose sum |
| 11 | of absolute coefficients is at most one, and its gap at the queried center |
| 12 | is exactly t. Thus a distance threshold yields either a nearby feasible |
| 13 | point for round-or-cut or a uniformly strong separation. |
| 14 | |
| 15 | # Formalization notes |
| 16 | |
| 17 | Rows and variables use computable finite index concatenation. No choice-based |
| 18 | coordinate labeling is needed to form the dense rational program. The |
| 19 | algebra holds in real variables and applies to exact rational certificates |
| 20 | by casting. It makes no full-dimensionality assumption. The actual matrix |
| 21 | construction and registered solver invocation remain RAM wrapper obligations. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax263307.DistanceProjection |
| 25 | |
| 26 | open Lax109476.LinearProgram |
| 27 | |
| 28 | /-- The distance LP with one additional variable and two rows per coordinate. -/ |
| 29 | def distanceProgram {K : Type} [Ring K] {m n : ℕ} (P : Program K m n) (center : Fin n → K) : |
| 30 | Program K (m + (n + n)) (n + 1) where |
| 31 | A := Fin.addCases |
| 32 | (fun i => Fin.addCases (P.A i) (fun _ => 0)) |
| 33 | (Fin.addCases |
| 34 | (fun i => Fin.addCases (fun j => if i = j then 1 else 0) (fun _ => -1)) |
| 35 | (fun i => Fin.addCases (fun j => if i = j then -1 else 0) (fun _ => -1))) |
| 36 | b := Fin.addCases P.b (Fin.addCases center (fun i => -center i)) |
| 37 | c := Fin.addCases (fun _ => 0) (fun _ => -1) |
| 38 | |
| 39 | def point {K : Type} {n : ℕ} (z : Fin (n + 1) → K) (j : Fin n) : K := z (Fin.castAdd 1 j) |
| 40 | def distance {K : Type} {n : ℕ} (z : Fin (n + 1) → K) : K := z (Fin.natAdd n (0 : Fin 1)) |
| 41 | |
| 42 | |
| 43 | def oldMultipliers {K : Type} {m n : ℕ} (dual : Fin (m + (n + n)) → K) (i : Fin m) : K := |
| 44 | dual (Fin.castAdd (n + n) i) |
| 45 | def plusMultipliers {K : Type} {m n : ℕ} (dual : Fin (m + (n + n)) → K) (i : Fin n) : K := |
| 46 | dual (Fin.natAdd m (Fin.castAdd n i)) |
| 47 | def minusMultipliers {K : Type} {m n : ℕ} (dual : Fin (m + (n + n)) → K) (i : Fin n) : K := |
| 48 | dual (Fin.natAdd m (Fin.natAdd n i)) |
| 49 | def normal {K : Type} [Sub K] {m n : ℕ} (dual : Fin (m + (n + n)) → K) (i : Fin n) : K := |
| 50 | minusMultipliers dual i - plusMultipliers dual i |
| 51 | |
| 52 | |
| 53 | axiom primal_characterization {m n : ℕ} (P : Program ℝ m n) (center : Fin n → ℝ) |
| 54 | (z : Fin (n + 1) → ℝ) : |
| 55 | PrimalFeasible (distanceProgram P center) z ↔ |
| 56 | PrimalFeasible P (point z) ∧ 0 ≤ distance z ∧ |
| 57 | ∀ j, |point z j - center j| ≤ distance z |
| 58 | |
| 59 | axiom objective_bounded {m n : ℕ} (P : Program ℝ m n) (center : Fin n → ℝ) : |
| 60 | IsBoundedAbove (distanceProgram P center) |
| 61 | |
| 62 | axiom projection_feasible_iff {m n : ℕ} (P : Program ℝ m n) (center : Fin n → ℝ) : |
| 63 | IsFeasible (distanceProgram P center) ↔ IsFeasible P |
| 64 | |
| 65 | axiom dual_normal {m n : ℕ} (P : Program ℝ m n) (center : Fin n → ℝ) |
| 66 | (dual : Fin (m + (n + n)) → ℝ) (feasible : DualFeasible (distanceProgram P center) dual) : |
| 67 | (∑ j, |normal dual j|) ≤ 1 ∧ |
| 68 | ∀ z, PrimalFeasible P z → (∑ j, normal dual j * z j) ≤ dualValue P (oldMultipliers dual) |
| 69 | |
| 70 | axiom optimal_gap {m n : ℕ} (P : Program ℝ m n) (center : Fin n → ℝ) |
| 71 | (z : Fin (n + 1) → ℝ) (dual : Fin (m + (n + n)) → ℝ) |
| 72 | (primal : PrimalFeasible (distanceProgram P center) z) |
| 73 | (dual_feasible : DualFeasible (distanceProgram P center) dual) |
| 74 | (matching : primalValue (distanceProgram P center) z = dualValue (distanceProgram P center) dual) : |
| 75 | PrimalFeasible P (point z) ∧ 0 ≤ distance z ∧ |
| 76 | (∀ j, |point z j - center j| ≤ distance z) ∧ |
| 77 | (∑ j, |normal dual j|) ≤ 1 ∧ |
| 78 | (∀ y, PrimalFeasible P y → (∑ j, normal dual j * y j) ≤ dualValue P (oldMultipliers dual)) ∧ |
| 79 | (∑ j, normal dual j * center j) - dualValue P (oldMultipliers dual) = distance z |
| 80 | |
| 81 | axiom strong_gap_dichotomy {m n : ℕ} (P : Program ℝ m n) (center : Fin n → ℝ) |
| 82 | (z : Fin (n + 1) → ℝ) (dual : Fin (m + (n + n)) → ℝ) |
| 83 | (primal : PrimalFeasible (distanceProgram P center) z) |
| 84 | (dual_feasible : DualFeasible (distanceProgram P center) dual) |
| 85 | (matching : primalValue (distanceProgram P center) z = dualValue (distanceProgram P center) dual) |
| 86 | (ρ : ℝ) : |
| 87 | (PrimalFeasible P (point z) ∧ ∀ j, |point z j - center j| ≤ ρ) ∨ |
| 88 | ((∑ j, |normal dual j|) ≤ 1 ∧ |
| 89 | (∀ y, PrimalFeasible P y → (∑ j, normal dual j * y j) ≤ dualValue P (oldMultipliers dual)) ∧ |
| 90 | ρ < (∑ j, normal dual j * center j) - dualValue P (oldMultipliers dual)) |
| 91 | |
| 92 | end Lax263307.DistanceProjection |
| 93 |
Formalization notes
Rows and variables use computable finite index concatenation. No choice-based coordinate labeling is needed to form the dense rational program. The algebra holds in real variables and applies to exact rational certificates by casting. It makes no full-dimensionality assumption. The actual matrix construction and registered solver invocation remain RAM wrapper obligations.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments