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

Definition
CK_CKLaneC_RSC2_BB_0023
by tianyipeng · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)
general-courtade-kumartransplant
Verbatim transplant of the Lean module CKLaneC.RSC2.BB_0023 of the machine-checked proof of the general Courtade–Kumar theorem (the most informative Boolean function conjecture), so that the complete proof can be verified on this platform.
It is the original source with only two mechanical changes. Imports of project modules are redirected to their transplanted bundles Definitions.Def_CK_*. Declarations that already exist in earlier platform definition bundles of this mission are removed, and those bundles are imported instead, so every constant keeps a single platform identity.
The module contains both definitions and the lemmas proved alongside them in the source. They are kept together so the transplant stays faithful and every proof is re-checked by the server.
Source: Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff, A Proof of the Most Informative Boolean Function Conjecture, arXiv:2609.24931 (2026). Lean development: https://github.com/dpwoodru/general-courtade-kumar-lean (Apache-2.0), module CKLaneC.RSC2.BB_0023 from release v1.0 (sources_v3.tar.zst).
Definition code
import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

-- ===== source module CKLaneC.RSC2.BB_0023 =====
section

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

namespace CKLaneC.RSC2.BB_0023
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 5332261958806667264, bh := 144115188075855872, tc := 7493989779944505344, th := 576460752303423488, sc := 2558044588346441728, sh := 252201579132747776 }
noncomputable def q0 : Cert := { V0 := [[[3284038492765927502]], [[(-100916852650462495), 241208111281948510], [42079160666733624]], [[2254720421286747, (-6719505657190181), (-1246865365002129)], [(-1405127774869412), 2801822993125571], [56720471753040]], [[(-80573164612868), 118721424143902, 109805591051583, (-23542745992705)], [43029080245917, (-67367387875890), (-45785485641026)], [(-3331598579097), (-1684005689873)], [3598882648192]], [[3646192131623, (-3666134307149), (-5441091609938), 1566918605214, 421936136606], [(-1861720320181), 1035810808642, 4020508689416, (-653355886642)], [228416471117, 332207418109, (-581179556806)], [(-121612666846), 203498500260], [(-27973792510)]]], r0 := 29083269532376, V1 := [[[7310394529904266672]], [[(-185064575066059931), 0], [77166120260388762]], [[2703465362617262, 0, 0], [(-1383142886838664), 0], [(-144836399093110)]], [[(-84641903011263), 0, 0, 0], [13434932881860, 0, 0], [11679721873473, 0], [5989914518553]], [[3910730502672, 0, 0, 0, 0], [(-712132746583), 0, 0, 0], [(-282364745666), 0, 0], [(-115087755937), 0], [(-88998459649)]]], r1 := 37851103089064, V2 := [[[11813036206110776252]], [[(-112692003699502994), 86503560248958215], [(-222451853010682955)]], [[1872284895189816, (-482110949621386), (-883460292005984)], [(-2962616323348119), 5704621052026162], [(-1577954763197363)]], [[(-59141050189715), (-38227335048772), 28846233654883, 7169180193406], [85702600387889, (-75417643064366), (-79019560333026)], [27459256916485, 118712140526743], [(-10280423659867)]], [[2807234367052, 1173412069959, (-68707426616), (-486490209240), (-39472451775)], [(-2857617219831), (-1754031753737), 3613740838612, 694645578336], [773905525403, (-4406296393091), (-2202780231664)], [1103096125977, 511332934865], [57521245738]]], r2 := 133676232791568, V3 := [[[16117901803025092152]], [[(-214092672132760799), 66921405650008971], [(-98587237642527813)]], [[1735524510818943, 4870694442687488, (-1707661850617976)], [(-8371912514752333), 5471265851600727], [(-1446193144649885)]], [[2935380480176, (-179972862711298), (-83768240021662), 40928311706244], [147378646855027, 351337133177738, (-203333512378789)], [(-90218519968955), 181284785469431], [(-18212977861261)]], [[(-695646161441), 967165011450, 7699721546811, 867299545762, (-936001370230)], [(-289457843654), (-18707603287763), (-7713787294358), 6322669790245], [5375876449258, 8269451558266, (-10344058449560)], [(-419990186981), 3496718910566], [(-180776612704)]]], r3 := 9884710873927272, Vm := [[[13682062022732515893]], [[(-121311472160433265), 0], [(-101211120199477204)]], [[1032463958147700, 0, 0], [(-3753631891163144), 0], [935964487151664]], [[(-39242492836709), 0, 0, 0], [27735908273016, 0, 0], [(-4470201725518), 0], [6916797282224]], [[2123139163219, 0, 0, 0, 0], [(-1206188371067), 0, 0, 0], [(-264123100445), 0, 0], [338285440303, 0], [32193849362]]], rm := 74655369645731 }
noncomputable def w0 : Wit := { Z0 := { p := [[[3361296933095342509]], [[(-108177095419587007), 258561302545795577], [45106454066574719]], [[2650887670261918, (-8321315032275924), 0], [(-1701321503899725), 3469727235890363], [101477407914392]], [[(-99684237471152), 203914436173993, 0, 0], [60576620829118, (-130870884915364), 0], [(-8042656856077), 7805954454953], [4174802329244]], [[4602188402285, (-7668018267012), 0, 0, 0], [(-2795189570202), 4659740063778, 0, 0], [544601956031, (-618665912006), 0], [(-185307987543), 321138640711], [(-21765508048)]]], r := 5135664302528, ok := true }, Z1 := { p := [[[8273961681465458484]], [[(-266282081032829555), 0], [111031271548491616]], [[6525261957567800, 0, 0], [(-4187868317291630), 0], [249790542558504]], [[(-245376584544375), 0, 0, 0], [149111682040906, 0, 0], [(-19797309184190), 0], [10276436502755]], [[11328463759473, 0, 0, 0, 0], [(-6880466634344), 0, 0, 0], [1340558660999, 0, 0], [(-456142738567), 0], [(-53576635195)]]], r := 9561320271487, ok := true }, Z2 := { p := [[[17380938568761028369]], [[(-336839214237890548), 258561302545795577], [(-664914145760384940)]], [[10077924124812015, (-8321315032275924), 0], [8837920895713416, 3469727235890363], [12746526827457894]], [[(-397568000893006), 203914436173993, 0, 0], [(-227804980333311), (-130870884915364), 0], [(-167499735042888), 7805954454953], [(-335846610502184)]], [[19069153610084, (-7668018267012), 0, 0, 0], [7604984555981, 4659740063778, 0, 0], [3242708416101, (-618665912006), 0], [4621420066792, 321138640711], [8432306028997]]], r := 20399362252801, ok := true }, Z3 := { p := [[[47444548592728153969]], [[(-3784086269712740095), 1182835310276483314], [(-1742528637788485414)]], [[339587253597412200, (-107030778605474581), 0], [136527311881814961, 7774897723801657], [39943236816048819]], [[(-31706081185675521), 9413070241424900, 0, 0], [(-12495587755818909), (-501202539668861), 0], [(-3312814018970158), (-51782227785406)], [(-1012122621942619)]], [[3008227428078444, (-876420257461195), 0, 0, 0], [1174523044220217, 39460960952153, 0, 0], [304125455090758, 4890253317330, 0], [84616877139572, 838257183080], [26190092455680]]], r := 1433621934632851, ok := true }, iE := { p := [[[33231743136392736854]], [[(-542013911273015801), 0], [(-452206490834543751)]], [[17604827151526154, 0, 0], [4907318603786118, 0], [13225061926527422]], [[(-706094846629578), 0, 0, 0], [(-31540567513677), 0, 0], [(-196219792598879), 0], [(-316159573877183)]], [[34292065677745, 0, 0, 0, 0], [(-1499396390882), 0, 0, 0], [5227342441882, 0, 0], [4126326032539, 0], [8329666833101]]], r := 34072714996608, ok := true }, iHu := { p := [[[76012301177206212445]], [[(-5671552350439278337), 0], [(-1554749872128141974)]], [[514885547754402359, 0, 0], [129007263814865586, 0], [38692596208016279]], [[(-48148427469463691), 0, 0, 0], [(-11765318078896285), 0, 0], [(-3225241635527547), 0], [(-991877095282765)]], [[4571871075503330, 0, 0, 0, 0], [1109244820788444, 0, 0, 0], [297127259219413, 0, 0], [83357480383342, 0], [25818339872712]]], r := 1834520203855447, ok := true }, T := { p := [[[7493989779944505344]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[10239678536401797624]], [[167010445131164999, 0], [139338134602670234]], [[(-2700604231418527), 0, 0], [3033155656589669, 0], [(-2178964057538233)]], [[85046070342802, 0, 0, 0], [(-76037244234913), 0, 0], [(-20844186643548), 0], [12315792526057]], [[(-4200041200135), 0, 0, 0, 0], [2290176742705, 0, 0, 0], [(-85816724803), 0, 0], [172102099849, 0], [(-206242852825)]]], r := 8393961575837, ok := true }, de := { p := [[[(-42259446069946058995)]], [[1366693427878336813, 0], [374653410731127081]], [[(-64558833196747335), 0, 0], [1542469811622533, 0], [(-4851464321414459)]], [[4251025484047189, 0, 0, 0], [6350437635478, 0, 0], [1740853560305, 0], [87572845691872]], [[(-314312547813161), 0, 0, 0, 0], [26145119897, 0, 0, 0], [96567517349, 0, 0], [1964752305, 0], [(-1774990600498)]]], r := 137710529588096, ok := true }, dde := { p := [[[(-345820928530635835380)]], [[32671256311830373799, 0], [8956213120231492439]], [[(-3226971499488609139), 0, 0], [(-886220690133474461), 0], [(-242500310504048484)]], [[318127986617502933, 0, 0, 0], [87195599060569870, 0, 0], [23903040669113766, 0], [6553565295448878]], [[(-31364830432132535), 0, 0, 0, 0], [(-8598162639992621), 0, 0, 0], [(-2357219013309720), 0, 0], [(-646134343080782), 0], [(-177123947454773)]]], r := 5260830581481691, ok := true }, nJu := { p := [[[(-84518892139892117990)]], [[2733386855756673627, 0], [749306821462254162]], [[(-129117666393494670), 0, 0], [3084939623245067, 0], [(-9702928642828917)]], [[8502050968094379, 0, 0, 0], [12700875270956, 0, 0], [3481707120610, 0], [175145691383744]], [[(-628625095626321), 0, 0, 0, 0], [52290239794, 0, 0, 0], [193135034698, 0, 0], [3929504611, 0], [(-3549981200995)]]], r := 275421059176184, ok := true }, Jd1 := { p := [[[(-691641857061271670759)]], [[65342512623660747598, 0], [17912426240462984878]], [[(-6453942998977218278), 0, 0], [(-1772441380266948921), 0], [(-485000621008096968)]], [[636255973235005867, 0, 0, 0], [174391198121139741, 0, 0], [47806081338227532, 0], [13107130590897757]], [[(-62729660864265070), 0, 0, 0, 0], [(-17196325279985242), 0, 0, 0], [(-4714438026619439), 0, 0], [(-1292268686161564), 0], [(-354247894909546)]]], r := 10521661162963376, ok := true }, term0 := { p := [[[11737418089445957111412]], [[(-2202788719079276252320), 0], [(-539267628660121477379)]], [[320981792900204298145, 0, 0], [103689091671033749214, 0], [20623656208331865718]], [[(-41876393100743988809), 0, 0, 0], [(-15201861167610521129), 0, 0], [(-3994934348190484418), 0], [(-720892109157767872)]], [[5137300728629991102, 0, 0, 0, 0], [1989783703051300499, 0, 0, 0], [587266646257962257, 0, 0], [140209281771344224, 0], [23902290071834149]]], r := 1247923580657918749, ok := true }, r0 := { p := [[[152763813036367915772]], [[(-14321040841390879846), 22012504865077503388], [(-1316493491919029280)]], [[1229812796406909156, (-1986562508051631150), 634837939147827372], [41934524780480259, (-224813188070674486)], [52435823598999784]], [[(-106512728458186677), 168147822122377939, (-46582669425168062), (-13823218836706935)], [333131210680924, 10485724707554790, (-11389913841023199)], [(-4041359850064223), 7644881237155194], [(-1117326342552603)]], [[9515483987135363, (-14545509392978029), 3647458573152456, 1807125576023928, (-57487154730512)], [(-194645282312242), (-419697705817417), 876374314598282, (-118898707136915)], [314137377077784, (-549839185969382), 243170414594764], [68347133002734, (-174160757532979)], [30613045145518]]], r := 18644489929838546, ok := true }, r1 := { p := [[[710874348503169401363]], [[(-58854910097516270730), 0], [(-9750509602965704986)]], [[4946458982859609991, 0, 0], [541890083265009952, 0], [277950499003988695]], [[(-433757672268121105), 0, 0, 0], [(-30980362495629531), 0, 0], [(-18995245812355758), 0], [(-6632900241423455)]], [[39476497335928272, 0, 0, 0, 0], [2126042871750231, 0, 0, 0], [1370934880434648, 0, 0], [411951956920559, 0], [174094723538070]]], r := 48461870047748567, ok := true }, r2 := { p := [[[971493488275396638491]], [[(-99260836489855114229), 25716607792482503396], [(-63131160783682593796)]], [[9128311686957338744, (-2165584353181603881), 16224287699034179], [6207715938682672939, (-259668752990216524)], [2349878629152009613]], [[(-845556456984474103), 188409443710977544, 4237568791073422, (-879062204697249)], [(-571722292466885780), 14881104597794071, 468533442491805], [(-227286605156152166), 10204372506750692], [(-81919014880103538)]], [[79630039500847146, (-17152932725489773), (-252320354244680), (-24781054563358), 19828621478841], [53539940125794451, (-1243666177440358), 249749437159451, (-110884722505151)], [20927447957524686, (-951681935919821), 138517283603387], [7904263490225150, (-340445234337168)], [2695461197557525]]], r := 331605450255475504, ok := true }, r3 := { p := [[[11713298484214753048723]], [[(-2243937456271455415454), 331699962406405636186], [(-762271254559679380546)]], [[327675460592481966032, (-60846195608973079330), (-156569495151150997)], [148274431725778324595, (-8697073054448546174)], [32635966037142195036]], [[(-42816359186925244609), 8882714148511183643, 11461346149971279, 3543045150544102], [(-21866308367286175858), 1682782310333378199, (-17596789446831962)], [(-6400072187656084801), 249763232653691130], [(-1210328253757779297)]], [[5257871508965331296, (-1159953221807041489), (-1386217219969102), (-139567341506455), (-96773729267486)], [2869823374359540659, (-242391458824269186), (-468895731839666), 687093169545500], [943943681679570503, (-44452590849453347), (-821960276641890)], [237217572590520233, (-6321069594625747)], [41500252076067749]]], r := 912041627091595278247, ok := true }, eta := { p := [[[(-2449441979006219883234)]], [[250765676768712404147, 0], [88978833969153404785]], [[(-24098595793915429647), 0, 0], [(-8857208649683532655), 0], [(-3129168989778111755)]], [[2305431869226116641, 0, 0, 0], [828327372736295055, 0, 0], [307736952234126858, 0], [101877805810562582]], [[(-222071860496393194), 0, 0, 0, 0], [(-78515488164320793), 0, 0, 0], [(-28648429492546660), 0, 0], [(-9861263560459622), 0], [(-3215894584381380)]]], r := 158519376832518319, ok := true } }
theorem sB_0 : stageB c0 w0 = true := by decide +kernel
theorem s0_0 : stageC0 w0 q0 = true := by decide +kernel
theorem s1_0 : stageC1 w0 q0 = true := by decide +kernel
theorem s2_0 : stageC2 w0 q0 = true := by decide +kernel
theorem s3_0 : stageC3 w0 q0 = true := by decide +kernel
theorem sE_0 : stageE w0 q0 = true := by decide +kernel
theorem sF_0 : stageF w0 = true := by decide +kernel
theorem ok_0 : (domOK c0 && cellCheck c0 q0) = true :=
  staged_check c0 q0 w0 (by decide +kernel) sB_0 s0_0 s1_0 s2_0 s3_0 sE_0 sF_0

noncomputable def c1 : Cell := { bc := 5332261958806667264, bh := 144115188075855872, tc := 7493989779944505344, th := 576460752303423488, sc := 3062447746611937280, sh := 252201579132747776 }
noncomputable def q1 : Cert := { V0 := [[[3090631786470191438]], [[(-92761959153220738), 228216934072555124], [39427447148101108]], [[1845438263711773, (-6284168185369962), (-1047284893991196)], [(-1252778701372847), 2671016343986411], [50883838432621]], [[(-57735070344010), 99927691684185, 90569666942468, (-20567536738013)], [33710424050255, (-63539711201837), (-38495637534963)], [(-2544443070489), (-1085890089713)], [3369445857719]], [[2222030425925, (-2680103848977), (-4245628697496), 1408853790216, 320058090112], [(-1293404136477), 884784270688, 3300595521124, (-598817757412)], [169089261402, 269391734339, (-491174432375)], [(-108336871144), 198687282458], [(-26506829771)]]], r0 := 17245708285732, V1 := [[[6950458327233783866]], [[(-175156793000458498), 0], [74448462081847748]], [[2274464561566895, 0, 0], [(-1336811794251359), 0], [(-122545230706712)]], [[(-60455526844120), 0, 0, 0], [9975680815519, 0, 0], [10639391721051, 0], [5766438523516]], [[2321465908555, 0, 0, 0, 0], [(-465235651178), 0, 0, 0], [(-240319662387), 0, 0], [(-108585794025), 0], [(-83477254338)]]], r1 := 19325605254668, V2 := [[[11594708484133351709]], [[(-105834065024709877), 85395137977417605], [(-228055308931269597)]], [[1573852407963384, (-622265298107106), (-826137076701984)], [(-2650531972345235), 5547400584351626], [(-1520272424424602)]], [[(-41864028299508), (-32144563457583), 28433593726529, 6247160552795], [71124352665273, (-81510591606065), (-72008629758207)], [30069214614584, 110082176775869], [(-8157411809215)]], [[1649282440993, 877164591775, (-133933722246), (-436141115359), (-30225362107)], [(-2068229891858), (-1314724046176), 3396638806757, 571942299113], [542619172142, (-4220071793310), (-1855894942172)], [1019646442393, 282684835786], [85358592833]]], r2 := 90019710320296, V3 := [[[15696671855090309772]], [[(-207135288863839257), 75951667202255056], [(-114744875707484255)]], [[1738700923357794, 4164407808145995, (-1845636566550339)], [(-7787848736128576), 6100918610772518], [(-1605597506656306)]], [[(-1548915015518), (-172736851043791), (-54835887439526), 41763926923133], [144215225321470, 279267552949305, (-214766400648535)], [(-69439501371498), 194476721152469], [(-18582042899297)]], [[(-448167164962), 1402998709668, 6757090288484, 4768256186, (-893000676073)], [(-729325579064), (-17283127793871), (-3835587727535), 6261317644767], [4996495315958, 5003220980639, (-10470072716605)], [37528430135, 3441913980310], [(-150084773344)]]], r3 := 4996313951071808, Vm := [[[13443285280401364911]], [[(-117593580408767286), 0], [(-108616121857623358)]], [[839279972313055, 0, 0], [(-3655279227802150), 0], [925974224135599]], [[(-26355679754010), 0, 0, 0], [21848468101889, 0, 0], [(-5517023886863), 0], [7572758255607]], [[1210307033729, 0, 0, 0, 0], [(-795231784038), 0, 0, 0], [(-259561827258), 0, 0], [317843936586, 0], [41947340148]]], rm := 41884651116059 }
noncomputable def w1 : Wit := { Z0 := { p := [[[3154815335188570896]], [[(-98639903047307074), 242678102706813145], [41925802339594993]], [[2146365011316228, (-7587684849792852), 0], [(-1488567051013521), 3225061718430384], [87347229664470]], [[(-70869248725439), 165105000870479, 0, 0], [46675704009139, (-114505157770271), 0], [(-6187812780479), 6719017666497], [3834229048193]], [[2800910301480, (-5451480671188), 0, 0, 0], [(-1914890253029), 3590438769933, 0, 0], [393564328909, (-475985598499), 0], [(-156709966822), 294940696014], [(-21560898576)]]], r := 2790015256816, ok := true }, Z1 := { p := [[[7765699286618020667]], [[(-242805915193371258), 0], [103201974989772291]], [[5283360027855332, 0, 0], [(-3664165048648666), 0], [215008565327927]], [[(-174447381478003), 0, 0, 0], [114894040637882, 0, 0], [(-15231539151948), 0], [9438102272475]], [[6894548434412, 0, 0, 0, 0], [(-4713576007456), 0, 0, 0], [968773732699, 0, 0], [(-385747610639), 0], [(-53072981109)]]], r := 4733129482302, ok := true }, Z2 := { p := [[[16744666204004004494]], [[(-300761972054404435), 242678102706813145], [(-648093451155171701)]], [[8078684916202993, (-7587684849792852), 0], [8008648898449604, 3225061718430384], [12423821415810750]], [[(-278898259912106), 165105000870479, 0, 0], [(-188892774027006), (-114505157770271), 0], [(-155521046233803), 6719017666497], [(-327003076904770)]], [[11455949305043, (-5451480671188), 0, 0, 0], [5532135538407, 3590438769933, 0, 0], [2768657869751, (-475985598499), 0], [4233801704704, 294940696014], [8215387714198]]], r := 10440586186900, ok := true }, Z3 := { p := [[[41021479828321612549]], [[(-2728644335012259978), 1000530076661165342], [(-1511562596543982835)]], [[203735213910922272, (-77754135987025727), 0], [97755258437810346, 6906525992644360], [34341146872203382]], [[(-15864515370236770), 5656047967948561, 0, 0], [(-7470128655021663), (-377240614798310), 0], [(-2370303769701781), (-43323560932796)], [(-869167096525354)]], [[1256001456806345, (-439003921589516), 0, 0, 0], [585863110141152, 24210456485725, 0, 0], [181338722087043, 3667471631857, 0], [60422265888265, 713810963777], [22465797617302]]], r := 573861354710529, ok := true }, iE := { p := [[[32212979837192138900]], [[(-479104163572378931), 0], [(-442527866165664055)]], [[14061795330101962, 0, 0], [4767320636787447, 0], [12852091916581403]], [[(-493105804294321), 0, 0, 0], [(-37577306081902), 0, 0], [(-177407640897232), 0], [(-308203543126229)]], [[20515648008447, 0, 0, 0, 0], [(-610968653422), 0, 0, 0], [4238099278962, 0, 0], [3836485410388, 0], [8109672892270]]], r := 16809354707737, ok := true }, iHu := { p := [[[66404951304833097700]], [[(-4071918381465897567), 0], [(-1336343870365255995)]], [[308637843739474888, 0, 0], [92528975928376236, 0], [33242027116735055]], [[(-24076952627136153), 0, 0, 0], [(-7021981110297593), 0, 0], [(-2304511175194180), 0], [(-851057695657430)]], [[1908045301196599, 0, 0, 0, 0], [552584545316552, 0, 0, 0], [177133573906636, 0, 0], [59516455328819, 0], [22134276362674]]], r := 719383624881887, ok := true }, T := { p := [[[7493989779944505344]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[10563517210787766492]], [[157111360179525974, 0], [145116991787793759]], [[(-2274527552181994), 0, 0], [2753319835466189, 0], [(-2220998547690945)]], [[59290641498131, 0, 0, 0], [(-64572479337931), 0, 0], [(-21191740323260), 0], [12659579123680]], [[(-2447912099006), 0, 0, 0, 0], [1593873968334, 0, 0, 0], [(-87971995059), 0, 0], [171669167442, 0], [(-210921316538)]]], r := 4120759990743, ok := true }, de := { p := [[[(-39754633593534417767)]], [[1151069016677985915, 0], [377763963002427811]], [[(-45007777774766503), 0, 0], [1568188783921220, 0], [(-4847590143597859)]], [[2477627294525613, 0, 0, 0], [6509927634364, 0, 0], [2136462737147, 0], [87577685126161]], [[(-153009334997038), 0, 0, 0, 0], [27024270445, 0, 0, 0], [101275448656, 0, 0], [2910665523, 0], [(-1774984537722)]]], r := 55125267548123, ok := true }, dde := { p := [[[(-291260459756789516866)]], [[22777063507699595080, 0], [7475098062372453976]], [[(-1880777402015798029), 0, 0], [(-618890786829299232), 0], [(-202570276673933578)]], [[154866714723796947, 0, 0, 0], [50811307437633381, 0, 0], [16675525606945317, 0], [5474135843018574]], [[(-12753815943200143), 0, 0, 0, 0], [(-4185700430456841), 0, 0, 0], [(-1373888914484652), 0, 0], [(-450823416616474), 0], [(-147950620768116)]]], r := 1949350928844903, ok := true }, nJu := { p := [[[(-79509267187068835534)]], [[2302138033355971830, 0], [755527926004855622]], [[(-90015555549533006), 0, 0], [3136377567842441, 0], [(-9695180287195718)]], [[4955254589051227, 0, 0, 0], [13019855268729, 0, 0], [4272925474294, 0], [175155370252323]], [[(-306018669994075), 0, 0, 0, 0], [54048540890, 0, 0, 0], [202550897313, 0, 0], [5821331047, 0], [(-3549969075443)]]], r := 110250535096237, ok := true }, Jd1 := { p := [[[(-582520919513579033731)]], [[45554127015399190160, 0], [14950196124744907953]], [[(-3761554804031596057), 0, 0], [(-1237781573658598464), 0], [(-405140553347867156)]], [[309733429447593895, 0, 0, 0], [101622614875266763, 0, 0], [33351051213890634, 0], [10948271686037149]], [[(-25507631886400286), 0, 0, 0, 0], [(-8371400860913681), 0, 0, 0], [(-2747777828969304), 0, 0], [(-901646833232947), 0], [(-295901241536231)]]], r := 3898701857689797, ok := true }, term0 := { p := [[[8347194924314158381287]], [[(-1294900445193045900024), 0], [(-379940854538481500900)]], [[157186772142112432534, 0, 0], [60739506131828629706, 0], [14489521081309269945]], [[(-17104624156493351798), 0, 0, 0], [(-7425440448264395431), 0, 0], [(-2336475091484190218), 0], [(-505683151613552699)]], [[1751205873396486537, 0, 0, 0, 0], [811170172265527132, 0, 0, 0], [286565781715591446, 0, 0], [81936481703484179, 0], [16750121176999968]]], r := 396065541768173799, ok := true }, r0 := { p := [[[128317588062766092723]], [[(-10432450619111004935), 18613245060528144977], [(-1232533828283205567)]], [[764728709916644090, (-1454607549671457850), 554122632245933776], [41535055238421177, (-205397728068338691)], [45429946458009903]], [[(-55550778243050372), 104706804974992536, (-35036544480758043), (-10758642836478780)], [(-413224359207511), 8986569106503579, (-9875921010807913)], [(-3040917342468002), 6683766106468875], [(-995276096787730)]], [[4130219140059346, (-7569436277005907), 2278369514190747, 1296334071646031, (-62516090472250)], [(-73025942558033), (-334269256526288), 654603383725378, (-90341297845940)], [198501605143290, (-420766113973359), 219181036767172], [54580952399742, (-154477074619352)], [26992674112961]]], r := 8549817871898167, ok := true }, r1 := { p := [[[610012877943418394710]], [[(-43250678616410101111), 0], [(-8775957842812129282)]], [[3062752138197678240, 0, 0], [439020996778891478, 0], [244681117405090267]], [[(-223624602766523769), 0, 0, 0], [(-21369280007670337), 0, 0], [(-14598859145192169), 0], [(-5902644023884905)]], [[16900450972178413, 0, 0, 0, 0], [1198857902289112, 0, 0, 0], [879497846990551, 0, 0], [324344406723594, 0], [154533293751379]]], r := 19497629865170165, ok := true }, r2 := { p := [[[803790828361079243864]], [[(-70839340973654149374), 22023423764752719045], [(-52642708485666942893)]], [[5496162091271717842, (-1576358625370973106), 23820225860164605], [4431997355586568898, (-234129480104049831)], [1965838040647087554]], [[(-425505489922462603), 114550179863907411, 3413798604794924, (-917278138334646)], [(-342521792025896993), 10975579312091130, 907176319346448], [(-162291079725689632), 8553499383097012], [(-68539575139214261)]], [[33388059213040974, (-8679363208069197), (-168429494507079), (-13986764515875), 18452765407644], [26744897559525363, (-762877272731730), 191896858411149, (-108833309245546)], [12537079849396947, (-716297377007351), 140020092376236], [5664858580131919, (-309012155996921)], [2263708077433672]]], r := 170502159132435240, ok := true }, r3 := { p := [[[8261582486212585937620]], [[(-1317606274556275871245), 238099016991971806892], [(-534795466162569934320)]], [[160274683688206718864, (-35731560633961680562), (-137384960408687151)], [86554891273070950302, (-6099859764114298240)], [22817661426713125537]], [[(-17471118416795351746), 4345609863225489986, 8425973338363884, 3172611384326278], [(-10657271333475437712), 995003490421380734, (-18089050870932143)], [(-3735643182093610420), 181203419482115822], [(-846492045315342365)]], [[1790929910046159844, (-473795524596465423), (-309976713069517), (-231015728887654), (-76711019118833)], [1168273961046519025, (-119603083208983610), (-28496133107620), 635194440066101], [460114286824342742, (-26283961530436512), (-824242396491525)], [138404392146431704, (-4437587027182237)], [28995255395851378]]], r := 247714726348636858778, ok := true }, eta := { p := [[[(-2028838129995050218663)]], [[176324667663190465372, 0], [74050734606546827517]], [[(-14267820557273230616), 0, 0], [(-6292019787490144517), 0], [(-2610104783414580595)]], [[1141482656183605793, 0, 0, 0], [493201814832845389, 0, 0], [218959316381856554, 0], [85219985260928210]], [[(-91749853596709787), 0, 0, 0, 0], [(-38967495502212896), 0, 0, 0], [(-17082194798062873), 0, 0], [(-7038310053768694), 0], [(-2695007468950722)]]], r := 69777906877607078, ok := true } }
theorem sB_1 : stageB c1 w1 = true := by decide +kernel
theorem s0_1 : stageC0 w1 q1 = true := by decide +kernel
theorem s1_1 : stageC1 w1 q1 = true := by decide +kernel
theorem s2_1 : stageC2 w1 q1 = true := by decide +kernel
theorem s3_1 : stageC3 w1 q1 = true := by decide +kernel
theorem sE_1 : stageE w1 q1 = true := by decide +kernel
theorem sF_1 : stageF w1 = true := by decide +kernel
theorem ok_1 : (domOK c1 && cellCheck c1 q1) = true :=
  staged_check c1 q1 w1 (by decide +kernel) sB_1 s0_1 s1_1 s2_1 s3_1 sE_1 sF_1

noncomputable def c2 : Cell := { bc := 5332261958806667264, bh := 144115188075855872, tc := 7493989779944505344, th := 576460752303423488, sc := 3819052484010180608, sh := 504403158265495552 }
noncomputable def q2 : Cert := { V0 := [[[2827554695808250066]], [[(-166085528584240555), 210198269727712156], [35941459918677170]], [[5694597000739163, (-11496180012008475), (-809751423765773)], [(-2160853965452613), 2487811530851861], [44580189487899]], [[(-303999443387476), 320144335517425, 137975424900473, (-16681636166070)], [97801829511309, (-117531658388892), (-29858340134118)], [(-3428782678239), (-380931008904)], [3068456009365]], [[19289290689254, (-14604750459978), (-12153890326214), 2370954608497, 212230532489], [(-6524372163380), 2861146872294, 5007898320839, (-513082450692)], [449440071347, 410500142976, (-384662066459)], [(-186184365390), 189998227581], [(-24384516492)]]], r0 := 126080883710760, V1 := [[[6443990676583134040]], [[(-325858377140107078), 0], [70516834916209877]], [[7326627495413762, 0, 0], [(-2574949387611975), 0], [(-92649510214614)]], [[(-320809208945187), 0, 0, 0], [27012044944333, 0, 0], [18665548243194, 0], [5452973416725]], [[19633561165888, 0, 0, 0, 0], [(-2195035079263), 0, 0, 0], [(-793730855220), 0, 0], [(-201433284403), 0], [(-75785771890)]]], r1 := 209620544768404, V2 := [[[11290357460195174159]], [[(-194740651240393855), 83260614380250493], [(-235417178990089804)]], [[5075031676130529, (-1588372861016903), (-742260948945631)], [(-4545153069960082), 5292569133237044], [(-1425991153499055)]], [[(-219887109347266), (-102233399374247), 54838161088713, 5043732024839], [223469722670449, (-175830091369173), (-62308900402125)], [65081098219802, 97877973226771], [(-5287774055409)]], [[13779540085881, 4890116488810, (-795771931416), (-735050295814), (-19733483557)], [(-11130382270236), (-3404352872818), 6141405228777, 422203496517], [1189429182084, (-7824433535916), (-1418238505215)], [1787239028471, 2463058359], [116159932533]]], r2 := 526292474614828, V3 := [[[15090840227137777179]], [[(-393573392554632420), 86930865382119144], [(-136833182475715291)]], [[6819310468071605, 6338692666380005, (-1953664801471333)], [(-13892243894930816), 6790323972142418], [(-1770961165253574)]], [[(-44615490657269), (-633977582586479), (-37236625370153), 40306703967202], [543291259991584, 365543061385327, (-219100585253182)], [(-82999956854222), 203244398163744], [(-17624881429923)]], [[(-3926359998819), 13683335348814, 21296922640814, (-1808831580228), (-772014507538)], [(-8724522090309), (-59415435473359), 1393091870715, 5750990382995], [17206309502908, 2051861346800, (-9950695666794)], [1139304202334, 3082919212358], [(-83565959896)]]], r3 := 24028502103260856, Vm := [[[13097431516129405543]], [[(-226319596479032934), 0], [(-119404098149071148)]], [[2616064427400897, 0, 0], [(-7084366377279106), 0], [907101770636610]], [[(-128016440639276), 0, 0, 0], [65345363369972, 0, 0], [(-14120824721377), 0], [8481344453794]], [[9698101077760, 0, 0, 0, 0], [(-3741133882448), 0, 0, 0], [(-1021360426148), 0, 0], [575634970962, 0], [57999350684]]], rm := 503403061131638 }
noncomputable def w2 : Wit := { Z0 := { p := [[[2876499303985323128]], [[(-174833067404359332), 221269177229640240], [37834456367978921]], [[6526693122814911, (-13448697492643026), 0], [(-2504989601287682), 2910342797536840], [71849820476870]], [[(-368405889004407), 502053317139608, 0, 0], [132424651199740, (-192691507791361), 0], [(-8563851017703), 5526909267451], [3412510421772]], [[24172672296348, (-28338914538801), 0, 0, 0], [(-9445638591731), 10186511630749, 0, 0], [1018075338668, (-658757770593), 0], [(-252843330094), 262500801674], [(-20774119659)]]], r := 25395323186215, ok := true }, Z1 := { p := [[[7080613671348487701]], [[(-430358319764576816), 0], [93130969521178883]], [[16065706148467473, 0, 0], [(-6166128249323523), 0], [176861096558449]], [[(-906845265241617), 0, 0, 0], [325968372183975, 0, 0], [(-21080248658961), 0], [8400025653594]], [[59501962575627, 0, 0, 0, 0], [(-23250802687337), 0, 0, 0], [2506031602875, 0, 0], [(-622383581769), 0], [(-51136294544)]]], r := 50491688829542, ok := true }, Z2 := { p := [[[15908373008248602850]], [[(-517532857448470696), 221269177229640240], [(-625632730296259476)]], [[24278400774923753, (-13448697492643026), 0], [14011596041579416, 2910342797536840], [11980478537934041]], [[(-1425327292919189), 502053317139608, 0, 0], [(-592399509781270), (-192691507791361), 0], [(-281118510602060), 5526909267451], [(-315038102871591)]], [[97240504413448, (-28338914538801), 0, 0, 0], [29693386880157, 10186511630749, 0, 0], [8994552727407, (-658757770593), 0], [7522359006994, 262500801674], [7919280896736]]], r := 110838912127134, ok := true }, Z3 := { p := [[[34322905335472921569]], [[(-3660820537333968579), 808586920100045209], [(-1272753021601508416)]], [[435912568631545681, (-105585610308493549), 0], [129782656279989093, 5953024697304884], [28550745171066322]], [[(-54329378663650939), 12128160639633217, 0, 0], [(-15908789248029803), (-538404817256545), 0], [(-3147602386682569), (-34084535692062)], [(-721771633878222)]], [[6889046867871639, (-1505938335036266), 0, 0, 0], [1998052380584083, 53125825758734, 0, 0], [384835901812152, 5194248027687, 0], [79989385506865, 581202661534], [18628532845485]]], r := 3562662424297164, ok := true }, iE := { p := [[[30890367298994440822]], [[(-812325428252708418), 0], [(-428575283241363577)]], [[42078121842035774, 0, 0], [9064298255214291, 0], [12354702025033163]], [[(-2505295179649852), 0, 0, 0], [(-159652757805512), 0, 0], [(-310340739192020), 0], [(-297264341694150)]], [[173197824277571, 0, 0, 0, 0], [(-14724053668), 0, 0, 0], [12994140558289, 0, 0], [6936007791912, 0], [7811080716857]]], r := 192651186320548, ok := true }, iHu := { p := [[[56441541627667754311]], [[(-5423899504174346555), 0], [(-1109909937147646229)]], [[659547212601632853, 0, 0], [123338640951940758, 0], [27618373610977554]], [[(-82375538508277296), 0, 0, 0], [(-14919110603834878), 0, 0], [(-3052945413139972), 0], [(-705873021171314)]], [[10458606598893182, 0, 0, 0, 0], [1881615020430643, 0, 0, 0], [375951764520505, 0, 0], [78792155638552, 0], [18339109742681]]], r := 4728414874720128, ok := true }, T := { p := [[[7493989779944505344]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[11015808378944575084]], [[289683226242091957, 0], [152834155400037642]], [[(-7387658234495761), 0, 0], [4805756026401904, 0], [(-2285375501167842)]], [[304539690711037, 0, 0, 0], [(-212376078995697), 0, 0], [(-43459197632323), 0], [13173398688210]], [[(-20198139100379), 0, 0, 0, 0], [8159567627997, 0, 0, 0], [(-365369305247), 0, 0], [341679841789, 0], [(-217941643249)]]], r := 55059474411809, ok := true }, de := { p := [[[(-36649961225872081863)]], [[1869334247320132042, 0], [382527857559718141]], [[(-115588686315281108), 0, 0], [3215980624791995, 0], [(-4840247161783882)]], [[10221662116467401, 0, 0, 0], [27037328588345, 0, 0], [5532735193754, 0], [87589054350378]], [[(-1012245432798476), 0, 0, 0, 0], [227307693199, 0, 0, 0], [435141357794, 0, 0], [9518452471, 0], [(-1774966856541)]]], r := 616368589970539, ok := true }, dde := { p := [[[(-236503261066355547328)]], [[29247954233043485476, 0], [5985102603672991249]], [[(-3879653562537495618), 0, 0], [(-797326633195637593), 0], [(-162459516959613358)]], [[512266538099466536, 0, 0, 0], [104769226572549189, 0, 0], [21439262580483038, 0], [4389593506049157]], [[(-67659026167785281), 0, 0, 0, 0], [(-13846008677535454), 0, 0, 0], [(-2834229331506347), 0, 0], [(-579798130248448), 0], [(-118639734102492)]]], r := 15123298741534126, ok := true }, nJu := { p := [[[(-73299922451744163726)]], [[3738668494640264085, 0], [765055715119436282]], [[(-231177372630562216), 0, 0], [6431961249583991, 0], [(-9680494323567764)]], [[20443324232934802, 0, 0, 0], [54074657176690, 0, 0], [11065470387509, 0], [175178108700756]], [[(-2024490865596951), 0, 0, 0, 0], [454615386399, 0, 0, 0], [870282715589, 0, 0], [19036904942, 0], [(-3549933713082)]]], r := 1232737179941072, ok := true }, Jd1 := { p := [[[(-473006522132711094655)]], [[58495908466086970953, 0], [11970205207345982499]], [[(-7759307125074991236), 0, 0], [(-1594653266391275185), 0], [(-324919033919226715)]], [[1024533076198933073, 0, 0, 0], [209538453145098379, 0, 0], [42878525160966077, 0], [8779187012098315]], [[(-135318052335570562), 0, 0, 0, 0], [(-27692017355070908), 0, 0, 0], [(-5668458663012694), 0, 0], [(-1159596260496895), 0], [(-237279468204984)]]], r := 30246597483068242, ok := true }, term0 := { p := [[[5524687026053585027716]], [[(-1352440580940447189627), 0], [(-247845075313453933986)]], [[262283346908932231451, 0, 0], [63121884485499955347, 0], [9413628932099597427]], [[(-45674410648822806336), 0, 0, 0], [(-12343026004545886734), 0, 0], [(-2422237282773588302), 0], [(-327774684447607681)]], [[7489857575629795401, 0, 0, 0, 0], [2159862315105890190, 0, 0, 0], [475643226651868488, 0, 0], [84842622376810224, 0], [10841215287670230]]], r := 2232476004252837088, ok := true }, r0 := { p := [[[102675443752347037613]], [[(-13994756665283744445), 15024595372586751748], [(-1113033618379543447)]], [[1700462598312634856, (-1966917700912065139), 465959437249605717], [75644003330727342, (-181150084365841856)], [37787179649885849]], [[(-200298641788411342), 233805609411407957, (-49414179746751992), (-7622036440762058)], [(-2937750349014171), 14535098708182933, (-8238834482264003)], [(-4276296017739453), 5615629286139837], [(-853390108661588)]], [[23880791030803486, (-27279631251864489), 5185540273449431, 1677307657840711, (-60451328375580)], [(-90221875355873), (-979666756602649), 911291881285252, (-62498682013818)], [453967131824848, (-603794139681902), 190554450590735], [82105251324918, (-131935570087886)], [22900719446466]]], r := 44867601522126292, ok := true }, r1 := { p := [[[502899368153146500626]], [[(-58998645805311729527), 0], [(-7624011869469200985)]], [[6812004925375193603, 0, 0], [673175217985461452, 0], [207488658523289755]], [[(-797303436418276678), 0, 0, 0], [(-54574754071193110), 0, 0], [(-21112222239973440), 0], [(-5064928622950149)]], [[96132125074218311, 0, 0, 0, 0], [4872173637714591, 0, 0, 0], [2059159871396334, 0, 0], [482052897335634, 0], [132250706235872]]], r := 168721399819385256, ok := true }, r2 := { p := [[[631434417337969940634]], [[(-93155321242160835274), 18135162836475749496], [(-41845784242964452404)]], [[11783439857617598536, (-2134546216295107331), 32771033738118019], [5846519628998878411, (-206820641725851640)], [1570442218306360130]], [[(-1468481494670085280), 249340145259867756, 5231072257073528, (-941038975905314)], [(-731269972605873132), 15139118882267865, 1385162222329774], [(-214124090220566566), 6760837717046731], [(-54706519367435382)]], [[184537951500359138, (-30217575157859541), (-422002337943914), (-5238113784749), 16306686921567], [91564396002855711, (-1675128160264661), 261444525115519, (-103269470723460)], [26773492978699131, (-995706550164353), 137359308116846], [7509437814612007, (-272191449274589)], [1815965390034727]]], r := 837090576785189099, ok := true }, r3 := { p := [[[5391314947768005394839]], [[(-1374425090189863328964), 160251455743598489432], [(-346996758876602852071)]], [[267014931454547103914, (-37288644029906897491), (-112910529400039645)], [89480040092329747249, (-3926228878027471307)], [14713925871601712803]], [[(-46582739046270703928), 7232517333467635348, 16698436564860288, 2303896934164749], [(-17651237745443540552), 1042876374198567502, (-17316565567889733)], [(-3859756740398600869), 123410713444628544], [(-546256613030121598)]], [[7650369364310727128, (-1264676283966771068), 645436741428017, (-677387526769874), (-37015581732269)], [3103660151627632498, (-202478710787193157), 1024899949171336, 487239003066520], [762613839029337664, (-28085579704752030), (-720967967685715)], [143024697830772588, (-2899889529952874)], [18685759717199312]]], r := 916697558242054575997, ok := true }, eta := { p := [[[(-1603436830059445159437)]], [[227899813193278421372, 0], [58764723867526258765]], [[(-29959624731533024916), 0, 0], [(-8253969115180865894), 0], [(-2077647600369925416)]], [[3857270480728892594, 0, 0, 0], [1045333796793485523, 0, 0], [287803748370722577, 0], [68069366110404220]], [[(-497167658986298666), 0, 0, 0, 0], [(-132366458357642712), 0, 0, 0], [(-36282130152795501), 0, 0], [(-9291447735235957), 0], [(-2157623938499325)]]], r := 666404028746003647, ok := true } }
theorem sB_2 : stageB c2 w2 = true := by decide +kernel
theorem s0_2 : stageC0 w2 q2 = true := by decide +kernel
theorem s1_2 : stageC1 w2 q2 = true := by decide +kernel
theorem s2_2 : stageC2 w2 q2 = true := by decide +kernel
theorem s3_2 : stageC3 w2 q2 = true := by decide +kernel
theorem sE_2 : stageE w2 q2 = true := by decide +kernel
theorem sF_2 : stageF w2 = true := by decide +kernel
theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

noncomputable def c3 : Cell := { bc := 5332261958806667264, bh := 144115188075855872, tc := 8646911284551352320, th := 576460752303423488, sc := 2558044588346441728, sh := 252201579132747776 }
noncomputable def q3 : Cert := { V0 := [[[3761285721089569074]], [[(-113905043646779118), 235951780358540936], [47494828727619443]], [[2470148417606523, (-6263353856222293), (-1377859805754161)], [(-1523626235682278), 2611622006697367], [51022725691524]], [[(-86963402848681), 96614519673595, 117803760462313, (-20104415101453)], [44292802551265, (-51079410243519), (-49120471293419)], [(-2474938895874), (-4012031273480)], [3980692920093]], [[3918624067417, (-2727931889910), (-5579483168488), 1100708515927, 435197414415], [(-1883357089285), 235496546796, 4098259139664, (-458960909626)], [181944975086, 520697522036, (-578667154845)], [(-123944657056), 178632751967], [(-33926978199)]]], r0 := 32141798647164, V1 := [[[7310394529904266672]], [[(-185064575066059931), 0], [77166120260388762]], [[2703465362617262, 0, 0], [(-1383142886838664), 0], [(-144836399093110)]], [[(-84641903011263), 0, 0, 0], [13434932881860, 0, 0], [11679721873473, 0], [5989914518553]], [[3910730502672, 0, 0, 0, 0], [(-712132746583), 0, 0, 0], [(-282364745666), 0, 0], [(-115087755937), 0], [(-88998459649)]]], r1 := 37851103089064, V2 := [[[11982566207226243645]], [[(-113544651114028554), 83054486000791442], [(-211353165568252074)]], [[1795655369442447, (-372401428088844), (-841392498833440)], [(-3099517994527265), 5396810496178682], [(-1349237361300892)]], [[(-56846650007679), (-38354341601545), 26048549657942, 6853569507019], [82000281958782, (-61739414990587), (-74903825861330)], [19362170148846, 110059801480550], [(-9249594631945)]], [[2716089749859, 1120517994994, 3092773604, (-446469717014), (-39360112979)], [(-2688735420241), (-1938351662843), 3230652026165, 676558639557], [837777183001, (-3703976277376), (-2121055000568)], [873772549514, 515629103600], [27355888998]]], r2 := 130772275523900, V3 := [[[16245227047644458838]], [[(-204679280009096472), 60553508813857002], [(-88410134227891149)]], [[1404528284807307, 4546290937418155, (-1483012029639379)], [(-7699673019047065), 4728518066294571], [(-1121799027662116)]], [[4334043976621, (-151901744294782), (-78384688336277), 34196838080393], [113881344447628, 321144967584109, (-169281538593742)], [(-74454536434255), 144605602946329], [(-12303233174344)]], [[(-561333244536), 463034170388, 6381174839633, 916646078830, (-754385811137)], [34873886645, (-14935252184260), (-7351942534264), 5080051333127], [3859394490826, 7476929248360, (-8096668393900)], [(-361527343102), 2469551895545], [(-104720751592)]]], r3 := 9184884387307644, Vm := [[[13682062022732515893]], [[(-121311472160433265), 0], [(-101211120199477204)]], [[1032463958147700, 0, 0], [(-3753631891163144), 0], [935964487151664]], [[(-39242492836709), 0, 0, 0], [27735908273016, 0, 0], [(-4470201725518), 0], [6916797282224]], [[2123139163219, 0, 0, 0, 0], [(-1206188371067), 0, 0, 0], [(-264123100445), 0, 0], [338285440303, 0], [32193849362]]], rm := 74655369645731 }
noncomputable def w3 : Wit := { Z0 := { p := [[[3878419538186933664]], [[(-124819725484138854), 258561302545795577], [52045908538355445]], [[3058716542609906, (-8321315032275924), 0], [(-1963063273730452), 3469727235890363], [117089316824298]], [[(-115020274005176), 203914436173993, 0, 0], [69896100956675, (-130870884915364), 0], [(-9279988680089), 7805954454953], [4817079610666]], [[5310217387252, (-7668018267012), 0, 0, 0], [(-3225218734849), 4659740063778, 0, 0], [628386872343, (-618665912006), 0], [(-213816908703), 321138640711], [(-25114047748)]]], r := 5733246819497, ok := true }, Z1 := { p := [[[8273961681465458484]], [[(-266282081032829555), 0], [111031271548491616]], [[6525261957567800, 0, 0], [(-4187868317291630), 0], [249790542558504]], [[(-245376584544375), 0, 0, 0], [149111682040906, 0, 0], [(-19797309184190), 0], [10276436502755]], [[11328463759473, 0, 0, 0, 0], [(-6880466634344), 0, 0, 0], [1340558660999, 0, 0], [(-456142738567), 0], [(-53576635195)]]], r := 9561320271487, ok := true }, Z2 := { p := [[[17898061173852619524]], [[(-353481844302442395), 258561302545795577], [(-657974691288604214)]], [[10485752997160002, (-8321315032275924), 0], [8576179125882689, 3469727235890363], [12762138736367801]], [[(-412904037427029), 203914436173993, 0, 0], [(-218485500205754), (-130870884915364), 0], [(-168737066866899), 7805954454953], [(-335204333220761)]], [[19777182595051, (-7668018267012), 0, 0, 0], [7174955391335, 4659740063778, 0, 0], [3326493332413, (-618665912006), 0], [4592911145632, 321138640711], [8428957489297]]], r := 20923304989805, ok := true }, Z3 := { p := [[[49810219213281120599]], [[(-3998147826923689255), 1182835310276483314], [(-1726978842340882099)]], [[358413394080262001, (-107030778605474581), 0], [135524906802477240, 7774897723801657], [39839672360478008]], [[(-33458921700597909), 9413070241424900, 0, 0], [(-12416665833914602), (-501202539668861), 0], [(-3303033512335496), (-51782227785406)], [(-1010446107576457)]], [[3174299630863133, (-876420257461195), 0, 0, 0], [1167483229795559, 39460960952153, 0, 0], [303347270109960, 4890253317330, 0], [84471652454608, 838257183080], [26159307949232]]], r := 1488928260277973, ok := true }, iE := { p := [[[33231743136392736854]], [[(-542013911273015801), 0], [(-452206490834543751)]], [[17604827151526154, 0, 0], [4907318603786118, 0], [13225061926527422]], [[(-706094846629578), 0, 0, 0], [(-31540567513677), 0, 0], [(-196219792598879), 0], [(-316159573877183)]], [[34292065677745, 0, 0, 0, 0], [(-1499396390882), 0, 0, 0], [5227342441882, 0, 0], [4126326032539, 0], [8329666833101]]], r := 34072714996608, ok := true }, iHu := { p := [[[76012301177206212445]], [[(-5671552350439278337), 0], [(-1554749872128141974)]], [[514885547754402359, 0, 0], [129007263814865586, 0], [38692596208016279]], [[(-48148427469463691), 0, 0, 0], [(-11765318078896285), 0, 0], [(-3225241635527547), 0], [(-991877095282765)]], [[4571871075503330, 0, 0, 0, 0], [1109244820788444, 0, 0, 0], [297127259219413, 0, 0], [83357480383342, 0], [25818339872712]]], r := 1834520203855447, ok := true }, T := { p := [[[8646911284551352320]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[10239678536401797624]], [[167010445131164999, 0], [139338134602670234]], [[(-2700604231418527), 0, 0], [3033155656589669, 0], [(-2178964057538233)]], [[85046070342802, 0, 0, 0], [(-76037244234913), 0, 0], [(-20844186643548), 0], [12315792526057]], [[(-4200041200135), 0, 0, 0, 0], [2290176742705, 0, 0, 0], [(-85816724803), 0, 0], [172102099849, 0], [(-206242852825)]]], r := 8393961575837, ok := true }, de := { p := [[[(-42259446069946058995)]], [[1366693427878336813, 0], [374653410731127081]], [[(-64558833196747335), 0, 0], [1542469811622533, 0], [(-4851464321414459)]], [[4251025484047189, 0, 0, 0], [6350437635478, 0, 0], [1740853560305, 0], [87572845691872]], [[(-314312547813161), 0, 0, 0, 0], [26145119897, 0, 0, 0], [96567517349, 0, 0], [1964752305, 0], [(-1774990600498)]]], r := 137710529588096, ok := true }, dde := { p := [[[(-345820928530635835380)]], [[32671256311830373799, 0], [8956213120231492439]], [[(-3226971499488609139), 0, 0], [(-886220690133474461), 0], [(-242500310504048484)]], [[318127986617502933, 0, 0, 0], [87195599060569870, 0, 0], [23903040669113766, 0], [6553565295448878]], [[(-31364830432132535), 0, 0, 0, 0], [(-8598162639992621), 0, 0, 0], [(-2357219013309720), 0, 0], [(-646134343080782), 0], [(-177123947454773)]]], r := 5260830581481691, ok := true }, nJu := { p := [[[(-84518892139892117990)]], [[2733386855756673627, 0], [749306821462254162]], [[(-129117666393494670), 0, 0], [3084939623245067, 0], [(-9702928642828917)]], [[8502050968094379, 0, 0, 0], [12700875270956, 0, 0], [3481707120610, 0], [175145691383744]], [[(-628625095626321), 0, 0, 0, 0], [52290239794, 0, 0, 0], [193135034698, 0, 0], [3929504611, 0], [(-3549981200995)]]], r := 275421059176184, ok := true }, Jd1 := { p := [[[(-691641857061271670759)]], [[65342512623660747598, 0], [17912426240462984878]], [[(-6453942998977218278), 0, 0], [(-1772441380266948921), 0], [(-485000621008096968)]], [[636255973235005867, 0, 0, 0], [174391198121139741, 0, 0], [47806081338227532, 0], [13107130590897757]], [[(-62729660864265070), 0, 0, 0, 0], [(-17196325279985242), 0, 0, 0], [(-4714438026619439), 0, 0], [(-1292268686161564), 0], [(-354247894909546)]]], r := 10521661162963376, ok := true }, term0 := { p := [[[11737418089445957111412]], [[(-2202788719079276252320), 0], [(-539267628660121477379)]], [[320981792900204298145, 0, 0], [103689091671033749214, 0], [20623656208331865718]], [[(-41876393100743988809), 0, 0, 0], [(-15201861167610521129), 0, 0], [(-3994934348190484418), 0], [(-720892109157767872)]], [[5137300728629991102, 0, 0, 0, 0], [1989783703051300499, 0, 0, 0], [587266646257962257, 0, 0], [140209281771344224, 0], [23902290071834149]]], r := 1247923580657918749, ok := true }, r0 := { p := [[[199216883570346767864]], [[(-18466148842562317253), 24384672803134322405], [(-1812549570016711010)]], [[1579441764636454686, (-2151443037363591355), 551050136459458306], [66531800855111290, (-271635123922871538)], [68682360698770294]], [[(-136767731093864796), 180866632991190074, (-35937012954096502), (-14020254347434589)], [(-796605678999164), 14162815239099499, (-11977248817307836)], [(-5192671207907116), 8594329922886417], [(-1492767807322159)]], [[12234528679163187, (-15659193224039740), 2726402118765452, 1728052712711447, 6802480487029], [(-137059299248496), (-714889131639169), 953164338176739, (-75187029352867)], [397400705920857, (-600862112383201), 232181947851833], [92391905342101, (-201185904608912)], [40508838337063]]], r := 22856491990583004, ok := true }, r1 := { p := [[[710874348503169401363]], [[(-58854910097516270730), 0], [(-9750509602965704986)]], [[4946458982859609991, 0, 0], [541890083265009952, 0], [277950499003988695]], [[(-433757672268121105), 0, 0, 0], [(-30980362495629531), 0, 0], [(-18995245812355758), 0], [(-6632900241423455)]], [[39476497335928272, 0, 0, 0, 0], [2126042871750231, 0, 0, 0], [1370934880434648, 0, 0], [411951956920559, 0], [174094723538070]]], r := 48461870047748567, ok := true }, r2 := { p := [[[1022984875919010251758]], [[(-103575263036992704896), 25771566198819960496], [(-63649461603868709481)]], [[9504146234464281932, (-2148950794100749493), 11401460407781495], [6238478922188901264, (-259026849667550040)], [2370778843248422080]], [[(-879787262656223829), 187437451840565716, 4074856485964126, (-732460735514805)], [(-574275372980560077), 15881343129188893, (-124066536895859)], [(-229180732403808051), 10666378834476036], [(-82570985280542946)]], [[82831352825549378, (-17078548795998889), (-233804184490204), (-29143137588225), 16892422192319], [53766457456757028, (-1308434116738399), 248993917827953, (-87359128704947)], [21072122631321530, (-941056049550353), 94289898228308], [7938360395085246, (-312916666770827)], [2705160954437499]]], r := 342640301801152441, ok := true }, r3 := { p := [[[12376098853390561438907]], [[(-2365585011930239061990), 331113297562647134025], [(-779730645790786496234)]], [[345435198035164487912, (-60801807199482319133), (-137449789910569012)], [151638050608179643172, (-8759899811562101081)], [33132578476936632658]], [[(-45135132239991921007), 8876945906030926576, 10784783080247745, 2858588365165789], [(-22350696885985172602), 1680801494691008462, (-13974600650600893)], [(-6489068103660295624), 247018315965710858], [(-1223074439011804579)]], [[5542305960381094680, (-1158822967656962187), (-1490302400536724), (-90156689397708), (-75287077038972)], [2932543909896151482, (-242018257306431316), (-510737437077190), 527902871437909], [956873173242855799, (-44546679272615011), (-565226964408145)], [239675468468699521, (-6417588021931728)], [41864549498089435]]], r := 922436831775471199507, ok := true }, eta := { p := [[[(-2449441979006219883234)]], [[250765676768712404147, 0], [88978833969153404785]], [[(-24098595793915429647), 0, 0], [(-8857208649683532655), 0], [(-3129168989778111755)]], [[2305431869226116641, 0, 0, 0], [828327372736295055, 0, 0], [307736952234126858, 0], [101877805810562582]], [[(-222071860496393194), 0, 0, 0, 0], [(-78515488164320793), 0, 0, 0], [(-28648429492546660), 0, 0], [(-9861263560459622), 0], [(-3215894584381380)]]], r := 158519376832518319, 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

noncomputable def c4 : Cell := { bc := 5332261958806667264, bh := 144115188075855872, tc := 8646911284551352320, th := 576460752303423488, sc := 3062447746611937280, sh := 252201579132747776 }
noncomputable def q4 : Cert := { V0 := [[[3542717152666349950]], [[(-104957451986689321), 223791365590402010], [44611006804731468]], [[2028049004603815, (-5906395627204917), (-1162873238231847)], [(-1366468901278299), 2510448286702791], [46732180682854]], [[(-62425719868539), 82576369862781, 97963225536281, (-17942812818236)], [34853585576293, (-50076593338905), (-41638188030392)], [(-1846633431548), (-3070028656275)], [3745125136214]], [[2386997281099, (-2011856975018), (-4405808538207), 1055708791870, 334392337369], [(-1312251140503), 262228629817, 3411575187524, (-448717372674)], [135237392150, 426102270400, (-497594897701)], [(-112035602408), 177171530920], [(-31954622596)]]], r0 := 18925697213068, V1 := [[[6950458327233783866]], [[(-175156793000458498), 0], [74448462081847748]], [[2274464561566895, 0, 0], [(-1336811794251359), 0], [(-122545230706712)]], [[(-60455526844120), 0, 0, 0], [9975680815519, 0, 0], [10639391721051, 0], [5766438523516]], [[2321465908555, 0, 0, 0, 0], [(-465235651178), 0, 0, 0], [(-240319662387), 0, 0], [(-108585794025), 0], [(-83477254338)]]], r1 := 19325605254668, V2 := [[[11762243703876314895]], [[(-106968284876393437), 82164584532772173], [(-217243982263589213)]], [[1509120938795504, (-513633910454693), (-789383216945285)], [(-2800410592620218), 5266197445357800], [(-1307474148607062)]], [[(-40147397873493), (-32541984296710), 25914409864405, 6003640153817], [68294638440627, (-68586212122735), (-68602012059365)], [22255938420629, 102747469062132], [(-7553047963209)]], [[1592218847716, 838963090871, (-66532457745), (-403834321048), (-30591066935)], [(-1943100253478), (-1506295849167), 3069369797632, 562887811131], [619670834605, (-3603298094230), (-1808914515895)], [821968427326, 317540174728], [50338208770]]], r2 := 87578868986804, V3 := [[[15841513023961125322]], [[(-199025323957348435), 69043095068618260], [(-103354478397120386)]], [[1418809283966448, 3946011338405079, (-1615117245752413)], [(-7245300405912595), 5312114341339383], [(-1255496030005203)]], [[679444843908, (-147847473348626), (-54163685994533), 35291300476860], [112952920145359, 263018826797420, (-180786455445525)], [(-59369955198345), 157048324335534], [(-12713636371406)]], [[(-370090388830), 855364017676, 5717600386767, 204018470156, (-731259878937)], [(-318512331300), (-14086497980324), (-4231096987837), 5109489033821], [3668893056269, 5013697820938, (-8332385892588)], [(-55928173914), 2475592756863], [(-87843831029)]]], r3 := 4635716107101448, Vm := [[[13443285280401364911]], [[(-117593580408767286), 0], [(-108616121857623358)]], [[839279972313055, 0, 0], [(-3655279227802150), 0], [925974224135599]], [[(-26355679754010), 0, 0, 0], [21848468101889, 0, 0], [(-5517023886863), 0], [7572758255607]], [[1210307033729, 0, 0, 0, 0], [(-795231784038), 0, 0, 0], [(-259561827258), 0, 0], [317843936586, 0], [41947340148]]], rm := 41884651116059 }
noncomputable def w4 : Wit := { Z0 := { p := [[[3640171540602197188]], [[(-113815272746892777), 242678102706813145], [48375925776455761]], [[2476575013057186, (-7587684849792852), 0], [(-1717577366554062), 3225061718430384], [100785264997465]], [[(-81772210067814), 165105000870479, 0, 0], [53856581549007, (-114505157770271), 0], [(-7139783977476), 6719017666497], [4424110440222]], [[3231819578631, (-5451480671188), 0, 0, 0], [(-2209488753495), 3590438769933, 0, 0], [454112687203, (-475985598499), 0], [(-180819192487), 294940696014], [(-24877959895)]]], r := 3085835849459, ok := true }, Z1 := { p := [[[7765699286618020667]], [[(-242805915193371258), 0], [103201974989772291]], [[5283360027855332, 0, 0], [(-3664165048648666), 0], [215008565327927]], [[(-174447381478003), 0, 0, 0], [114894040637882, 0, 0], [(-15231539151948), 0], [9438102272475]], [[6894548434412, 0, 0, 0, 0], [(-4713576007456), 0, 0, 0], [968773732699, 0, 0], [(-385747610639), 0], [(-53072981109)]]], r := 4733129482302, ok := true }, Z2 := { p := [[[17230022409417630786]], [[(-315937341753990139), 242678102706813145], [(-641643327718310932)]], [[8408894917943952, (-7587684849792852), 0], [7779638582909063, 3225061718430384], [12437259451143746]], [[(-289801221254481), 165105000870479, 0, 0], [(-181711896487139), (-114505157770271), 0], [(-156473017430800), 6719017666497], [(-326413195512740)]], [[11886858582194, (-5451480671188), 0, 0, 0], [5237537037941, 3590438769933, 0, 0], [2829206228044, (-475985598499), 0], [4209692479040, 294940696014], [8212070652879]]], r := 10692329215755, ok := true }, Z3 := { p := [[[43022539981643943235]], [[(-2884152606986311431), 1000530076661165342], [(-1497749544558694113)]], [[215047309846819396, (-77754135987025727), 0], [97000777208213727, 6906525992644360], [34254499750337790]], [[(-16742523213415801), 5656047967948561, 0, 0], [(-7421707742050212), (-377240614798310), 0], [(-2362968826438067), (-43323560932796)], [(-867739474597799)]], [[1325392971477734, (-439003921589516), 0, 0, 0], [582253744031418, 24210456485725, 0, 0], [180860574509624, 3667471631857, 0], [60315461916574, 713810963777], [22439662737633]]], r := 594940755661288, ok := true }, iE := { p := [[[32212979837192138900]], [[(-479104163572378931), 0], [(-442527866165664055)]], [[14061795330101962, 0, 0], [4767320636787447, 0], [12852091916581403]], [[(-493105804294321), 0, 0, 0], [(-37577306081902), 0, 0], [(-177407640897232), 0], [(-308203543126229)]], [[20515648008447, 0, 0, 0, 0], [(-610968653422), 0, 0, 0], [4238099278962, 0, 0], [3836485410388, 0], [8109672892270]]], r := 16809354707737, ok := true }, iHu := { p := [[[66404951304833097700]], [[(-4071918381465897567), 0], [(-1336343870365255995)]], [[308637843739474888, 0, 0], [92528975928376236, 0], [33242027116735055]], [[(-24076952627136153), 0, 0, 0], [(-7021981110297593), 0, 0], [(-2304511175194180), 0], [(-851057695657430)]], [[1908045301196599, 0, 0, 0, 0], [552584545316552, 0, 0, 0], [177133573906636, 0, 0], [59516455328819, 0], [22134276362674]]], r := 719383624881887, ok := true }, T := { p := [[[8646911284551352320]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[10563517210787766492]], [[157111360179525974, 0], [145116991787793759]], [[(-2274527552181994), 0, 0], [2753319835466189, 0], [(-2220998547690945)]], [[59290641498131, 0, 0, 0], [(-64572479337931), 0, 0], [(-21191740323260), 0], [12659579123680]], [[(-2447912099006), 0, 0, 0, 0], [1593873968334, 0, 0, 0], [(-87971995059), 0, 0], [171669167442, 0], [(-210921316538)]]], r := 4120759990743, ok := true }, de := { p := [[[(-39754633593534417767)]], [[1151069016677985915, 0], [377763963002427811]], [[(-45007777774766503), 0, 0], [1568188783921220, 0], [(-4847590143597859)]], [[2477627294525613, 0, 0, 0], [6509927634364, 0, 0], [2136462737147, 0], [87577685126161]], [[(-153009334997038), 0, 0, 0, 0], [27024270445, 0, 0, 0], [101275448656, 0, 0], [2910665523, 0], [(-1774984537722)]]], r := 55125267548123, ok := true }, dde := { p := [[[(-291260459756789516866)]], [[22777063507699595080, 0], [7475098062372453976]], [[(-1880777402015798029), 0, 0], [(-618890786829299232), 0], [(-202570276673933578)]], [[154866714723796947, 0, 0, 0], [50811307437633381, 0, 0], [16675525606945317, 0], [5474135843018574]], [[(-12753815943200143), 0, 0, 0, 0], [(-4185700430456841), 0, 0, 0], [(-1373888914484652), 0, 0], [(-450823416616474), 0], [(-147950620768116)]]], r := 1949350928844903, ok := true }, nJu := { p := [[[(-79509267187068835534)]], [[2302138033355971830, 0], [755527926004855622]], [[(-90015555549533006), 0, 0], [3136377567842441, 0], [(-9695180287195718)]], [[4955254589051227, 0, 0, 0], [13019855268729, 0, 0], [4272925474294, 0], [175155370252323]], [[(-306018669994075), 0, 0, 0, 0], [54048540890, 0, 0, 0], [202550897313, 0, 0], [5821331047, 0], [(-3549969075443)]]], r := 110250535096237, ok := true }, Jd1 := { p := [[[(-582520919513579033731)]], [[45554127015399190160, 0], [14950196124744907953]], [[(-3761554804031596057), 0, 0], [(-1237781573658598464), 0], [(-405140553347867156)]], [[309733429447593895, 0, 0, 0], [101622614875266763, 0, 0], [33351051213890634, 0], [10948271686037149]], [[(-25507631886400286), 0, 0, 0, 0], [(-8371400860913681), 0, 0, 0], [(-2747777828969304), 0, 0], [(-901646833232947), 0], [(-295901241536231)]]], r := 3898701857689797, ok := true }, term0 := { p := [[[8347194924314158381287]], [[(-1294900445193045900024), 0], [(-379940854538481500900)]], [[157186772142112432534, 0, 0], [60739506131828629706, 0], [14489521081309269945]], [[(-17104624156493351798), 0, 0, 0], [(-7425440448264395431), 0, 0], [(-2336475091484190218), 0], [(-505683151613552699)]], [[1751205873396486537, 0, 0, 0, 0], [811170172265527132, 0, 0, 0], [286565781715591446, 0, 0], [81936481703484179, 0], [16750121176999968]]], r := 396065541768173799, ok := true }, r0 := { p := [[[167673655573396486347]], [[(-13471478299688014759), 20699020924041114951], [(-1683502226044009676)]], [[982458256137440087, (-1579283655634320464), 488458270790704020], [62210135625900607, (-245876813024732989)], [59661022177267007]], [[(-71280836734338808), 112631440873007754, (-27337532864173340), (-11066288575488305)], [(-1264674258195285), 11724588371463170, (-10334318307266753)], [(-3924630787791412), 7541123374584014], [(-1328137493716703)]], [[5303787347480292, (-8133449442319752), 1691890336254639, 1260504724437336, (-15165605807386)], [(-35713667699588), (-520136447211224), 708627359159248, (-61095558028675)], [252160205027216, (-462418461064020), 209905168688622], [73469107335114, (-178315591580594)], [35749559618877]]], r := 10425342015182259, ok := true }, r1 := { p := [[[610012877943418394710]], [[(-43250678616410101111), 0], [(-8775957842812129282)]], [[3062752138197678240, 0, 0], [439020996778891478, 0], [244681117405090267]], [[(-223624602766523769), 0, 0, 0], [(-21369280007670337), 0, 0], [(-14598859145192169), 0], [(-5902644023884905)]], [[16900450972178413, 0, 0, 0, 0], [1198857902289112, 0, 0, 0], [879497846990551, 0, 0], [324344406723594, 0], [154533293751379]]], r := 19497629865170165, ok := true }, r2 := { p := [[[847925905488628178639]], [[(-73978525478504198017), 22108267095350195965], [(-53108165639201457514)]], [[5724607115010418910, (-1562892036563169320), 18738829620908953], [4454724563317685488, (-231719930404138489)], [1983448689459036871]], [[(-442824638561932856), 113903961715253617, 3314728979764741, (-779845318629857)], [(-344095633571843391), 11754532590774757, 318452041333407], [(-163720551780712157), 9030432777232386], [(-69131514216100063)]], [[34735004367468728, (-8640214396796866), (-154757880570284), (-18759730837562), 15958741083527], [26860696864294682, (-810219231832493), 196292743822259, (-87972843217875)], [12630240312490149, (-711816701657079), 99921562469510], [5691471220661364, (-284068882516920)], [2272265175066391]]], r := 175518843274733627, ok := true }, r3 := { p := [[[8737255144784922789177]], [[(-1389037363297508160828), 237585212180489165886], [(-547062737642711301335)]], [[168964497677430494841, (-35700288136293530311), (-120072926453922703)], [88544526143199976464, (-6165142964053239909)], [23177103715791959257]], [[(-18418290291964734497), 4344126228143643488, 7287437405478724, 2616816052117206], [(-10896097216367044417), 994519669027097088, (-14682224023134841)], [(-3788175812302330085), 178393319112846402], [(-855462916745636536)]], [[1887902555420555644, (-473374786272603406), (-426554639946175), (-153846012156687), (-62631330707056)], [1193955924138790132, (-119240497486691880), (-196116529451548), 505331728750564], [466401133823837705, (-26259991501718082), (-592057572789731)], [139840852821628456, (-4527260855328509)], [29256738317003794]]], r := 250144214562977117519, ok := true }, eta := { p := [[[(-2028838129995050218663)]], [[176324667663190465372, 0], [74050734606546827517]], [[(-14267820557273230616), 0, 0], [(-6292019787490144517), 0], [(-2610104783414580595)]], [[1141482656183605793, 0, 0, 0], [493201814832845389, 0, 0], [218959316381856554, 0], [85219985260928210]], [[(-91749853596709787), 0, 0, 0, 0], [(-38967495502212896), 0, 0, 0], [(-17082194798062873), 0, 0], [(-7038310053768694), 0], [(-2695007468950722)]]], r := 69777906877607078, ok := true } }
theorem sB_4 : stageB c4 w4 = true := by decide +kernel
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 := 5332261958806667264, bh := 144115188075855872, tc := 8646911284551352320, th := 576460752303423488, sc := 3819052484010180608, sh := 504403158265495552 }
noncomputable def q5 : Cert := { V0 := [[[3244582220731071296]], [[(-188507954019653088), 206765995542141159], [40793747242781074]], [[6285269148598157, (-10917699145801250), (-904630402012054)], [(-2375485451956076), 2362626350398508], [42256918479415]], [[(-329769743680440), 270090410787878, 150793736241654, (-14927186510731)], [101743026620785, (-96926150760139), (-32632265275106)], [(-2363645694579), (-1951395066346)], [3431047874417]], [[20735486180743, (-11161990041578), (-12810186661364), 1899972331990, 225360526347], [(-6655519164936), 1083390312821, 5268500340375, (-411160322029)], [360150198001, 652615269101, (-398255229677)], [(-195976716481), 172641757566], [(-29189732062)]]], r0 := 142218870473980, V1 := [[[6443990676583134040]], [[(-325858377140107078), 0], [70516834916209877]], [[7326627495413762, 0, 0], [(-2574949387611975), 0], [(-92649510214614)]], [[(-320809208945187), 0, 0, 0], [27012044944333, 0, 0], [18665548243194, 0], [5452973416725]], [[19633561165888, 0, 0, 0, 0], [(-2195035079263), 0, 0, 0], [(-793730855220), 0, 0], [(-201433284403), 0], [(-75785771890)]]], r1 := 209620544768404, V2 := [[[11453949676581220255]], [[(-197703831566391456), 80351457234947751], [(-225077896646336384)]], [[4867714841840585, (-1377654733254582), (-712478695520770)], [(-4872940223456770), 5048403275027902], [(-1235899932347019)]], [[(-210294964076573), (-104922257785054), 50567141291484, 4882701446728], [215859735870468, (-152298943639129), (-59774190637376)], [50453257432915, 92219965415762], [(-5212129559499)]], [[13259812446306, 4697870622473, (-553960785922), (-688818474921), (-20472607237)], [(-10454451389150), (-4177231442535), 5628618406026, 422054622983], [1541285234666, (-6816470933915), (-1408220963374)], [1475485696194, 69024058931], [76938143887]]], r2 := 528195201696840, V3 := [[[15257197823435225305]], [[(-381058008895801730), 79576233900757884], [(-124084932713213364)]], [[5632899257270832, 6170827876940157, (-1729311006724917)], [(-13158914859630614), 5978964362666053], [(-1401708407987792)]], [[(-21780218272043), (-554206979380791), (-46051851681571), 34643465705237], [434109583094174, 366277586258562, (-187524167184835)], [(-77009998251599), 167225676506292], [(-12294718760265)]], [[(-3424185019102), 9352706206895, 18637054701235, (-1163855805576), (-647759373918)], [(-5056872948029), (-50001408152428), (-874647525611), 4805422775880], [13081236691639, 3777033975620, (-8123345804077)], [635144680782, 2282299366408], [(-48890485398)]]], r3 := 23339971024652288, Vm := [[[13097431516129405543]], [[(-226319596479032934), 0], [(-119404098149071148)]], [[2616064427400897, 0, 0], [(-7084366377279106), 0], [907101770636610]], [[(-128016440639276), 0, 0, 0], [65345363369972, 0, 0], [(-14120824721377), 0], [8481344453794]], [[9698101077760, 0, 0, 0, 0], [(-3741133882448), 0, 0, 0], [(-1021360426148), 0, 0], [575634970962, 0], [57999350684]]], rm := 503403061131638 }
noncomputable def w5 : Wit := { Z0 := { p := [[[3319037658444603610]], [[(-201730462389645383), 221269177229640240], [43655141963052601]], [[7530799757094128, (-13448697492643026), 0], [(-2890372616870402), 2910342797536840], [82903639011773]], [[(-425083718082008), 502053317139608, 0, 0], [152797674461238, (-192691507791361), 0], [(-9881366558888), 5526909267451], [3937512025122]], [[27891544957325, (-28338914538801), 0, 0, 0], [(-10898813759689), 10186511630749, 0, 0], [1174702313847, (-658757770593), 0], [(-291742303954), 262500801674], [(-23970138068)]]], r := 28551053738060, ok := true }, Z1 := { p := [[[7080613671348487701]], [[(-430358319764576816), 0], [93130969521178883]], [[16065706148467473, 0, 0], [(-6166128249323523), 0], [176861096558449]], [[(-906845265241617), 0, 0, 0], [325968372183975, 0, 0], [(-21080248658961), 0], [8400025653594]], [[59501962575627, 0, 0, 0, 0], [(-23250802687337), 0, 0, 0], [2506031602875, 0, 0], [(-622383581769), 0], [(-51136294544)]]], r := 50491688829542, ok := true }, Z2 := { p := [[[16350911362707883332]], [[(-544430252433756747), 221269177229640240], [(-619812044701185796)]], [[25282507409202970, (-13448697492643026), 0], [13626213025996696, 2910342797536840], [11991532356468944]], [[(-1482005121996790), 502053317139608, 0, 0], [(-572026486519771), (-192691507791361), 0], [(-282436026143245), 5526909267451], [(-314513101268241)]], [[100959377074425, (-28338914538801), 0, 0, 0], [28240211712198, 10186511630749, 0, 0], [9151179702587, (-658757770593), 0], [7483460033134, 262500801674], [7916084878327]]], r := 113689841471874, ok := true }, Z3 := { p := [[[35940079175673011987]], [[(-3871991757950955675), 808586920100045209], [(-1260846972206898647)]], [[460168889910812116, (-105585610308493549), 0], [128705846645476004, 5953024697304884], [28482576099682198]], [[(-57341255333723470), 12128160639633217, 0, 0], [(-15802537596512333), (-538404817256545), 0], [(-3137213890627195), (-34084535692062)], [(-720609228555152)]], [[7270096438481420, (-1505938335036266), 0, 0, 0], [1985302881299171, 53125825758734, 0, 0], [383777463038328, 5194248027687, 0], [79842719778641, 581202661534], [18607372071176]]], r := 3705056019904372, ok := true }, iE := { p := [[[30890367298994440822]], [[(-812325428252708418), 0], [(-428575283241363577)]], [[42078121842035774, 0, 0], [9064298255214291, 0], [12354702025033163]], [[(-2505295179649852), 0, 0, 0], [(-159652757805512), 0, 0], [(-310340739192020), 0], [(-297264341694150)]], [[173197824277571, 0, 0, 0, 0], [(-14724053668), 0, 0, 0], [12994140558289, 0, 0], [6936007791912, 0], [7811080716857]]], r := 192651186320548, ok := true }, iHu := { p := [[[56441541627667754311]], [[(-5423899504174346555), 0], [(-1109909937147646229)]], [[659547212601632853, 0, 0], [123338640951940758, 0], [27618373610977554]], [[(-82375538508277296), 0, 0, 0], [(-14919110603834878), 0, 0], [(-3052945413139972), 0], [(-705873021171314)]], [[10458606598893182, 0, 0, 0, 0], [1881615020430643, 0, 0, 0], [375951764520505, 0, 0], [78792155638552, 0], [18339109742681]]], r := 4728414874720128, ok := true }, T := { p := [[[8646911284551352320]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[11015808378944575084]], [[289683226242091957, 0], [152834155400037642]], [[(-7387658234495761), 0, 0], [4805756026401904, 0], [(-2285375501167842)]], [[304539690711037, 0, 0, 0], [(-212376078995697), 0, 0], [(-43459197632323), 0], [13173398688210]], [[(-20198139100379), 0, 0, 0, 0], [8159567627997, 0, 0, 0], [(-365369305247), 0, 0], [341679841789, 0], [(-217941643249)]]], r := 55059474411809, ok := true }, de := { p := [[[(-36649961225872081863)]], [[1869334247320132042, 0], [382527857559718141]], [[(-115588686315281108), 0, 0], [3215980624791995, 0], [(-4840247161783882)]], [[10221662116467401, 0, 0, 0], [27037328588345, 0, 0], [5532735193754, 0], [87589054350378]], [[(-1012245432798476), 0, 0, 0, 0], [227307693199, 0, 0, 0], [435141357794, 0, 0], [9518452471, 0], [(-1774966856541)]]], r := 616368589970539, ok := true }, dde := { p := [[[(-236503261066355547328)]], [[29247954233043485476, 0], [5985102603672991249]], [[(-3879653562537495618), 0, 0], [(-797326633195637593), 0], [(-162459516959613358)]], [[512266538099466536, 0, 0, 0], [104769226572549189, 0, 0], [21439262580483038, 0], [4389593506049157]], [[(-67659026167785281), 0, 0, 0, 0], [(-13846008677535454), 0, 0, 0], [(-2834229331506347), 0, 0], [(-579798130248448), 0], [(-118639734102492)]]], r := 15123298741534126, ok := true }, nJu := { p := [[[(-73299922451744163726)]], [[3738668494640264085, 0], [765055715119436282]], [[(-231177372630562216), 0, 0], [6431961249583991, 0], [(-9680494323567764)]], [[20443324232934802, 0, 0, 0], [54074657176690, 0, 0], [11065470387509, 0], [175178108700756]], [[(-2024490865596951), 0, 0, 0, 0], [454615386399, 0, 0, 0], [870282715589, 0, 0], [19036904942, 0], [(-3549933713082)]]], r := 1232737179941072, ok := true }, Jd1 := { p := [[[(-473006522132711094655)]], [[58495908466086970953, 0], [11970205207345982499]], [[(-7759307125074991236), 0, 0], [(-1594653266391275185), 0], [(-324919033919226715)]], [[1024533076198933073, 0, 0, 0], [209538453145098379, 0, 0], [42878525160966077, 0], [8779187012098315]], [[(-135318052335570562), 0, 0, 0, 0], [(-27692017355070908), 0, 0, 0], [(-5668458663012694), 0, 0], [(-1159596260496895), 0], [(-237279468204984)]]], r := 30246597483068242, ok := true }, term0 := { p := [[[5524687026053585027716]], [[(-1352440580940447189627), 0], [(-247845075313453933986)]], [[262283346908932231451, 0, 0], [63121884485499955347, 0], [9413628932099597427]], [[(-45674410648822806336), 0, 0, 0], [(-12343026004545886734), 0, 0], [(-2422237282773588302), 0], [(-327774684447607681)]], [[7489857575629795401, 0, 0, 0, 0], [2159862315105890190, 0, 0, 0], [475643226651868488, 0, 0], [84842622376810224, 0], [10841215287670230]]], r := 2232476004252837088, ok := true }, r0 := { p := [[[134526627742781929475]], [[(-18112804223479829130), 16795281406312076137], [(-1508759931984936411)]], [[2187016537169722191, (-2144408996256769689), 419022987931580559], [108463473757540013, (-214795830666545853)], [49770677982561059]], [[(-256953311830509156), 251860778510676942, (-39339961467643310), (-7982850087300693)], [(-5309777672124486), 18330277456709563, (-8567658512316662)], [(-5549299603858813), 6363090457175421], [(-1137569249118996)]], [[30629708698514445, (-29272789751092974), 3855303133444597, 1668981443592490, (-30029197743004)], [85836921037122, (-1398765955885386), 980013712608859, (-46146267177801)], [580156243915230, (-668384770296928), 183391125339136], [110049748152055, (-152199163876463)], [30361044397016]]], r := 57066996378294850, ok := true }, r1 := { p := [[[502899368153146500626]], [[(-58998645805311729527), 0], [(-7624011869469200985)]], [[6812004925375193603, 0, 0], [673175217985461452, 0], [207488658523289755]], [[(-797303436418276678), 0, 0, 0], [(-54574754071193110), 0, 0], [(-21112222239973440), 0], [(-5064928622950149)]], [[96132125074218311, 0, 0, 0, 0], [4872173637714591, 0, 0, 0], [2059159871396334, 0, 0], [482052897335634, 0], [132250706235872]]], r := 168721399819385256, ok := true }, r2 := { p := [[[667828553358882932281]], [[(-97403553140287222247), 18255460414444560618], [(-42254675224396014552)]], [[12280481485268859442, (-2113727918413246707), 27500339372884184], [5877874335056481080, (-202448086958008056)], [1584465710488632925]], [[(-1528768087002362616), 247726105177350110, 5167991283496974, (-818427640286513)], [(-734750916860220534), 16228565900199141, 818305643297479], [(-216123348540900630), 7239929163886152], [(-55228900915420557)]], [[192025457959884426, (-30071038635308122), (-385086328014322), (-15332032719262), 14380127806399], [91977430792894701, (-1803955112120073), 280971793082911, (-86075469387770)], [26993493178469069, (-1000956798359083), 103258143027856], [7550277100438082, (-251021508295263)], [1823451524508440]]], r := 886582922772430393, ok := true }, r3 := { p := [[[5711383799368260878097]], [[(-1448940530388895775421), 159826280335791370076], [(-354914721016975385284)]], [[281482131894671360074, (-37229153300638813501), (-99964978250180462)], [91569050597165556784, (-3989939930771088671)], [14958096054987278817]], [[(-49111399108771395350), 7234486696099195088, 13238020608457609, 2013686708160903], [(-18055074044864766427), 1045754382076084229, (-14610452998862287)], [(-3915605194825407485), 120870436622025278], [(-552125723658305192)]], [[8065245460973775937, (-1263953204367925780), 342579243800407, (-486482690551772), (-35186633103802)], [3172658643525912990, (-201390286528032569), 454370666875675, 415574875428780], [772966776696368151, (-27795682812913897), (-554325029004528)], [144488103550335054, (-2965958451172660)], [18859293277727839]]], r := 973960031014968549841, ok := true }, eta := { p := [[[(-1603436830059445159437)]], [[227899813193278421372, 0], [58764723867526258765]], [[(-29959624731533024916), 0, 0], [(-8253969115180865894), 0], [(-2077647600369925416)]], [[3857270480728892594, 0, 0, 0], [1045333796793485523, 0, 0], [287803748370722577, 0], [68069366110404220]], [[(-497167658986298666), 0, 0, 0, 0], [(-132366458357642712), 0, 0, 0], [(-36282130152795501), 0, 0], [(-9291447735235957), 0], [(-2157623938499325)]]], r := 666404028746003647, 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 5188146770730811392 5476377146882523136 6917529027641081856 9223372036854775808 2305843009213693952 4323455642275676160 :=
  (RegionPosI.split_t 8070450532247928832 (RegionPosI.split_s 3314649325744685056 (RegionPosI.split_s 2810246167479189504 (RegionPosI.of_check c0 q0 ok_0 5188146770730811392 5476377146882523136 6917529027641081856 8070450532247928832 2305843009213693952 2810246167479189504 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 5188146770730811392 5476377146882523136 6917529027641081856 8070450532247928832 2810246167479189504 3314649325744685056 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 5188146770730811392 5476377146882523136 6917529027641081856 8070450532247928832 3314649325744685056 4323455642275676160 (by decide +kernel))) (RegionPosI.split_s 3314649325744685056 (RegionPosI.split_s 2810246167479189504 (RegionPosI.of_check c3 q3 ok_3 5188146770730811392 5476377146882523136 8070450532247928832 9223372036854775808 2305843009213693952 2810246167479189504 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 5188146770730811392 5476377146882523136 8070450532247928832 9223372036854775808 2810246167479189504 3314649325744685056 (by decide +kernel))) (RegionPosI.of_check c5 q5 ok_5 5188146770730811392 5476377146882523136 8070450532247928832 9223372036854775808 3314649325744685056 4323455642275676160 (by decide +kernel))))

end CKLaneC.RSC2.BB_0023

end
Source
arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneC.RSC2.BB_0023 (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneC/RSC2/BB_0023.lean)
View graph