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

import Definitions.Def_CK_CKLaneC_RSC2_S03_0151_part00

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

namespace CKLaneC.RSC2.S03_0151
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c3 : Cell := { bc := 8725724278030336, bh := 281474976710656, tc := 6917529027641081856, th := 2305843009213693952, sc := 13258597302978740224, sh := 576460752303423488 }
noncomputable def q3 : Cert := { V0 := [[[178425800323233643]], [[(-22768062132005863), 59467239445940637], [654528689930999]], [[383363614054318, (-7586281131508212), (-4013025395013)], [(-82403776987481), 218087890909003], [(-8153830625989)]], [[(-7434571354509), 127344034400382, 1536048664933, (-445536860088)], [1273370878719, (-27434260273720), (-44157816969)], [1030715679185, (-2717167091946)], [158357551000]], [[156297495131, (-2447309196210), (-221807600209), 170445693771, 88677159], [(-26616608898), 419629311874, 16825239001, (-4899916209)], [(-16354424692), 343274873016, 388165018], [(-20040247608), 52772154801], [(-3595726789)]]], r0 := 4987105482453, V1 := [[[475606053633244090]], [[(-60639807930426526), 0], [1743253062656361]], [[1011478422903402, 0, 0], [(-218922141279043), 0], [(-21724581887083)]], [[(-19074426288972), 0, 0, 0], [3278098206173, 0, 0], [2741323255665, 0], [421952248881]], [[387082758975, 0, 0, 0, 0], [(-62929968891), 0, 0, 0], [(-42566693250), 0, 0], [(-53312676203), 0], [(-9581446664)]]], r1 := 1816427094904, V2 := [[[18431771148440442974]], [[(-278725709862972), 280881307854], [(-482937284564135)]], [[429338869229, (-25907470212), (-5008077)], [(-9012090939077), 18251929668], [650889855]], [[(-7923382584), (-596397745), 1017546, 87], [15641322159, (-1682582927), (-488521)], [(-369845229), 299145267], [(-17033689)]], [[190848764, 959189, (-40515), (-27), 0], [(-283725761), (-38884400), 99236, 11], [37181883, (-27545386), (-15963)], [3993418, 65289], [240371]]], r2 := 41173636360, V3 := [[[18434198497710863126]], [[(-545200378142813), 469553380228], [(-404772784288168)]], [[11455661480, (-31492705597), (-16718170)], [(-17581969685253), 30509204026], [(-2498456807)]], [[4437207, (-2290923621), 2972599, 584], [745027468, (-2044720382), (-1630521)], [167044415, 499957599], [(-529032)]], [[(-53181), (-842093), (-41800), (-168), 0], [318520, (-148985248), 289819, 76], [12233294, (-33456171), (-53266)], [31106, 108751], [2977]]], r3 := 248512234561, Vm := [[[18431772576378515643]], [[(-278860433767136), 0], [(-482844401961193)]], [[426638904976, 0, 0], [(-9020861296782), 0], [2176604233]], [[(-7918328061), 0, 0, 0], [15466286159, 0, 0], [(-514166804), 0], [(-16655458)]], [[190775490, 0, 0, 0, 0], [(-283373145), 0, 0, 0], [34328061, 0, 0], [3954036, 0], [238244]]], rm := 5195967830 }
noncomputable def w3 : Wit := { Z0 := { p := [[[178437842753535343]], [[(-22772672417989140), 59479280917845114], [654661224901581]], [[384029619023634, (-7590890805996380), 0], [(-82454291849959), 218220408300527], [(-8154995436088)]], [[(-7480931294704), 128009873007878, 0, 0], [1280616899180, (-27484763949987), 0], [1031161295669, (-2718331812030)], [158378096567]], [[158146416776, (-2493643764902), 0, 0, 0], [(-27115333583), 426872299726, 0, 0], [(-16418723923), 343720431889, 0], [(-20048111490), 52792698855], [(-3596166365)]]], r := 1191737726736, ok := true }, Z1 := { p := [[[475834247342760916]], [[(-60727126447971039), 0], [1745763266404216]], [[1024078984063024, 0, 0], [(-219878111599891), 0], [(-21746654496235)]], [[(-19949150119210), 0, 0, 0], [3414978397815, 0, 0], [2749763455117, 0], [422341590846]], [[421723778070, 0, 0, 0, 0], [(-72307556219), 0, 0, 0], [(-43783263794), 0, 0], [(-53461630640), 0], [(-9589776971)]]], r := 452669919097, ok := true }, Z2 := { p := [[[3573485564497368958233]], [[(-59022812598760303785), 59479280917845114], [(-102266550358043506884)]], [[1135209402969371830, (-7590890805996380), 0], [1710416051667025139, 218220408300527], [3135225614598828660]], [[(-23725166892237490), 128009873007878, 0, 0], [(-32610196791549162), (-27484763949987), 0], [(-52666195066667674), (-2718331812030)], [(-97959825687318840)]], [[531820869942333, (-2493643764902), 0, 0, 0], [670614515477789, 426872299726, 0, 0], [1001295185990123, 343720431889, 0], [1649772844411472, 52792698855], [3087883976918722]]], r := 1430518725739903, ok := true }, Z3 := { p := [[[4181481984490519479292]], [[(-161615643089949726646), 139191340565625466], [(-119988203348064851360)]], [[6684655363397010038, (-20843950790559251), 0], [4708842480437800132, 499731485499104], [3681978972303765520]], [[(-281668136905062503), 820039123593697, 0, 0], [(-195798241825818201), (-72413050221518), 0], [(-145264821045057421), (-6264654532932)], [(-115106854376476713)]], [[11971679339153778, (-34090933127117), 0, 0, 0], [8276023544071378, 2540620989705, 0, 0], [6052186674319374, 916527853409, 0], [4555499880176815, 121883037267], [3629797528640322]]], r := 12188744828443775, ok := true }, iE := { p := [[[3576690836857941722738]], [[(-59055909469602742044), 0], [(-102254790702707311814)]], [[1135899985763637771, 0, 0], [1710314296783175504, 0], [3135079126717847083]], [[(-23740145204758323), 0, 0, 0], [(-32607660803808279), 0, 0], [(-52664854896328913), 0], [(-97956980747436057)]], [[532166176634556, 0, 0, 0, 0], [670551510927155, 0, 0, 0], [1001263738353119, 0, 0], [1649746422925011, 0], [3087819379115517]]], r := 1430451713001733, ok := true }, iHu := { p := [[[4185023630822689282819]], [[(-161706092465190992032), 0], [(-119975487958044929712)]], [[6688522889140344874, 0, 0], [4708579368879543629, 0], [3681819571649538715]], [[(-281832490301950698), 0, 0, 0], [(-195786969437182469), 0, 0], [(-145261299904990181), 0], [(-115103753130306227)]], [[11978691982107520, 0, 0, 0, 0], [8275554563052564, 0, 0, 0], [6052037022796642, 0, 0], [4555430139232191, 0], [3629727036941152]]], r := 12189802902472354, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[95138881844165870]], [[1570869121627536, 0], [2719946144188132]], [[(-4277459415633), 0, 0], [44325999629303, 0], [(-5631014765039)]], [[61971081876, 0, 0, 0], [(-138029489736), 0, 0], [(-102408976256), 0], [60523262516]], [[(-1347197587), 0, 0, 0, 0], [1999066695, 0, 0, 0], [(-1514319), 0, 0], [1100422770, 0], [(-976181826)]]], r := 1907940849, ok := true }, de := { p := [[[(-106269397424497666510)]], [[578740810865480996, 0], [429388343545356868]], [[(-12577043061154726), 0, 0], [6349356527858, 0], [(-6923263037826067)]], [[364552014968570, 0, 0, 0], [93887804, 0, 0], [69658693, 0], [148887394384968]], [[(-11887565705029), 0, 0, 0, 0], [1389, 0, 0, 0], [1515865, 0, 0], [765, 0], [(-3602114380139)]]], r := 2641657503369, ok := true }, dde := { p := [[[(-39151853193166619374316)]], [[1701675549018500390917, 0], [1262533471852435772803]], [[(-73985901996325855171), 0, 0], [(-54892772348789968093), 0], [(-40726890901203304376)]], [[3216778347539758975, 0, 0, 0], [2386641999599721873, 0, 0], [1770734386799793770, 0], [1313770674180668779]], [[(-139859928153899578), 0, 0, 0, 0], [(-103767043469027008), 0, 0, 0], [(-76988451609085286), 0, 0], [(-57120464094813180), 0], [(-42379699167116909)]]], r := 20595750326177121, ok := true }, nJu := { p := [[[(-212538794848995333020)]], [[1157481621730961993, 0], [858776687090713737]], [[(-25154086122309451), 0, 0], [12698713055717, 0], [(-13846526075652134)]], [[729104029937141, 0, 0, 0], [187775608, 0, 0], [139317386, 0], [297774788769937]], [[(-23775131410058), 0, 0, 0, 0], [2778, 0, 0, 0], [3031730, 0, 0], [1530, 0], [(-7204228760278)]]], r := 5283315006732, ok := true }, Jd1 := { p := [[[(-78303706386333238748632)]], [[3403351098037000781834, 0], [2525066943704871545606]], [[(-147971803992651710341), 0, 0], [(-109785544697579936186), 0], [(-81453781802406608752)]], [[6433556695079517951, 0, 0, 0], [4773283999199443747, 0, 0], [3541468773599587541, 0], [2627541348361337558]], [[(-279719856307799156), 0, 0, 0, 0], [(-207534086938054016), 0, 0, 0], [(-153976903218170571), 0, 0], [(-114240928189626359), 0], [(-84759398334233818)]]], r := 41191500652354235, ok := true }, term0 := { p := [[[115290409800466158051077858]], [[(-10020142209864326646881062), 0], [(-7432542490622932924665521)]], [[653376556662832910110251, 0, 0], [646143364480587830023461, 0], [359549730725182108763917]], [[(-37873685057177514863922), 0, 0, 0], [(-42136204674136040398667), 0, 0], [(-31259881772940056286527), 0], [(-15462581491694729396072)]], [[2058247553813504486700, 0, 0, 0, 0], [2442574764790586257475, 0, 0, 0], [2038572459036164367418, 0, 0], [1344400942233335313606, 0], [623444663641924809844]]], r := 557310420662797162099, ok := true }, r0 := { p := [[[3839019100611691051256]], [[(-197977274021528999201), 2558789458665296761886], [(-110090014710260439561)]], [[7791591972240170307, (-131814300735569461246), 426093926728603649305], [5719518829343075200, (-73381461761321951012)], [3378778946378620209]], [[(-276881335124931213), 5174563849181120167, (-21855401145165918945), (-123601547868943000)], [(-222708024640934390), 3809358079951139583, (-12222323957835333899)], [(-175977580832451745), 2252189792277157259], [(-105635787877870997)]], [[9501231731517519, (-183329539350618253), 849218759924796221, 37849605786092374, (-10275359872314233)], [7779490291548964, (-148044854223461733), 632457403386458385, 2639056322877806], [6827938852639961, (-117216954332969631), 375145327071359909], [5509978886844991, (-70414178613556558)], [3331289415130863]]], r := 172328968962238020, ok := true }, r1 := { p := [[[27263461996731995634422]], [[(-1396751021888814528708), 0], [(-782088583454617968636)]], [[54121340002600935834, 0, 0], [40434337449456551102, 0], [24005412689141944411]], [[(-1887898666354641585), 0, 0, 0], [(-1555958142395444432), 0, 0], [(-1244794952894794656), 0], [(-750557364056884024)]], [[63656732354904186, 0, 0, 0, 0], [53561182596450914, 0, 0, 0], [47783084345772961, 0, 0], [38988034661636580, 0], [23670154702914616]]], r := 53014307100947448, ok := true }, r2 := { p := [[[49174426432792986520821929]], [[(-2346999951660736472071803), 9057004492045103557502], [(-3137223734305349812877168)]], [[91977973764826063825049, (-307802983525771172167), 460124285454568734], [148049686320293739095943, (-291859299565049362746)], [150795694422078443068048]], [[(-3487962002709739908112), 10086937821639533181, 321436318462170, (-7875384599375)], [(-5736205360136133306782), 9704216966856656743, 155387677666590], [(-7067346728091135995709), 9410016344202578978], [(-6455823038042406040486)]], [[133769777653849245002, (-337443505165015517), (-6363070689674), 809977459071, (-24068584631)], [215343741155787241585, (-310482241010823148), 2245980297063, (-302312326162)], [271903087572793974943, (-310254063369668662), (-2005267513114)], [301088299563951127098, (-303442595176128134)], [259399710969679889057]]], r := 1961728043225040699555, ok := true }, r3 := { p := [[[230163008045936825196597701]], [[(-20011504141780403800274650), 46105658107736180847013], [(-14851584791098804595477022)]], [[1305040453392129745407583, (-3181363196406949716275), 1827960944415676751], [1291357092295919343330485, (-1492399891718147570008)], [718663685603021366743146]], [[(-75652848477536971144232), 189413983538416158690, 3320625264066968, (-62593815556007)], [(-84217099236453569980594), 102872064583187650536, 535121267892428], [(-62489761350489876210871), 48199044657787890444], [(-30911100486717475173486)]], [[4111513315015308454366, (-10456818554593930292), (-130272086324448), 6310055508136, (-184209305854)], [4882097287097274215434, (-6122707905293261570), 21828985420515, (-2181902995785)], [4075359995420258026786, (-3321240735795922625), (-6807405794729)], [2687833811547423620648, (-1555850904236754392)], [1246435583630394488700]]], r := 62928853868646041330995, ok := true }, eta := { p := [[[(-49271635734464719627491065)]], [[2351704316841109461215175, 0], [3140329008862589714931311]], [[(-92183416782936819136136), 0, 0], [(-148198898592528639709274), 0], [(-150895509374295730351400)]], [[3496728186514969489608, 0, 0, 0], [5742685326638563459306, 0, 0], [7072128658923520743477, 0], [6459036012569784620857]], [[(-134143120471280851297), 0, 0, 0, 0], [(-215619282282503018045), 0, 0, 0], [(-272110306060444765511), 0, 0], [(-301241948536079775089), 0], [(-259503200097791821511)]]], r := 214771643033046382063, 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 7881299347898368 9007199254740992 4611686018427387904 9223372036854775808 11529215046068469760 13835058055282163712 :=
  (RegionPosI.split_s 12682136550675316736 (RegionPosI.split_b 8444249301319680 (RegionPosI.of_check c0 q0 ok_0 7881299347898368 8444249301319680 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 8444249301319680 9007199254740992 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel))) (RegionPosI.split_b 8444249301319680 (RegionPosI.of_check c2 q2 ok_2 7881299347898368 8444249301319680 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 8444249301319680 9007199254740992 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel))))

end CKLaneC.RSC2.S03_0151