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

import Definitions.Def_CK_CKLaneC_RSC2_S02_0131_part00

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

namespace CKLaneC.RSC2.S02_0131
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c7 : Cell := { bc := 2744381022928896, bh := 70368744177664, tc := 2305843009213693952, th := 2305843009213693952, sc := 7782220156096217088, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[129074295427409796]], [[(-4851186760594313), 129065178549627262], [328685709877935]], [[53818224286447, (-4850158815025660), (-13674177567776)], [(-12210739949154), 328616062792464], [(-3376696086530)]], [[(-698111688986), 53768186888205, 1541704293666, (-4556160849406)], [136789987966, (-12202917416549), (-104456124903)], [125810663932, (-3376157928799)], [52700253394]], [[10258125448, (-696622628733), (-75037632557), 513544710473, 1423457085], [(-2042823142), 136410071755, 11731079784, (-34794539162)], [(-1405882442), 125750064885, 807161461], [(-1965333421), 52692579859], [(-957321041)]]], r0 := 1647711922966, V1 := [[[1030305910104663065]], [[(-38552139882353627), 0], [2612048987162175]], [[418081568940329, 0, 0], [(-95736028229387), 0], [(-26878547366144)]], [[(-5217421341915), 0, 0, 0], [1000415210720, 0, 0], [991326026375, 0], [419676174289]], [[73758599045, 0, 0, 0, 0], [(-13578099878), 0, 0, 0], [(-10513913453), 0, 0], [(-15506288210), 0], [(-7625458008)]]], r1 := 601789858809, V2 := [[[18442877837778383317]], [[(-45274239815307), 46105527911], [(-99041278551285)]], [[57824110057, (-700504852), (-525713)], [(-1167326512622), 2376028810], [1365571866]], [[(-883249211), (-15402453), 22155, 6], [1637557726, (-35981414), (-40665)], [(-98986378), 30794380], [(-10352169)]], [[17544660, 28169, (-38), (-1), 0], [(-24858075), (-798669), 1712, 0], [2420271, (-462961), (-1052)], [672161, 3529], [119162]]], r2 := 2308111261, V3 := [[[18444428117612115897]], [[(-85765893014221), 54952934074], [(-59393448396169)]], [[385659188, 569291635, (-1249156)], [(-2199229323069), 2832175584], [(-256866857)]], [[110988, (-55105446), 20544, 28], [19876972, 29427125, (-96608)], [(-2689345), 36712751], [(-29065)]], [[(-1293), (-15622), 1611, (-2), 0], [6270, (-2840440), 1585, 3], [257668, 383906, (-2499)], [(-505), 4304], [137]]], r3 := 18028060830, Vm := [[[18442878168919971955]], [[(-45279600021733), 0], [(-99024190400770)]], [[57722988283, 0, 0], [(-1167603116142), 0], [1587689028]], [[(-883088894), 0, 0, 0], [1632327146, 0, 0], [(-102581453), 0], [(-10320048)]], [[17542522, 0, 0, 0, 0], [(-24849323), 0, 0, 0], [2351921, 0, 0], [671648, 0], [119010]]], rm := 265230005 }
noncomputable def w7 : Wit := { Z0 := { p := [[[129078854151098845]], [[(-4851700786899065), 129078854151098845], [328720537046877]], [[53843247602463, (-4851700786899065), 0], [(-12214651895336), 328720537046877], [(-3376965184179)]], [[(-698856467291), 53843247602463, 0, 0], [136980004619, (-12214651895336), 0], [125840966991, (-3376965184179)], [52704090412]], [[10275211213, (-698856467291), 0, 0, 0], [(-2048505775), 136980004619, 0, 0], [(-1407356491), 125840966991, 0], [(-1965765727), 52704090412], [(-957386995)]]], r := 375705848338, ok := true }, Z1 := { p := [[[1032630833208790767]], [[(-38813606295192519), 0], [2629764296375022]], [[430745980819707, 0, 0], [(-97717215162687), 0], [(-27015721473429)]], [[(-5590851738326), 0, 0, 0], [1095840036952, 0, 0], [1006727735934, 0], [421632723302]], [[82201689705, 0, 0, 0, 0], [(-16388046195), 0, 0, 0], [(-11258851923), 0, 0], [(-15726125814), 0], [(-7659095957)]]], r := 151065696968, ok := true }, Z2 := { p := [[[12002565422502437670992]], [[(-126751547216030050709), 129078854151098845], [(-277279869211294599264)]], [[1581098162245078447, (-4851700786899065), 0], [2941200175238509910, 328720537046877], [6795503886772777975]], [[(-22253151569628153), 53843247602463, 0, 0], [(-36183863733811707), (-12214651895336), 0], [(-72198558964542614), (-3376965184179)], [(-169340621076222323)]], [[354036260733494, (-698856467291), 0, 0, 0], [498307507187648, 136980004619, 0, 0], [883779226698905, 125840966991, 0], [1800886016331216, 52704090412], [4253007280916026]]], r := 1075546033741239, ok := true }, Z3 := { p := [[[19076736240832435347764]], [[(-640374674848509557778), 410308411104036964], [(-443463699474595616501)]], [[22721587635366900516, (-24862556845492035), 0], [15045072413675465512, 985477492731599], [10893188748408351165]], [[(-818986024790966670), 860942044684098, 0, 0], [(-535913074595154058), (-56294787991050), 0], [(-371012139724138756), (-10267013478614)], [(-271825478250661976)]], [[29739438529267931, (-30822696764328), 0, 0, 0], [19361911996403727, 1809126586774, 0, 0], [13235764079913431, 594725643142, 0], [9279825288831147, 160961204026], [6833524157128039]]], r := 23077298511409672, ok := true }, iE := { p := [[[12006008688152360226694]], [[(-126784419761235340504), 0], [(-277271100368860402821)]], [[1581514893039441760, 0, 0], [2941120221226362528, 0], [6795413803944756779]], [[(-22259075820743023), 0, 0, 0], [(-36182700744608564), 0, 0], [(-72197728012077329), 0], [(-169339215158999688)]], [[354131356027691, 0, 0, 0, 0], [498287996214904, 0, 0, 0], [883767543795565, 0, 0], [1800873000399887, 0], [4252981741971065]]], r := 1075427567231507, ok := true }, iHu := { p := [[[19082003713677689876361]], [[(-640540402774056859151), 0], [(-443451048074351089209)]], [[22727489175605607368, 0, 0], [15044718274579290115, 0], [10893056942154233832]], [[(-819198951782308956), 0, 0, 0], [(-535900942129085106), 0, 0], [(-371008344550817226), 0], [(-271823411856826497)]], [[29747173984884502, 0, 0, 0, 0], [19361485515775412, 0, 0, 0], [13235633136692324, 0, 0], [9279765246560288, 0], [6833486520030674]]], r := 23077542646703993, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[28342672053596982]], [[299300902084494, 0], [654555903782539]], [[(-572852055595), 0, 0], [6881202335446, 0], [(-925432382032)]], [[7071803693, 0, 0, 0], [(-14689436208), 0, 0], [(-10169609683), 0], [7908703436]], [[(-130959328), 0, 0, 0, 0], [181328299, 0, 0, 0], [(-23641), 0, 0], [86908830, 0], [(-101393634)]]], r := 151604126, ok := true }, de := { p := [[[(-128754766237599766021)]], [[492864752449680765, 0], [341214059388240530]], [[(-9126552157352297), 0, 0], [793229555301, 0], [(-4374264643464711)]], [[225346967736077, 0, 0, 0], [1844043, 0, 0], [1276645, 0], [74773754883750]], [[(-6259637992667), 0, 0, 0, 0], [4, 0, 0, 0], [23646, 0, 0], [2, 0], [(-1437956824687)]]], r := 1114385109820, ok := true }, dde := { p := [[[(-212023036170123674838404)]], [[7852212147649511545700, 0], [5436146871449661839406]], [[(-290822673281015008140), 0, 0], [(-201338774603212820555), 0], [(-139388381868415475974)]], [[10771210121516426302, 0, 0, 0], [7456991622584607083, 0, 0], [5162532661789343317, 0], [3574061073548249549]], [[(-398933708204299872), 0, 0, 0, 0], [(-276184874910668485), 0, 0, 0], [(-191204913399735636), 0, 0], [(-132372632353632804), 0], [(-91642591629434338)]]], r := 44449437416907812, ok := true }, nJu := { p := [[[(-257509532475199532041)]], [[985729504899361530, 0], [682428118776481061]], [[(-18253104314704593), 0, 0], [1586459110603, 0], [(-8748529286929421)]], [[450693935472155, 0, 0, 0], [3688086, 0, 0], [2553291, 0], [149547509767501]], [[(-12519275985333), 0, 0, 0, 0], [9, 0, 0, 0], [47293, 0, 0], [5, 0], [(-2875913649373)]]], r := 2228770219627, ok := true }, Jd1 := { p := [[[(-424046072340247349676807)]], [[15704424295299023091400, 0], [10872293742899323678812]], [[(-581645346562030016280), 0, 0], [(-402677549206425641110), 0], [(-278776763736830951947)]], [[21542420243032852605, 0, 0, 0], [14913983245169214166, 0, 0], [10325065323578686634, 0], [7148122147096499099]], [[(-797867416408599744), 0, 0, 0, 0], [(-552369749821336969), 0, 0, 0], [(-382409826799471272), 0, 0], [(-264745264707265608), 0], [(-183285183258868675)]]], r := 88898874833815618, ok := true }, term0 := { p := [[[3379042734685888841571850433]], [[(-250275900263207443044896998), 0], [(-173255045269978240860693442)]], [[13903780447291411296516537, 0, 0], [12833103040726893137168564, 0], [6663281303692688747042952]], [[(-686595670631430105296121), 0, 0, 0], [(-712938983441529727917941), 0, 0], [(-493560905268139926140571), 0], [(-227798091004571480661493)]], [[31786537403025419967801, 0, 0, 0, 0], [35206587194953448858798, 0, 0, 0], [27419763485303986786362, 0, 0], [16873535549108046389247, 0], [7301097826866207139750]]], r := 6411481399405276515763, ok := true }, r0 := { p := [[[2123510410849456705407]], [[(-74170355931199796819), 4246540181074388655922], [(-49087700904082436046)]], [[2007659718838668814, (-148288060952905284937), 2122308930021421721436], [1703924233425246689, (-98166730126799232676)], [1203464411825277676]], [[(-51553042868522281), 4012562125207449872, (-74038750935608195167), (-960919079160130038)], [(-45223984838638361), 3406899213735895241, (-49066023264810338961)], [(-41680358886714326), 2406734793409517289], [(-29996055823121663)]], [[1360970689995520, (-103005167862190097), 2000768390630282562, 105234992328786222, (-239928033899876158)], [1132491594964321, (-90398496230918113), 1701551389417006403, 17338670540754149], [1098202124608484, (-83339482036936571), 1202979368351572209], [1037469231144352, (-59987540617342468)], [753464723748335]]], r := 292534813901262282, ok := true }, r1 := { p := [[[134943302404560713594024]], [[(-4642157901829779589443), 0], [(-3124229607681004126795)]], [[123053593392686426390, 0, 0], [107155673142935956037, 0], [76632588491087282501]], [[(-3102882878245628403), 0, 0, 0], [(-2796186307520648096), 0, 0], [(-2625106048392485073), 0], [(-1910577780352413669)]], [[81123258998055721, 0, 0, 0, 0], [68961079722589735, 0, 0, 0], [68089216154003256, 0, 0], [65397948295501830, 0], [48000519631150771]]], r := 80087235706048345, ok := true }, r2 := { p := [[[822483314056511440059771178]], [[(-27736518758190671243724934), 41883589121647957481919], [(-41560540513619727948896467)]], [[831747122807240618520167, (-1005626034596056751487), 452270650164662147], [1382755106546251309570287, (-1064238902771424686545)], [1584263278205301723648568]], [[(-25834909076868559768293), 24830930606430369382, 173209792225527, (-34519846650337)], [(-40963794422813032760304), 24872042341833711998, 68265639896316], [(-52271597023325674767648), 27186627132307713580], [(-53822118541204852055244)]], [[847174200459245649773, (-674221707981222364), (-18248052122796), 1097097851176, (-3588772704555)], [1261466739783749614367, (-596882728050385218), (-17375620750924), (-29278420157792)], [1536748098061082897979, (-628429846081241304), (-12775127818604)], [1765225364518610203488, (-695509312071737451)], [1716747258429676469265]]], r := 8094555591136418074325, ok := true }, r3 := { p := [[[6754179725384879456919538639]], [[(-500305153680955248871843118), 353785928460531869228489], [(-346409824176097222326996113)]], [[27794648791155707210416223, (-22356002115467795543998), 1767692954283809473], [25659876026830972076125721, (-9088959585948584118419)], [13323990555434766029716548]], [[(-1372573211180900275374388), 1170616699068237781770, 3837936888444642, (-593469803197421)], [(-1425546620002240939065150), 574054785573153398444, (-529678853494192)], [(-986959446971132679523239), 233209427392627698962], [(-455530215713777361336738)]], [[63544998249265410544259, (-56048099626237864069), (-308206043797796), 65118760347381, (-84556190126731)], [70397312972589371129126, (-30054032970266643778), (-253354510166578), (-686406765091817)], [54831028144542047474333, (-14727424168117884615), (-331944569495564)], [33742906985434148989221, (-5982771403940491748)], [14600503812853093028582]]], r := 670275640952483550436231, ok := true }, eta := { p := [[[(-823109569827521834917188903)]], [[27759532025703188198306015, 0], [41576427079199740572155467]], [[(-832555095859466087322069), 0, 0], [(-1383334043395469916087567), 0], [(-1584668898576557637326789)]], [[25863626025545377162500, 0, 0, 0], [40984032159976602278188, 0, 0], [52286328687613576257856, 0], [53832492205528683984596]], [[(-848210476102588237228), 0, 0, 0, 0], [(-1262184936067264142131), 0, 0, 0], [(-1537262204712761330771), 0, 0], [(-1765601362788284272975), 0], [(-1717012766794756674672)]]], r := 767172932760696329360, ok := true } }
theorem sB_7 : stageB c7 w7 = true := by decide +kernel
theorem s0_7 : stageC0 w7 q7 = true := by decide +kernel
theorem s1_7 : stageC1 w7 q7 = true := by decide +kernel
theorem s2_7 : stageC2 w7 q7 = true := by decide +kernel
theorem s3_7 : stageC3 w7 q7 = true := by decide +kernel
theorem sE_7 : stageE w7 q7 = true := by decide +kernel
theorem sF_7 : stageF w7 = true := by decide +kernel
theorem ok_7 : (domOK c7 && cellCheck c7 q7) = true :=
  staged_check c7 q7 w7 (by decide +kernel) sB_7 s0_7 s1_7 s2_7 s3_7 sE_7 sF_7

theorem region : RegionPosI 2251799813685248 2814749767106560 0 4611686018427387904 6917529027641081856 8070450532247928832 :=
  (RegionPosI.split_b 2533274790395904 (RegionPosI.split_s 7493989779944505344 (RegionPosI.split_b 2392537302040576 (RegionPosI.of_check c0 q0 ok_0 2251799813685248 2392537302040576 0 4611686018427387904 6917529027641081856 7493989779944505344 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2392537302040576 2533274790395904 0 4611686018427387904 6917529027641081856 7493989779944505344 (by decide +kernel))) (RegionPosI.split_b 2392537302040576 (RegionPosI.of_check c2 q2 ok_2 2251799813685248 2392537302040576 0 4611686018427387904 7493989779944505344 8070450532247928832 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2392537302040576 2533274790395904 0 4611686018427387904 7493989779944505344 8070450532247928832 (by decide +kernel)))) (RegionPosI.split_s 7493989779944505344 (RegionPosI.split_b 2674012278751232 (RegionPosI.of_check c4 q4 ok_4 2533274790395904 2674012278751232 0 4611686018427387904 6917529027641081856 7493989779944505344 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 2674012278751232 2814749767106560 0 4611686018427387904 6917529027641081856 7493989779944505344 (by decide +kernel))) (RegionPosI.split_b 2674012278751232 (RegionPosI.of_check c6 q6 ok_6 2533274790395904 2674012278751232 0 4611686018427387904 7493989779944505344 8070450532247928832 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 2674012278751232 2814749767106560 0 4611686018427387904 7493989779944505344 8070450532247928832 (by decide +kernel)))))

end CKLaneC.RSC2.S02_0131