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

import Definitions.Def_CK_CKLaneC_RSC2_BA_0129_part00

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

namespace CKLaneC.RSC2.BA_0129
open CKLaneC.TM3 CKLaneC.RSCell

theorem s0_4 : stageC0 w4 q4 = true := by decide +kernel
theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel
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 := 2738188573441261568, bh := 144115188075855872, tc := 17293822569102704640, th := 1152921504606846976, sc := 5080060379673919488, sh := 252201579132747776 }
noncomputable def q5 : Cert := { V0 := [[[4200597134502954301]], [[(-115642464933535170), 259505070574797303], [70203463228833412]], [[1226857919595344, (-6036022668028436), (-1877663394353045)], [(-1660114421602932), 3664308743910696], [(-586286075798847)]], [[(-20668936191022), 19494355565216, 143627920029962, (-23983376781786)], [13219719003300, (-32569855943900), (-87192688328225)], [20180386454939, (-47017015765094)], [22940536741308]], [[455006708469, 220128937421, (-4717462465484), 893295030604, 698023801030], [(-292094630649), (-1807039122364), 5939488637038, (-542295642605)], [(-283218644154), 1769271771228, (-448834835963)], [(-623939000636), 1392405769085], [(-787586269491)]]], r0 := 54325174462744, V1 := [[[4458201254988877102]], [[(-121534046051882582), 0], [73780085351505317]], [[1241671387507484, 0, 0], [(-1686787996304991), 0], [(-633731141070734)]], [[(-20355434184087), 0, 0, 0], [11263846429055, 0, 0], [21948236210637, 0], [24323501393697]], [[446063744258, 0, 0, 0, 0], [(-246052436418), 0, 0, 0], [(-306140242611), 0, 0], [(-656183511766), 0], [(-838221517789)]]], r1 := 26720467027404, V2 := [[[15141910281813139203]], [[(-48119681616969923), 30465562745692174], [(-172810707714415429)]], [[236987331483988, (-134435251279157), (-243957170358938)], [(-2678982949670867), 3317063975084049], [(-17560251393970)]], [[(-4263427345777), (-10477464759808), 5986395207842, 1795697137598], [16588877234838, (-15433789327586), (-39356999264210)], [(-4979084540121), 94303695674815], [(-2793848646923)]], [[110650835703, 79580181258, 55271279641, (-82385429638), (-12291529494)], [(-290853947441), (-1180972498004), 1012740030664, 376043792778], [193411345817, (-608170401607), (-2113339329974)], [81531121869, 167188996943], [16391734029]]], r2 := 218460170546572, V3 := [[[16912039261393449744]], [[(-75749709402829943), 26983844180772805], [(-82266038670436067)]], [[24386921256798, 883636913893551, (-428339683221982)], [(-4036281952139066), 2958968181827421], [(-82098623258555)]], [[66244313557, (-25054690174282), (-6242489167442), 6476036411683], [2688832827108, 96627361023508, (-70253532287692)], [(-2686243625925), 85916470395016], [(-148784839502)]], [[(-1196129680), (-60365391064), 680028252548, (-31167183615), (-94766326071)], [8094597331, (-2799951604967), (-987406178696), 1405640658390], [80849291845, 2736440387058, (-3930593489044)], [(-1232945684), 222894904924], [1498848487]]], r3 := 1901826528172076, Vm := [[[15239899316236313491]], [[(-50227952567658446), 0], [(-160296812820917446)]], [[228790732924218, 0, 0], [(-2939260169737004), 0], [491046178736770]], [[(-3992801357300), 0, 0, 0], [14778454919046, 0, 0], [(-14431028610767), 0], [4348193357190]], [[110729507578, 0, 0, 0, 0], [(-240650325559), 0, 0, 0], [51403681101, 0, 0], [16082463299, 0], [68717067389]]], rm := 41361966269604 }
noncomputable def w5 : Wit := { Z0 := { p := [[[4365322343195616904]], [[(-129687032030734598), 291021489546374460], [78729546189273666]], [[1794015125713738, (-8645802135382307), 0], [(-2369436933480300), 5248636412618244], [(-503382467037325)]], [[(-37128386666890), 119601008380915, 0, 0], [41463125515482, (-157962462232020), 0], [13969924796400, (-33558831135822)], [24288468667006]], [[897623883982, (-2475225777793), 0, 0, 0], [(-1127104411264), 2764208367698, 0, 0], [(-51879477443), 931328319760, 0], [(-729147751504), 1619231244467], [(-796258639006)]]], r := 11456353422466, ok := true }, Z1 := { p := [[[4656343832741991364]], [[(-138332834166116905), 0], [83978182601891911]], [[1913616134094654, 0, 0], [(-2527399395712320), 0], [(-536941298173146)]], [[(-39603612444682), 0, 0, 0], [44227333883181, 0, 0], [14901253116160, 0], [25907699911473]], [[957465476247, 0, 0, 0, 0], [(-1202244705348), 0, 0, 0], [(-55338109273), 0, 0], [(-777757601604), 0], [(-849342548273)]]], r := 6817356755509, ok := true }, Z2 := { p := [[[34804295788046086769]], [[(-459661997303759772), 291021489546374460], [(-1650769755622635002)]], [[8077567555529223, (-8645802135382307), 0], [16166579114319647, 5248636412618244], [74813446440334251]], [[(-177463467995516), 119601008380915, 0, 0], [(-256065594869147), (-157962462232020), 0], [(-793451283450816), (-33558831135822)], [(-3692393163250265)]], [[4508837294223, (-2475225777793), 0, 0, 0], [4779056106743, 2764208367698, 0, 0], [11993726555862, 931328319760, 0], [39184947878159, 1619231244467], [185502747760138]]], r := 39647103302153, ok := true }, Z3 := { p := [[[67763964523115665023]], [[(-2826712728498003193), 1006942157414371167], [(-3069879217571532952)]], [[126873127121448138, (-56767864454735468), 0], [122978158755345975, 12956182937426569], [145503433425576453]], [[(-5958735950679343), 2439061030581554, 0, 0], [(-5721801367020086), (-559565460585057), 0], [(-6054525984676113), (-167031557155269)], [(-7240908882016322)]], [[284527094691463, (-113857873765442), 0, 0, 0], [271616963881881, 20022768435691, 0, 0], [280847270693737, 9783259861077, 0], [304552750126587, 5273918716013], [366447511739164]]], r := 542785758906673, ok := true }, iE := { p := [[[43290984454898446031]], [[(-469297728388302469), 0], [(-1497710463579193528)]], [[8936607900182022, 0, 0], [15933495526019869, 0], [73834813033168607]], [[(-199587671222935), 0, 0, 0], [(-224560671209650), 0, 0], [(-794254706706710), 0], [(-3645173586878594)]], [[5135947961232, 0, 0, 0, 0], [3964591153988, 0, 0, 0], [12141291442709, 0, 0], [39116609190927, 0], [183954729392591]]], r := 38081114609129, ok := true }, iHu := { p := [[[74893983519146805341]], [[(-2809165883273914564), 0], [(-2978138267230240233)]], [[128408478809208626, 0, 0], [124413758205108495, 0], [144320705930571355]], [[(-6045678711747879), 0, 0, 0], [(-5711303697296454), 0, 0], [(-6054840761795489), 0], [(-7203564988574360)]], [[289039288309167, 0, 0, 0, 0], [271119591426198, 0, 0, 0], [280843839444395, 0, 0], [304716411167611, 0], [365112554012581]]], r := 509230207727565, ok := true }, T := { p := [[[17293822569102704640]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[7860351784687468674]], [[85210472419029716, 0], [271939556551427156]], [[(-698893801956025), 0, 0], [3002896652493301, 0], [(-3998081523636725)]], [[11072685435404, 0, 0, 0], [(-38351633745929), 0, 0], [(-40658498933654), 0], [59730031441533]], [[(-275375395718), 0, 0, 0, 0], [580561435776, 0, 0, 0], [(-86029883038), 0, 0], [652503923607, 0], [(-1617567785228)]]], r := 1858804648056, ok := true }, de := { p := [[[(-41987620454537830159)]], [[688762469247970897, 0], [730191790706495461]], [[(-16368259684840799), 0, 0], [1545022959478880, 0], [(-18396595103981001)]], [[542766975453072, 0, 0, 0], [3269135555478, 0, 0], [3465775288139, 0], [646719312710179]], [[(-20207777474591), 0, 0, 0, 0], [6917209363, 0, 0, 0], [97029806198, 0, 0], [7774381782, 0], [(-25526333419328)]]], r := 9895948742186, ok := true }, dde := { p := [[[(-339389001388233237742)]], [[16130981454221452856, 0], [17101266052971615428]], [[(-802348342179531797), 0, 0], [(-852220769286299278), 0], [(-901774401654772537)]], [[39829681340595509, 0, 0, 0], [42218634710965746, 0, 0], [44758101460497517, 0], [47457979772172875]], [[(-1977366869386112), 0, 0, 0, 0], [(-2096327866024618), 0, 0, 0], [(-2222617459968632), 0, 0], [(-2356102340688314), 0], [(-2497797002354627)]]], r := 842618152430487, ok := true }, nJu := { p := [[[(-83975240909075660318)]], [[1377524938495941794, 0], [1460383581412990923]], [[(-32736519369681597), 0, 0], [3090045918957760, 0], [(-36793190207962001)]], [[1085533950906145, 0, 0, 0], [6538271110957, 0, 0], [6931550576279, 0], [1293438625420359]], [[(-40415554949181), 0, 0, 0, 0], [13834418726, 0, 0, 0], [194059612397, 0, 0], [15548763564, 0], [(-51052666838656)]]], r := 19791897484362, ok := true }, Jd1 := { p := [[[(-678778002776466475483)]], [[32261962908442905713, 0], [34202532105943230857]], [[(-1604696684359063593), 0, 0], [(-1704441538572598555), 0], [(-1803548803309545074)]], [[79659362681191018, 0, 0, 0], [84437269421931493, 0, 0], [89516202920995034, 0], [94915959544345751]], [[(-3954733738772223), 0, 0, 0, 0], [(-4192655732049236), 0, 0, 0], [(-4445234919937264), 0, 0], [(-4712204681376627), 0], [(-4995594004709253)]]], r := 1685236304860964, ok := true }, term0 := { p := [[[10189999348351546873763]], [[(-956298712782780832051), 0], [(-951722225547448973081)]], [[70025848996775713455, 0, 0], [91966870114431918612, 0], [72154312898843825184]], [[(-4595413416446433698), 0, 0, 0], [(-6784357884682904117), 0, 0], [(-7029913689987029996), 0], [(-4958551536150903928)]], [[283693430517922437, 0, 0, 0, 0], [446990719685947405, 0, 0, 0], [520175224181059038, 0, 0], [485270297669072707, 0], [322079642541493774]]], r := 218202785472611073, ok := true }, r0 := { p := [[[533912342321739787795]], [[(-23579203082356219158), 63564732867112233350], [(-19261059168486416933)]], [[986417626938534933, (-2439464428473003813), 1228667955255638966], [769706011877212593, (-2522498936834834056)], [938321383081293382]], [[(-41610089065608091), 95122810482137460, (-5509337428397070), (-44592369395967372)], [(-27261895661291709), 97350458677130585, (-74803444272507254)], [(-37886314595361042), 120762647503028388], [(-46407006489259989)]], [[1819941346381229, (-3981156194472215), (-355579453809210), 3046361987474533, 241488756089146], [1008561441053228, (-3363973453497256), 2131169924277278, 925560759013666], [1358399815870104, (-4644340751340573), 3485526565958152], [1853807558200591, (-6000752867063968)], [2341282176084184]]], r := 36811299957243320, ok := true }, r1 := { p := [[[598661412349034437792]], [[(-26021202464287668904), 0], [(-21857408189934672919)]], [[1081092449469944557, 0, 0], [869078463244829748, 0], [1062536154192018504]], [[(-45582841922232563), 0, 0, 0], [(-30668902249070113), 0, 0], [(-42632589899259547), 0], [(-52581269786082501)]], [[1997412604252473, 0, 0, 0, 0], [1135831831968236, 0, 0, 0], [1521649632901486, 0, 0], [2088203820797811, 0], [2653262810242144]]], r := 14289140051541297, ok := true }, r2 := { p := [[[2302310965002068433562]], [[(-122054437687906109308), 43586272591731253096], [(-217941100865981197154)]], [[5773583992536710006, (-1754170077929994198), 98633635075784797], [11444955905567753824, (-1591049479235045562)], [16200776534651473385]], [[(-270259023317795344), 76898811960790543, 2244018723629517, (-995735396877348)], [(-535024144149018427), 64082868502506006, (-1890694151481141)], [(-839086748013045908), 87791125720165466], [(-1091620360628064892)]], [[12764561041253501, (-3434968296216559), (-25813268468402), (-4524564559029), 9808341308811], [24918885777605249, (-2474034307779544), 153436760370646, (-61903403109372)], [38839690898003978, (-3267416743328148), (-42362582122725)], [55906158845728410, (-4526195445011340)], [69690834538480961]]], r := 1597535608458621015, ok := true }, r3 := { p := [[[16943056920103561847165]], [[(-1613858735193730919657), 369333854450045527406], [(-1725552781943341515079)]], [[118662931966990661678, (-31865975514497802089), 170950067915229646], [168148198990965877115, (-19136388128634501100)], [134944129105747164741]], [[(-7804286074196732293), 2304451320724160762, 11134650576224456, (-3170717422874936)], [(-12441583691931226522), 1721827229678249329, (-14836750055136059)], [(-13229633064768576846), 1013135467336510642], [(-9424028491602299174)]], [[482429775668550851, (-149867131345306728), (-316918157079089), (-86197915860403), 51487856501461], [820923248020229918, (-122761469171784958), 42383751987930, 47417066237608], [981003903385645128, (-90436641008107106), (-114446324859602)], [926836329964793070, (-53494548798669535)], [618202213615061266]]], r := 267818873480420067241, ok := true }, eta := { p := [[[(-3112599438199377652072)]], [[169270582406045186955, 0], [254142850775386427138]], [[(-8274972179184915892), 0, 0], [(-13611142746870679887), 0], [(-18074527415035569890)]], [[396924296930043703, 0, 0, 0], [646780598416628931, 0, 0], [950724721430716329, 0], [1188644103203804289]], [[(-19093194529545396), 0, 0, 0, 0], [(-30522939700519752), 0, 0, 0], [(-44617258935073616), 0, 0], [(-61678488173460563), 0], [(-74748871720028004)]]], r := 166401623190478576, 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 2305843009213693952 2882303761517117440 16140901064495857664 18446744073709551616 4323455642275676160 5332261958806667264 :=
  (RegionPosI.split_s 4827858800541171712 (RegionPosI.split_s 4575657221408423936 (RegionPosI.split_b 2594073385365405696 (RegionPosI.of_check c0 q0 ok_0 2305843009213693952 2594073385365405696 16140901064495857664 18446744073709551616 4323455642275676160 4575657221408423936 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2594073385365405696 2882303761517117440 16140901064495857664 18446744073709551616 4323455642275676160 4575657221408423936 (by decide +kernel))) (RegionPosI.split_b 2594073385365405696 (RegionPosI.of_check c2 q2 ok_2 2305843009213693952 2594073385365405696 16140901064495857664 18446744073709551616 4575657221408423936 4827858800541171712 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2594073385365405696 2882303761517117440 16140901064495857664 18446744073709551616 4575657221408423936 4827858800541171712 (by decide +kernel)))) (RegionPosI.split_b 2594073385365405696 (RegionPosI.of_check c4 q4 ok_4 2305843009213693952 2594073385365405696 16140901064495857664 18446744073709551616 4827858800541171712 5332261958806667264 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 2594073385365405696 2882303761517117440 16140901064495857664 18446744073709551616 4827858800541171712 5332261958806667264 (by decide +kernel))))

end CKLaneC.RSC2.BA_0129