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

import Definitions.Def_CK_CKLaneC_RSC2_S02_0018_part00

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

namespace CKLaneC.RSC2.S02_0018
open CKLaneC.TM3 CKLaneC.RSCell

theorem sE_6 : stageE w6 q6 = true := by decide +kernel
theorem sF_6 : stageF w6 = true := by decide +kernel
theorem ok_6 : (domOK c6 && cellCheck c6 q6) = true :=
  staged_check c6 q6 w6 (by decide +kernel) sB_6 s0_6 s1_6 s2_6 s3_6 sE_6 sF_6

noncomputable def c7 : Cell := { bc := 3799912185593856, bh := 140737488355328, tc := 6917529027641081856, th := 2305843009213693952, sc := 2810246167479189504, sh := 72057594037927936 }
noncomputable def q7 : Cert := { V0 := [[[723712886054216698]], [[(-5934623563385757), 240702259428833212], [2747148308688591]], [[24486138315785, (-1965042617998351), (-266984260151461)], [(-23033060223633), 909621890399296], [(-40452121264347)]], [[(-141238238298), 7999875851597, 6553919447898, (-29276920024670)], [110703492741, (-7526742087242), (-3033821527901)], [337426818151, (-13417412396274)], [909707900273]], [[1189919214, (-45582485796), (-80496534205), 712332338742, 96362305775], [(-818063318), 34998680912, 74925646936, (-329739967280)], [(-1565445652), 110833061087, 33219143051], [(-7575516800), 301869363553], [(-23835208292)]]], r0 := 4749256448773, V1 := [[[1916968944411223912]], [[(-15510150087764904), 0], [7179677384086840]], [[61460485090784, 0, 0], [(-57850882324690), 0], [(-106264695555254)]], [[(-341858133867), 0, 0, 0], [251145585746, 0, 0], [860511480722, 0], [2392884246133]], [[2870769243, 0, 0, 0, 0], [(-1765825987), 0, 0, 0], [(-3693605185), 0, 0], [(-19395028452), 0], [(-62742715543)]]], r1 := 1574295759881, V2 := [[[18442511048839452119]], [[(-16963601385625), 102585467058], [(-156201384887070)]], [[17237248521, (-57212158), (-2376275)], [(-636656002349), 7626724926], [12749986757]], [[(-166660788), (-2326389), 12211, 54], [704617425, (-3959559), (-265294)], [(-187788105), 142384582], [(-126791942)]], [[2195584, 5946, 48, (-1), 0], [(-6807981), (-175925), 1356, 8], [1481604, (-61792), (-9902)], [1789194, 17724], [2108371]]], r2 := 4139393220, V3 := [[[18445586010828783062]], [[(-29692702849222), 55440084270], [(-42901571517466)]], [[32109765, 1177993566, (-2548614)], [(-1099950141664), 4125029113], [(-385481045)]], [[10449, (-6424666), (-42750), 115], [2384189, 87726666, (-284541)], [(-8215338), 77149286], [(-55682)]], [[(-102), (-2084), 543, 1, 0], [847, (-477141), (-4779), 17], [44378, 1643961, (-10620)], [(-1449), 11803], [379]]], r3 := 9137363598, Vm := [[[18442511598981953730]], [[(-16964276359795), 0], [(-156160334723126)]], [[17227667833, 0, 0], [(-636706113229), 0], [13522498974]], [[(-166652104), 0, 0, 0], [703895668, 0, 0], [(-188719705), 0], [(-126603340)]], [[2195553, 0, 0, 0, 0], [(-6807270), 0, 0, 0], [1467726, 0, 0], [1789169, 0], [2107089]]], rm := 489924497 }
noncomputable def w7 : Wit := { Z0 := { p := [[[724517519472313533]], [[(-5954436203118213), 241505839824104511], [2756319616548365]], [[24730724142096, (-1984812067706071), 0], [(-23260712906618), 918773205516121], [(-40552277087254)]], [[(-143502672111), 8243574714032, 0, 0], [113582861025, (-7753570968873), 0], [339899381454, (-13517425695752)], [911761892620]], [[1209999570, (-47834224037), 0, 0, 0], [(-846096251), 37860953675, 0, 0], [(-1596202938), 113299793818, 0], [(-7626169848), 303920630873], [(-23886073609)]]], r := 1141725148400, ok := true }, Z1 := { p := [[[1932046718592836088]], [[(-15878496541648567), 0], [7350185644128974]], [[65948597712257, 0, 0], [(-62028567750980), 0], [(-108139405566009)]], [[(-382673792296), 0, 0, 0], [302887629402, 0, 0], [906398350545, 0], [2431365046988]], [[3226665520, 0, 0, 0, 0], [(-2256256669), 0, 0, 0], [(-4256541166), 0, 0], [(-20336452926), 0], [(-63696196290)]]], r := 402709036874, ok := true }, Z2 := { p := [[[11060977397875954109734]], [[(-39935567060057910353), 241505839824104511], [(-367727980587759906384)]], [[193548629541763532, (-1984812067706071), 0], [1318273861274816918, 918773205516121], [12999915959484029618]], [[(-1298994226546118), 8243574714032, 0, 0], [(-6179269726544207), (-7753570968873), 0], [(-46487025891192891), (-13517425695752)], [(-467550843440459124)]], [[12487189488630, (-47834224037), 0, 0, 0], [39775713905721, 37860953675, 0, 0], [215247143622358, 113299793818, 0], [1669433648142898, 303920630873], [16951858153382594]]], r := 1370945504275608, ok := true }, Z3 := { p := [[[35827147894098890540864]], [[(-837864458044327525254), 1564400398210775195], [(-1210590431974536931249)]], [[20629983638825309000, (-43793812358368004), 0], [28573706085576415402, 5096342029884256], [43054350147026096175]], [[(-515527237732537832), 1069383347621278, 0, 0], [(-706001220605823304), (-131170982571472), 0], [(-1019767777990062877), (-77772886699038)], [(-1554064010905514854)]], [[12973049827848959, (-26661177404394), 0, 0, 0], [17679512539441300, 3040479853293, 0, 0], [25231235919932203, 2039227250989, 0], [36886348951543091, 1769446097492], [56488418557649119]]], r := 44588655004434622, ok := true }, iE := { p := [[[11064811442199428948631]], [[(-39946069897524731834), 0], [(-367713394533875099749)]], [[193603661068122524, 0, 0], [1318230687641238989, 0], [12999701362564574031]], [[(-1299386054432321), 0, 0, 0], [(-6178974811157447), 0, 0], [(-46486402994450214), 0], [(-467546018525374518)]], [[12491125674259, 0, 0, 0, 0], [39773118964338, 0, 0, 0], [215243133590490, 0, 0], [1669419727829240, 0], [16951731751656663]]], r := 1370157403482004, ok := true }, iHu := { p := [[[35837219172238523964591]], [[(-838078354249536623648), 0], [(-1210557622804879104951)]], [[20635276960919054272, 0, 0], [28573083285268098047, 0], [43053849461667946149]], [[(-515659699450037039), 0, 0, 0], [(-705986330112279433), 0, 0], [(-1019758032384296128), 0], [(-1554052619586629154)]], [[12976385362211617, 0, 0, 0, 0], [17679148833037667, 0, 0, 0], [25231001555167254, 0, 0], [36886125352743518, 0], [56488118029647317]]], r := 44582528924354904, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[30753562200179544]], [[111026197930586, 0], [1022023448814309]], [[(-137276805645), 0, 0], [3715503966307, 0], [(-2166816208835)]], [[1173269210, 0, 0, 0], [(-5084485695), 0, 0], [(-7344257115), 0], [26745923336]], [[(-15041913), 0, 0, 0, 0], [43454416, 0, 0, 0], [(-5910), 0, 0], [90664150, 0], [(-495294894)]]], r := 314992113, ok := true }, de := { p := [[[(-137978555877050123832)]], [[341203351125310116, 0], [492849284958781279]], [[(-4374264656390196), 0, 0], [396589884253, 0], [(-9126552184320285)]], [[74773754883734, 0, 0, 0], [319131, 0, 0], [460968, 0], [225346967736028]], [[(-1437956824687), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-6259637992667)]]], r := 1114385110075, ok := true }, dde := { p := [[[(-424032764574308954019650)]], [[10872293775025792808600, 0], [15704424341703922912656]], [[(-278776763736770614095), 0, 0], [(-402677548016382149759), 0], [(-581645346561904189136)]], [[7148122147096494754, 0, 0, 0], [10325065323583160690, 0, 0], [14913983245175657904, 0], [21542420243032849986]], [[(-183285183258866252), 0, 0, 0, 0], [(-264745264707276565), 0, 0, 0], [(-382409826799397616), 0, 0], [(-552369749821350263), 0], [(-797867416408605339)]]], r := 88889943993158541, ok := true }, nJu := { p := [[[(-275957111754100247663)]], [[682406702250620233, 0], [985698569917562558]], [[(-8748529312780392), 0, 0], [793179768506, 0], [(-18253104368640570)]], [[149547509767469, 0, 0, 0], [638263, 0, 0], [921936, 0], [450693935472057]], [[(-2875913649373), 0, 0, 0, 0], [2, 0, 0, 0], [11822, 0, 0], [2, 0], [(-12519275985333)]]], r := 2228770220142, ok := true }, Jd1 := { p := [[[(-848065529148617908039299)]], [[21744587550051585617201, 0], [31408848683407845825313]], [[(-557553527473541228190), 0, 0], [(-805355096032764299518), 0], [(-1163290693123808378272)]], [[14296244294192989508, 0, 0, 0], [20650130647166321380, 0, 0], [29827966490351315809, 0], [43084840486065699973]], [[(-366570366517732504), 0, 0, 0, 0], [(-529490529414553130), 0, 0, 0], [(-764819653598795232), 0, 0], [(-1104739499642700525), 0], [(-1595734832817210677)]]], r := 177779887986317075, ok := true }, term0 := { p := [[[13515671821649073048828636705]], [[(-693078755175815313783498234), 0], [(-1001010672024088539912426768)]], [[26656457033927094588841839, 0, 0], [51332672583980186085808576, 0], [55608922543463399386998655]], [[(-911324716285618890682335), 0, 0, 0], [(-1974318073324223857481023), 0, 0], [(-2851694875663772743742701), 0], [(-2746050953803744259078341)]], [[29208988058086398193655, 0, 0, 0, 0], [67497789043597724257698, 0, 0, 0], [109679998526173316268730, 0, 0], [140821468726839697490364, 0], [127130080880573278352257]]], r := 25646077361929752361348, ok := true }, r0 := { p := [[[30340922348317866793443]], [[(-447574600191690482014), 20157196360399134166752], [(-996129723006952775862)]], [[6494906136772598380, (-296263414886072751811), 3312991927037902573327], [14218088634798325969, (-662308855687685650941)], [35061284534382029162]], [[(-115172397691498546), 4291861174391863561, (-47972594808476745446), (-15392291698388815257)], [(-197710390196229589), 9425961447452841209, (-109202980569983297638)], [(-494382039134624769), 23317145032435153470], [(-1257683633506601246)]], [[2423404088447778, (-76174203379066582), 690136410321951864, 462603012573571008, (-1232459400270289620)], [3406927060201957, (-130890058313839368), 1535965498093949464, 391777413863308498], [6762986671198235, (-327903088509279575), 3848257078709286826], [17603460289591933, (-836522745718154689)], [45514757050653683]]], r := 854229357009267067, ok := true }, r1 := { p := [[[211295777521105269436005]], [[(-3049481012977991057117), 0], [(-6969633142167935536397)]], [[43824634835531999172, 0, 0], [97753861555949519288, 0], [245662841131585248943]], [[(-781664430785927210), 0, 0, 0], [(-1348260280445275364), 0, 0], [(-3408331775947239253), 0], [(-8819345466608010694)]], [[16594864423719328, 0, 0, 0, 0], [23351939328459978, 0, 0, 0], [46261758751337179, 0, 0], [121551414968937615, 0], [319344228335249522]]], r := 282702734660504284, ok := true }, r2 := { p := [[[994624449403880064028581953]], [[(-19019928217617788438292123), 54231686402150546551814], [(-71521041782206834690937416)]], [[401696839721622692054971, (-707998828058329189724), 447698190785116098], [1342189702932035867275176, (-1945805593056319385657)], [3902290228846919985255728]], [[(-9417415929762948174107), 12461925682338190305, 118852357252813, (-33820675261336)], [(-28099483581923419709211), 24185940033054561417, 71873412918730], [(-72371359221231674542491), 71150478411216064850], [(-190253665297783274842071)]], [[231385301665879084069, (-269979329306467538), (-17524645411549), (-2847203217727), (-3043374967491)], [657125104257877820979, (-413393651374535625), (-3331493786077), (-17564994183688)], [1506713357496385372999, (-866344526593394349), (-19489503527025)], [3498315221344550756302, (-2614659155294147917)], [8721757538536058085618]]], r := 17295185460896115078665, ok := true }, r3 := { p := [[[27016974505401154142356926014]], [[(-1385468973073921757974116051), 1590878677033950630858099], [(-2001488740439219755695039952)]], [[53287050390575566284004824, (-76265129933693524616244), 1507580372745166194], [102639827444253953770876449, (-59004772407811935351830)], [111198113296203580848036664]], [[(-1821775754944611464434408), 2865316940673161521726, 7849178849325703, (-3024171728262404)], [(-3947677685084502518323431), 2827900513351901748976, (-5033720972143834)], [(-5702444425359685248848921), 2186502965960615579587], [(-5491370979940092643377770)]], [[58390166895913573392010, (-96809888191969102686), (-1486607663854847), (-10656058719947861), (-1122212001695235)], [134963199943540792354041, (-106240863196328050751), (-2717700396455438), (-9506547311641858)], [219324486744610030781628, (-104789855087379372120), (-4816361837508695)], [281607920398145463694500, (-81008669753420089779)], [254233083793888279876913]]], r := 2706193599762629826858918, ok := true }, eta := { p := [[[(-995722627452863547973938213)]], [[19047556615499404727840755, 0], [71560995228473415774183674]], [[(-402387582253139825157702), 0, 0], [(-1343190414183487972190955), 0], [(-3903759658809298266956566)]], [[9434918662444878011977, 0, 0, 0], [28124492673200538883792, 0, 0], [72408100562992780639093, 0], [190307858203201399324366]], [[(-231831576709161969485), 0, 0, 0, 0], [(-657759100410637581269), 0, 0, 0], [(-1507631489909275397585), 0, 0], [(-3499668861943452380345), 0], [(-8723758677387927240714)]]], r := 1466024745210998114446, 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 3377699720527872 3940649673949184 4611686018427387904 9223372036854775808 2305843009213693952 2882303761517117440 :=
  (RegionPosI.split_s 2594073385365405696 (RegionPosI.split_b 3659174697238528 (RegionPosI.split_s 2449958197289549824 (RegionPosI.of_check c0 q0 ok_0 3377699720527872 3659174697238528 4611686018427387904 9223372036854775808 2305843009213693952 2449958197289549824 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 3377699720527872 3659174697238528 4611686018427387904 9223372036854775808 2449958197289549824 2594073385365405696 (by decide +kernel))) (RegionPosI.split_s 2449958197289549824 (RegionPosI.of_check c2 q2 ok_2 3659174697238528 3940649673949184 4611686018427387904 9223372036854775808 2305843009213693952 2449958197289549824 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 3659174697238528 3940649673949184 4611686018427387904 9223372036854775808 2449958197289549824 2594073385365405696 (by decide +kernel)))) (RegionPosI.split_b 3659174697238528 (RegionPosI.split_s 2738188573441261568 (RegionPosI.of_check c4 q4 ok_4 3377699720527872 3659174697238528 4611686018427387904 9223372036854775808 2594073385365405696 2738188573441261568 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 3377699720527872 3659174697238528 4611686018427387904 9223372036854775808 2738188573441261568 2882303761517117440 (by decide +kernel))) (RegionPosI.split_s 2738188573441261568 (RegionPosI.of_check c6 q6 ok_6 3659174697238528 3940649673949184 4611686018427387904 9223372036854775808 2594073385365405696 2738188573441261568 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 3659174697238528 3940649673949184 4611686018427387904 9223372036854775808 2738188573441261568 2882303761517117440 (by decide +kernel)))))

end CKLaneC.RSC2.S02_0018