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

import Definitions.Def_CK_CKLaneC_RSC2_BD_0097_part00

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

namespace CKLaneC.RSC2.BD_0097
open CKLaneC.TM3 CKLaneC.RSCell

theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

noncomputable def c5 : Cell := { bc := 8791026472627208192, bh := 144115188075855872, tc := 15564440312192434176, th := 576460752303423488, sc := 3819052484010180608, sh := 504403158265495552 }
noncomputable def q5 : Cert := { V0 := [[[7146271563252896444]], [[(-357631458360262304), 210560821847100702], [69033258910010557]], [[8876892000253711, (-5426615087005696), (-2301774446344749)], [(-2412737458230204), 1047494328445964], [227387173409965]], [[(-432132190913580), (-219673297647042), 267961878282434, 4245094442513], [36908141494076, 100196772357875, (-51724425491814)], [6353197202438, (-9753550808987)], [3319721818859]], [[26669465541776, 14627489268430, (-11327357900243), (-3425563807955), 386293576159], [(-2613575170757), (-9697658284969), 3613066508998, 661233310827], [(-569413054256), 1871585148310, (-344609624366)], [14064824876, (-62451192813)], [7544601660]]], r0 := 417047183387700, V1 := [[[8142280428908927910]], [[(-378508514006566306), 0], [73063137026208570]], [[7551888136397167, 0, 0], [(-1842000750770066), 0], [171983066043095]], [[(-358552635718424), 0, 0, 0], [(-7699603765333), 0, 0], [14685055413619, 0], [3008544918299]], [[22665371521667, 0, 0, 0, 0], [(-993103669420), 0, 0, 0], [(-715866284119), 0, 0], [46682101923, 0], [910845366]]], r1 := 343396463577348, V2 := [[[7946141933895144115]], [[(-348811669378768700), 192576048747562737], [(-194910521480628297)]], [[8247876967501198, (-4074741979802419), (-2219274010825166)], [(-5438719739550681), 6830756386925496], [(-638985185739591)]], [[(-396503317443573), (-247065390209162), 228991416617248, 9242268484312], [239771481317714, (-314068002720533), (-81959097156862)], [32615181585724, 61365251510610], [(-5514117603819)]], [[24599245660176, 14126985587712, (-7479260547765), (-3534132862732), 247052940894], [(-13745463754573), (-2110932212908), 15409917896317, (-663511544583)], [1753466151384, (-9763764966584), 374358778580], [798070540437, (-230617745625)], [(-30070124731)]]], r2 := 536154268335152, V3 := [[[14135879392508994745]], [[(-545866598921886701), 154866218122807161], [(-83762070721160707)]], [[3644660012249869, 13998789614044883, (-4709168512830282)], [(-10042894279620445), 5912732202945260], [(-242288838373211)]], [[25049359704284, (-954754542392792), (-183849971430201), 127803582832861], [158583279543687, 463860590931577, (-257162032038723)], [(-14828083714532), 68023230922921], [(-309328161486)]], [[(-3178480194158), 263042799755, 53681402838554, (-3936122725205), (-3092046976814)], [652833807898, (-45786811068234), (-4149683047470), 8716353994048], [2597784441536, 2564774124432, (-4817569655215)], [126796813180, 163437818197], [3514236148]]], r3 := 20222224625378504, Vm := [[[10888046314426753657]], [[(-392131273745182969), 0], [(-58642501414621512)]], [[3553889332234396, 0, 0], [(-6025866126425446), 0], [1653294047318964]], [[(-217094384999664), 0, 0, 0], [26186492321326, 0, 0], [73631843164755, 0], [10512891888100]], [[16142994650922, 0, 0, 0, 0], [(-3246318543067), 0, 0, 0], [811648307076, 0, 0], [1753805891643, 0], [(-51462401924)]]], rm := 933562964101270 }
noncomputable def w5 : Wit := { Z0 := { p := [[[8039852244541579583]], [[(-505757637573056454), 297772305353391836], [97625913839842223]], [[21944019041316790, (-18731764354557647), 0], [(-7037315222055745), 3615774586660823], [671457575374797]], [[(-1396572818768696), 812741445974695, 0, 0], [453779801948219, (-260641304520584), 0], [(-63104609916812), 24868799087955], [9296130661791]], [[98879039775051, (-51724919213656), 0, 0, 0], [(-35679573468922), 16806659331415, 0, 0], [5940468645071, (-2337207774697), 0], [(-902813793634), 344301135621], [83178372470]]], r := 77868388146018, ok := true }, Z1 := { p := [[[9528713771308538765]], [[(-599416459345844686), 0], [115704786773146339]], [[26007726271190269, 0, 0], [(-8340521744658661), 0], [795801570814574]], [[(-1655197414836973), 0, 0, 0], [537813098605297, 0, 0], [(-74790648790295), 0], [11017636339900]], [[117189973066727, 0, 0, 0, 0], [(-42286901889092), 0, 0, 0], [7040555431195, 0, 0], [(-1070001533196), 0], [98581774779]]], r := 82945257380236, ok := true }, Z2 := { p := [[[9221803657989848625]], [[(-539352923692155748), 297772305353391836], [(-301382003091145234)]], [[24011585897465773, (-18731764354557647), 0], [4172190409217789, 3615774586660823], [2527236265668806]], [[(-1530589792168840), 812741445974695, 0, 0], [(-221201955418317), (-260641304520584), 0], [(-72851752304485), 24868799087955], [(-52663845835719)]], [[108794129090130, (-51724919213656), 0, 0, 0], [7603120409189, 16806659331415, 0, 0], [1642624263353, (-2337207774697), 0], [1129125203214, 344301135621], [655597578561]]], r := 89300381578853, ok := true }, Z3 := { p := [[[27172523578083671902]], [[(-3304392640932892621), 937479582932572458], [(-507052035473435258)]], [[376230627689507681, (-116218400156259273), 0], [47898117292293287, 4955753225435520], [6872632050020371]], [[(-46618282263344186), 13178416137870331, 0, 0], [(-6086799587786667), (-368094373606307), 0], [(-745312033785368), (-12238800423356)], [(-105525520032698)]], [[5882027059865690, (-1632663561873369), 0, 0, 0], [759750665679495, 36771395657088, 0, 0], [90011584274368, 2525658137135, 0], [11448526362248, 153914146283], [1648720354745]]], r := 2347959756654029, ok := true }, iE := { p := [[[25214963486896406225]], [[(-716699437207451602), 0], [(-107181065562263685)]], [[44108092931178303, 0, 0], [236307731351525, 0], [3862923538850966]], [[(-2859028765869724), 0, 0, 0], [303086819906657, 0, 0], [(-129169793819851), 0], [(-34171652329878)]], [[211521905388367, 0, 0, 0, 0], [(-29645452556877), 0, 0, 0], [9341593158907, 0, 0], [291433992796, 0], [821058953318]]], r := 194653543375712, ok := true }, iHu := { p := [[[39692263229956597694]], [[(-3551911183229701551), 0], [(-440869537965279126)]], [[435485695296186512, 0, 0], [49878467022922392, 0], [6709186789194183]], [[(-54109143312282399), 0, 0, 0], [(-5870150005869534), 0, 0], [(-728613466770697), 0], [(-103470045891940)]], [[6854096880101971, 0, 0, 0, 0], [741865407549610, 0, 0, 0], [90006498547187, 0, 0], [11429338886329, 0], [1626830166684]]], r := 2500224859832140, ok := true }, T := { p := [[[15564440312192434176]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[13495255192329538982]], [[383583414917092418, 0], [57364185052269804]], [[(-12704200532612946), 0, 0], [3134516739959425, 0], [(-1823630817079448)]], [[498081090628325, 0, 0, 0], [(-231063030554280), 0, 0], [(-28679954612123), 0], [1749081003667]], [[(-33334713334655), 0, 0, 0, 0], [7945535541565, 0, 0, 0], [(-414638246804), 0, 0], [122410638661, 0], [(-74882374546)]]], r := 87278241832604, ok := true }, de := { p := [[[(-29436209227173967919)]], [[1949841887834478003, 0], [242017845562593289]], [[(-114668298672428007), 0, 0], [3498954462679104, 0], [(-1766604604702764)]], [[10232429850585133, 0, 0, 0], [50585866110174, 0, 0], [6278807737329, 0], [19566933080341]], [[(-1012116717612885), 0, 0, 0, 0], [731341284207, 0, 0, 0], [550801319626, 0, 0], [11267201967, 0], [(-240227419780)]]], r := 616218061360142, ok := true }, dde := { p := [[[(-149630957799906733502)]], [[17599301222005250143, 0], [2184456591958497099]], [[(-2355711438013866393), 0, 0], [(-296277058256283572), 0], [(-36292599802450223)]], [[310679537262192103, 0, 0, 0], [38449850802094648, 0, 0], [4772463916887634, 0], [594096006892555]], [[(-41039683529751822), 0, 0, 0, 0], [(-5096352753633138), 0, 0, 0], [(-633689850366516), 0, 0], [(-78515512534780), 0], [(-9740830391720)]]], r := 9161693067256682, ok := true }, nJu := { p := [[[(-58872418454347935837)]], [[3899683775668956007, 0], [484035691125186579]], [[(-229336597344856013), 0, 0], [6997908925358209, 0], [(-3533209209405527)]], [[20464859701170267, 0, 0, 0], [101171732220349, 0, 0], [12557615474658, 0], [39133866160683]], [[(-2024233435225769), 0, 0, 0, 0], [1462682568414, 0, 0, 0], [1101602639253, 0, 0], [22534403934, 0], [(-480454839559)]]], r := 1232436122720272, ok := true }, Jd1 := { p := [[[(-299261915599813467004)]], [[35198602444010500286, 0], [4368913183916994199]], [[(-4711422876027732785), 0, 0], [(-592554116512567144), 0], [(-72585199604900446)]], [[621359074524384206, 0, 0, 0], [76899701604189297, 0, 0], [9544927833775268, 0], [1188192013785111]], [[(-82079367059503643), 0, 0, 0, 0], [(-10192705507266276), 0, 0, 0], [(-1267379700733032), 0, 0], [(-157031025069560), 0], [(-19481660783440)]]], r := 18323386134513358, ok := true }, term0 := { p := [[[2492232978118581154395]], [[(-585235383033487166984), 0], [(-62089119878083081780)]], [[112708616171772257197, 0, 0], [15560518446628453094, 0], [1385813102932412752]], [[(-19532513034094002596), 0, 0, 0], [(-3019079769083773502), 0, 0], [(-351681653292983190), 0], [(-28742201641576174)]], [[3194007336967626286, 0, 0, 0, 0], [526749755940741889, 0, 0, 0], [68741983485013186, 0, 0], [7356731162431217, 0], [569902233531768]]], r := 839881421962025327, ok := true }, r0 := { p := [[[310694525573790795446]], [[(-41845516832018995463), 17154438440850413509], [(-1431784429840123115)]], [[5221376117629289677, (-1901715538477093180), 20966099611117694], [26246989826116487, (-162280821908079000)], [46225945264922493]], [[(-634394567214946817), 228442635127639433, 14472925254917127, (-4100777603180274)], [10735346966639769, 12965595438644859, (-3690876626758960)], [(-6137133454753704), 2728335952705794], [(-435405530615299)]], [[77955432534750242, (-27975117849030585), (-1266050924173223), 155956843913684, 116036846628180], [(-2336201432178445), (-830775381901087), 157947140370602, 95637084393174], [765721245681022, (-318776134965852), 45001210319252], [24402643682424, (-36142105096582)], [9953946877734]]], r := 243756217584726048, ok := true }, r1 := { p := [[[396546822520665831610]], [[(-50984987245504661217), 0], [(-2323180918696415953)]], [[6335479777195134989, 0, 0], [92366639698526715, 0], [61029759933672320]], [[(-772297635081313868), 0, 0, 0], [6790103664937238, 0, 0], [(-7871980469064068), 0], [(-627574254602651)]], [[95303924922462749, 0, 0, 0, 0], [(-2075306000882268), 0, 0, 0], [960378767444794, 0, 0], [38270886371199, 0], [13497221681007]]], r := 221135719162024268, ok := true }, r2 := { p := [[[339134566985458165923]], [[(-46325685183934800109), 16676326761153984541], [(-11464728061142967143)]], [[5809166243909513672, (-1839904359710210392), 2946370642551896], [1593686967712411238, (-636377549230526)], [244211356159462177]], [[(-710870142980945336), 223597648959223992, 13418956747684183, (-2875096162675252)], [(-194814374839130124), (-6936640283383879), 1877864758784854], [(-32874048860250755), 2020926811105808], [(-5258472753916473)]], [[87835137430901684, (-27590098328047405), (-1029058220367145), (-3179680313079), 91389879723139], [24364325602061313, 695848405011846, 506348947028892, (-273259994570153)], [4235388000986087, (-544482721327264), 172927221602802], [743870236323119, (-50355304301781)], [103302832623933]]], r := 372090297941302440, ok := true }, r3 := { p := [[[2883891950063516010053]], [[(-682827241126750690847), 97254825622911105127], [(-90490594959013712136)]], [[130797472311347396901, (-21693682023521047359), (-239560877325367306)], [22924693752966132841, (-1510551802176193575)], [2220916721066727823]], [[(-22649356467391093568), 4336839633965371210, (-13023290756642811), 9474703221787317], [(-4479960925756875669), 397453331595159549, (-11343439286756801)], [(-570761526818231519), 26386430567297258], [(-48491184349056242)]], [[3702484931220658431, (-758971984888115736), 2231418558336616, (-98922847088653), (-321831893547507)], [783558319973181778, (-73537752091739144), (-1173589950623552), 689180350642679], [111950845018064882, (-6000859982239626), (-203629773957698)], [12526865942758694, (-403747387279405)], [991631766316785]]], r := 323736411354068583230, ok := true }, eta := { p := [[[(-858468926857515943825)]], [[122722736768102004389, 0], [15725384781839345851]], [[(-16662782501219243354), 0, 0], [(-2219594858795917142), 0], [(-351189703951742161)]], [[2172776992980854640, 0, 0, 0], [276754094570664698, 0, 0], [50488151834887631, 0], [6534872223960813]], [[(-281767690919368163), 0, 0, 0, 0], [(-34912598045774575), 0, 0, 0], [(-6590199034764440), 0, 0], [(-901577748540310), 0], [(-127293192149781)]]], r := 539746754406758719, ok := true } }
theorem sB_5 : stageB c5 w5 = true := by decide +kernel
theorem s0_5 : stageC0 w5 q5 = true := by decide +kernel
theorem s1_5 : stageC1 w5 q5 = true := by decide +kernel
theorem s2_5 : stageC2 w5 q5 = true := by decide +kernel
theorem s3_5 : stageC3 w5 q5 = true := by decide +kernel
theorem sE_5 : stageE w5 q5 = true := by decide +kernel
theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

theorem region : RegionPosI 8646911284551352320 8935141660703064064 13835058055282163712 16140901064495857664 2305843009213693952 4323455642275676160 :=
  (RegionPosI.split_t 14987979559889010688 (RegionPosI.split_s 3314649325744685056 (RegionPosI.split_s 2810246167479189504 (RegionPosI.of_check c0 q0 ok_0 8646911284551352320 8935141660703064064 13835058055282163712 14987979559889010688 2305843009213693952 2810246167479189504 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 8646911284551352320 8935141660703064064 13835058055282163712 14987979559889010688 2810246167479189504 3314649325744685056 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 8646911284551352320 8935141660703064064 13835058055282163712 14987979559889010688 3314649325744685056 4323455642275676160 (by decide +kernel))) (RegionPosI.split_s 3314649325744685056 (RegionPosI.split_s 2810246167479189504 (RegionPosI.of_check c3 q3 ok_3 8646911284551352320 8935141660703064064 14987979559889010688 16140901064495857664 2305843009213693952 2810246167479189504 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 8646911284551352320 8935141660703064064 14987979559889010688 16140901064495857664 2810246167479189504 3314649325744685056 (by decide +kernel))) (RegionPosI.of_check c5 q5 ok_5 8646911284551352320 8935141660703064064 14987979559889010688 16140901064495857664 3314649325744685056 4323455642275676160 (by decide +kernel))))

end CKLaneC.RSC2.BD_0097