Courtade–Kumar proof module `CKLaneC.RSC2.BD_0180` (transplant)

import Definitions.Def_CK_CKLaneC_RSC2_BD_0180_part00

/-! RA-stat cover batch BD_0180 (generated by tools/emit_cover2.py; compact format). -/

namespace CKLaneC.RSC2.BD_0180
open CKLaneC.TM3 CKLaneC.RSCell

theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

noncomputable def c3 : Cell := { bc := 8863084066665136128, bh := 72057594037927936, tc := 13546827679130451968, th := 288230376151711744, sc := 16303030651081195520, sh := 126100789566373888 }
noncomputable def q3 : Cert := { V0 := [[[762154356312875865]], [[(-45274312532871557), 16176140436332659], [5431939798899831]], [[35139971153655, (-956174108388091), (-1270018161876)], [(-299349073991591), 114720244294372], [24909742403124]], [[(-553940834044), 320302581856, 225790427024, (-8876580384)], [(-1032345777950), (-6220901316834), (-27089975269)], [(-1163366060248), 520010811660], [177866930772]], [[1069862787, (-2728215495), (-13508011812), 1562622536, 2069505], [(-8579710292), (-30452776116), 4692190236, (-187480961)], [(-15243143431), (-23077209571), (-316151667)], [(-7664075269), 3686418757], [1008084933]]], r0 := 14980360096, V1 := [[[1036738282652144518]], [[(-61456396338806118), 0], [7373440401272717]], [[36239760288237, 0, 0], [(-403593422827386), 0], [33648093730998]], [[(-511022803456), 0, 0, 0], [(-1635318265800), 0, 0], [(-1538751923209), 0], [239542339854]], [[813320000, 0, 0, 0, 0], [(-7547846089), 0, 0, 0], [(-23151671098), 0, 0], [(-10008387772), 0], [1348858645]]], r1 := 6159917072, V2 := [[[1483095149587387687]], [[(-45329630173380120), 16009936302107470], [(-138696671424676150)]], [[37039292909034, (-939625111082712), (-2430072256356)], [(-292743921475953), 156489932643895], [13056754844059]], [[(-547306536316), (-87778377838), 360286898350, (-8343161574)], [(-1350090444067), (-9938120650212), 182110351051], [(-268564012317), (-1109414943185)], [173850130682]], [[993188742, (-2003806789), (-17249552858), 1447011926, 3839584], [(-10246110082), 45772218896, (-19414058936), (-311879181)], [(-27929451853), 54347783066, 4237658939], [(-8554677586), (-11618881231)], [(-386648726)]]], r2 := 50855488028, V3 := [[[2246377359165797802]], [[(-90819926323430581), 31685899348866570], [(-133145637927925720)]], [[84867867121329, (-1827041958317970), (-14515122072286)], [(-603771365990647), 330851875014421], [27185864842726]], [[(-1314820514989), (-2885627137849), 2274895506062, (-61025827266)], [(-1911081001726), (-21723442690644), 577940162588], [(-663885771645), (-1875923468205)], [363734765893]], [[1007891288, 45306125303, (-116360377123), 10026112909, 88189270], [(-31420885920), 123593654876, (-50248542463), (-2689102245)], [(-51695110287), 70129235758, 16472242382], [(-18481023921), (-22068163892)], [(-512763332)]]], r3 := 196110909320, Vm := [[[2032678679213609169]], [[(-83176364816906327), 0], [(-112880294828075887)]], [[124703280545142, 0, 0], [(-1464139298610681), 0], [1421310549468344]], [[4476738208375, 0, 0, 0], [(-25072871610053), 0, 0], [7175199566519, 0], [79050218388954]], [[186869303278, 0, 0, 0, 0], [(-671409794628), 0, 0, 0], [(-1591276642542), 0, 0], [4644467285816, 0], [3893739813664]]], rm := 30825702169140 }
noncomputable def w3 : Wit := { Z0 := { p := [[[763094280437628356]], [[(-45441985242662328), 16236048519949539], [5452056903159353]], [[45255599051238, (-966850749843880), 0], [(-302853794353784), 116001210705518], [25145734517752]], [[(-771217271619), 962885086196, 0, 0], [(-830375478525), (-6443697752209), 0], [(-1203130173991), 535015628037], [180188912119]], [[1878807775, (-16408878120), 0, 0, 0], [(-12404157550), (-17667563373), 0, 0], [(-13101270906), (-25598514341), 0], [(-8041889908), 3833806640], [1029018497]]], r := 2190147219, ok := true }, Z1 := { p := [[[1039107105276770528]], [[(-61878447990008277), 0], [7424077485153161]], [[61624645516580, 0, 0], [(-412396656141322), 0], [34241000194386]], [[(-1050168199651), 0, 0, 0], [(-1130724055863), 0, 0], [(-1638304917775), 0], [245363625013]], [[2558376545, 0, 0, 0, 0], [(-16890767727), 0, 0, 0], [(-17840028467), 0, 0], [(-10950658598), 0], [1401216677]]], r := 1239608995, ok := true }, Z2 := { p := [[[1490050402459499656]], [[(-45969831547017972), 16236048519949539], [(-140655518192793394)]], [[57318228144603, (-966850749843880), 0], [(-175983251796844), 116001210705518], [198194760193452]], [[(-796345283851), 962885086196, 0, 0], [(-3131443197393), (-6443697752209), 0], [(-5373609077439), 535015628037], [(-5846037700806)]], [[2190521739, (-16408878120), 0, 0, 0], [(-6665799790), (-17667563373), 0, 0], [(-33311731008), (-25598514341), 0], [(-24290931168), 3833806640], [16671890785]]], r := 3682630665, ok := true }, Z3 := { p := [[[2270728210660322390]], [[(-93799714882368495), 32725509092912931], [(-137514126921819199)]], [[210812823010773, (-1972925122165751), 0], [(-262464732625661), 215718269223390], [292783273949918]], [[(-3395715851024), 3947209421492, 0, 0], [(-8623637022640), (-11092923097274), 0], [(-10013637138554), 838983801175], [(-5427962391829)]], [[14439665298, (-70381914738), 0, 0, 0], [(-17449453282), (-78710047776), 0, 0], [(-71603059091), (-26891030555), 0], [(-31941965823), 5595927276], [23039924978]]], r := 10682334573, ok := true }, iE := { p := [[[18610076723759905272]], [[(-13512865391504480), 0], [(-18338577704409255)]], [[308803304790129, 0, 0], [545312811156754, 0], [762339516416071]], [[(-643277113137), 0, 0, 0], [2853327355009, 0, 0], [2298302303104, 0], [(-1803498007649)]], [[7979877477, 0, 0, 0, 0], [18246536016, 0, 0, 0], [53277692382, 0, 0], [43685004363, 0], [39757929055]]], r := 7100518268, ok := true }, iHu := { p := [[[18755309652311413715]], [[(-27449193998802143), 0], [(-28851940265872171)]], [[647525893136338, 0, 0], [1138069115662204, 0], [715398450368988]], [[(-2246805973573), 0, 0, 0], [3444000331778, 0, 0], [3620000348733, 0], [(-2609166856200)]], [[29742644151, 0, 0, 0, 0], [70250228091, 0, 0, 0], [124760378392, 0, 0], [77613736915, 0], [36304569070]]], r := 15024478706, ok := true }, T := { p := [[[13546827679130451968]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18284844924174454378]], [[13276713032002167, 0], [18018090652304418]], [[(-293766338810262), 0, 0], [(-509616820002972), 0], [(-731261557044036)]], [[198424996191, 0, 0, 0], [(-4150992890461), 0, 0], [(-4363122608440), 0], [313297042066]], [[(-2362854849), 0, 0, 0, 0], [(-5094784710), 0, 0, 0], [(-24906672894), 0, 0], [(-5628811335), 0], [(-7053005461)]]], r := 5171766732, ok := true }, de := { p := [[[(-4042288804949100943)]], [[178882887621550530, 0], [188024405688157061]], [[(-181240147042761), 0, 0], [1073328161676490, 0], [(-200237429442437)]], [[2877622400552, 0, 0, 0], [6127041531824, 0, 0], [6440153991058, 0], [3341720237747]], [[(-8374531736), 0, 0, 0, 0], [34975918152, 0, 0, 0], [80051630955, 0, 0], [38642034104, 0], [(-10222149863)]]], r := 5203169814, ok := true }, dde := { p := [[[(-54463502546647783888)]], [[110362409074047335, 0], [116002299897808173]], [[(-2628402252858293), 0, 0], [(-4628189563478728), 0], [(-2903906883991231)]], [[10198993018847, 0, 0, 0], [(-10577660271609), 0, 0], [(-11118214338913), 0], [11843868524649]], [[(-136720644333), 0, 0, 0, 0], [(-326074191767), 0, 0, 0], [(-557105140858), 0, 0], [(-360252731158), 0], [(-166884425291)]]], r := 139644260357, ok := true }, nJu := { p := [[[(-8084577609898201885)]], [[357765775243101060, 0], [376048811376314123]], [[(-362480294085521), 0, 0], [2146656323352981, 0], [(-400474858884873)]], [[5755244801105, 0, 0, 0], [12254083063649, 0, 0], [12880307982116, 0], [6683440475495]], [[(-16749063471), 0, 0, 0, 0], [69951836304, 0, 0, 0], [160103261911, 0, 0], [77284068209, 0], [(-20444299726)]]], r := 10406339617, ok := true }, Jd1 := { p := [[[(-108927005093295567776)]], [[220724818148094671, 0], [232004599795616346]], [[(-5256804505716586), 0, 0], [(-9256379126957456), 0], [(-5807813767982462)]], [[20397986037695, 0, 0, 0], [(-21155320543217), 0, 0], [(-22236428677825), 0], [23687737049298]], [[(-273441288666), 0, 0, 0, 0], [(-652148383534), 0, 0, 0], [(-1114210281715), 0, 0], [(-720505462315), 0], [(-333768850582)]]], r := 279288520708, ok := true }, term0 := { p := [[[333722054552556548837]], [[(-1323878662838388048), 0], [(-1260277680577139032)]], [[33465167351245104, 0, 0], [53335463939641307, 0], [30401435839961148]], [[(-187380061887410), 0, 0, 0], [(-10328941408757), 0, 0], [(-23436952489044), 0], [(-177396668697304)]], [[2689704091192, 0, 0, 0, 0], [6087967190939, 0, 0, 0], [8974929393997, 0, 0], [5910851545518, 0], [2527802524549]]], r := 1110675404827, ok := true }, r0 := { p := [[[59390296229991986847]], [[(-197116166249572306), 2517249093135630195], [(-115115471277630317)]], [[5250258642655554, (-7172409944127678), 26355680636548058], [4558540330988275, (-5021007471495850)], [2147887573418657]], [[(-21699919099125), 183214439893527, (-25025567003509), (-8933094904409)], [33898788814953, 207482233880270, (-58577442945982)], [8493940649793, 90166465135206], [(-10046723907420)]], [[304564733739, (-667368697915), 279410856714, 1072083837959, (-45431847472)], [445670673787, 1108397879397, 2770344248822, (-107755508643)], [733615874937, 485799019179, 907518485135], [292135759710, (-437857487660)], [106712183749]]], r := 1100363429413, ok := true }, r1 := { p := [[[109752678914754169125]], [[(-320586919465673055), 0], [(-217973153791682255)]], [[8269172861670169, 0, 0], [8946679582647211, 0], [3937357566849426]], [[(-31994974006964), 0, 0, 0], [51153522530756, 0, 0], [20251479680483, 0], [(-19006693276050)]], [[440537014631, 0, 0, 0, 0], [753238295998, 0, 0, 0], [1288980906689, 0, 0], [574502075821, 0], [194751193255]]], r := 535746662200, ok := true }, r2 := { p := [[[60854493235461006752]], [[(-264300342881177733), 2519572787744447870], [(-480210465221484030)]], [[5502530142897703, (-7358675679076955), 25668477081396600], [17971439023727910, (-5129742768132480)], [16893748647057689]], [[(-25962083002348), 180817540980386, 11321199798775, (-12731192161984)], [(-25517955646247), 237918105828635, 93064818872614], [3171904352093, 17657259422802], [(-74909851279000)]], [[324500205086, (-627488745934), 166825415216, 1265925897605, (-40599759771)], [1276536843238, 1692687872864, (-4265642125979), 591219189178], [2466271797401, 1893924417715, (-1913431269269)], [2305662273346, (-182792157744)], [1325314416206]]], r := 4567342392541, ok := true }, r3 := { p := [[[247109844316905464544]], [[(-1536685280651665414), 10094451168804144481], [(-1786251655262875732)]], [[37173096890928169, (-32265478496857982), 96751499662559915], [73843041882549672, (-16609868190115414)], [48639854227246255]], [[(-208216027121914), 828905379346564, 671258029822697, (-162930698569600)], [(-74325149260177), 679985080151717, 547442737234872], [(-28893272245206), 110081394146419], [(-261711322106119)]], [[2901582917952, (-2189872357141), (-16334169350029), 16651606430739, (-491420500962)], [7549379096318, 9271640631507, (-22273737460157), 2757976607642], [11878963927929, 4467763383023, (-4806218079208)], [8756285923225, (-1199444853782)], [3985255266486]]], r := 61622519537346, ok := true }, eta := { p := [[[(-220410695519229415315)]], [[666719951537317226, 0], [724065092684483289]], [[(-16062009395540432), 0, 0], [(-28487787075053377), 0], [(-20230320492010753)]], [[70123440456310, 0, 0, 0], [(-36515868955533), 0, 0], [(-21509371214750), 0], [101883112877621]], [[(-948113067466), 0, 0, 0, 0], [(-2295560233819), 0, 0, 0], [(-4110420815310), 0, 0], [(-3159955970230), 0], [(-1659497506032)]]], r := 14790839812989930, ok := true } }
theorem sB_3 : stageB c3 w3 = true := by decide +kernel
theorem s0_3 : stageC0 w3 q3 = true := by decide +kernel
theorem s1_3 : stageC1 w3 q3 = true := by decide +kernel
theorem s2_3 : stageC2 w3 q3 = true := by decide +kernel
theorem s3_3 : stageC3 w3 q3 = true := by decide +kernel
theorem sE_3 : stageE w3 q3 = true := by decide +kernel
theorem sF_3 : stageF w3 = true := by decide +kernel
theorem ok_3 : (domOK c3 && cellCheck c3 q3) = true :=
  staged_check c3 q3 w3 (by decide +kernel) sB_3 s0_3 s1_3 s2_3 s3_3 sE_3 sF_3

theorem region : RegionPosI 8646911284551352320 8935141660703064064 12682136550675316736 13835058055282163712 15924728282382073856 16429131440647569408 :=
  (RegionPosI.split_s 16176929861514821632 (RegionPosI.of_check c0 q0 ok_0 8646911284551352320 8935141660703064064 12682136550675316736 13835058055282163712 15924728282382073856 16176929861514821632 (by decide +kernel)) (RegionPosI.split_t 13258597302978740224 (RegionPosI.of_check c1 q1 ok_1 8646911284551352320 8935141660703064064 12682136550675316736 13258597302978740224 16176929861514821632 16429131440647569408 (by decide +kernel)) (RegionPosI.split_b 8791026472627208192 (RegionPosI.of_check c2 q2 ok_2 8646911284551352320 8791026472627208192 13258597302978740224 13835058055282163712 16176929861514821632 16429131440647569408 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 8791026472627208192 8935141660703064064 13258597302978740224 13835058055282163712 16176929861514821632 16429131440647569408 (by decide +kernel)))))

end CKLaneC.RSC2.BD_0180