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

import Definitions.Def_CK_CKLaneC_RSC2_S03_0129_part00

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

namespace CKLaneC.RSC2.S03_0129
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def w7 : Wit := { Z0 := { p := [[[1007294753884398723]], [[(-37811686240554880), 143899250554914103], [2028067438563133]], [[420131437998190, (-5401669462936412), 0], [(-75159450239533), 289723919794733], [(-14350499848944)]], [[(-5548198765301), 60018776856884, 0, 0], [845059394949, (-10737064319934), 0], [533777696601, (-2050071406992)], [157432451759]], [[83490092296, (-792599823615), 0, 0, 0], [(-13018022135), 120722770707, 0, 0], [(-5979690096), 76253956657, 0], [(-5862029543), 22490350251], [(-2017445947)]]], r := 210392591753, ok := true }, Z1 := { p := [[[1151194004439312826]], [[(-43213355703491291), 0], [2317791358357866]], [[480150214855075, 0, 0], [(-85896514559466), 0], [(-16400571255936)]], [[(-6340798588915), 0, 0, 0], [965782165656, 0, 0], [610031653258, 0], [179922802011]], [[95417248339, 0, 0, 0, 0], [(-14877739582), 0, 0, 0], [(-6833931539), 0, 0], [(-6699462334), 0], [(-2305652511)]]], r := 57334186502, ok := true }, Z2 := { p := [[[4742437677751625100251]], [[(-49874179387530161674), 143899250554914103], [(-76731903688628174170)]], [[631089149841680641, (-5401669462936412), 0], [811027333497515712, 289723919794733], [1327453116065324031]], [[(-9076328805687579), 60018776856884, 0, 0], [(-10086218627565385), (-10737064319934), 0], [(-14058432706944145), (-2050071406992)], [(-23393533864837874)]], [[147922911196199, (-792599823615), 0, 0, 0], [141319775247890, 120722770707, 0, 0], [173791568565146, 76253956657, 0], [248036458353356, 22490350251], [415830201020404]]], r := 150251019678014, ok := true }, Z3 := { p := [[[7490155044729021327611]], [[(-248716673757809056675), 454449331118645499], [(-122111568472355459266)]], [[8789039534227508286, (-27367556545558226), 0], [4107591896534263226, 857281672029785], [2118318789210679961]], [[(-316026610928791306), 940789791629104, 0, 0], [(-145836336485614048), (-48329576773836), 0], [(-71591987732393505), (-6175587727834)], [(-37391579182770292)]], [[11456120405450162, (-33575783091025), 0, 0, 0], [5258442303764696, 1527838032461, 0, 0], [2546327487002553, 354396331744, 0], [1267232410380144, 68107749804], [665408612443243]]], r := 4479474814664621, ok := true }, iE := { p := [[[4745412891986071297252]], [[(-49878227175390047050), 0], [(-76725913450827012791)]], [[631198741468574596, 0, 0], [811022048390352891, 0], [1327410729453801089]], [[(-9078399502989546), 0, 0, 0], [(-10085896779938667), 0, 0], [(-14058389540309793), 0], [(-23393068861650244)]], [[147963597096339, 0, 0, 0, 0], [141312862360705, 0, 0, 0], [173789499636163, 0, 0], [248035966449403, 0], [415824242154963]]], r := 150157014676676, ok := true }, iHu := { p := [[[7493262495560724498191]], [[(-248733846613389936185), 0], [(-122105706519300769110)]], [[8789830725197302242, 0, 0], [4107582046313590745, 0], [2118276561543243694]], [[(-316056825891246212), 0, 0, 0], [(-145835299032529630), 0, 0], [(-71591874070490794), 0], [(-37391113473021626)]], [[11457245314689746, 0, 0, 0, 0], [5258400297037587, 0, 0, 0], [2546319318348906, 0, 0], [1267231013624522, 0], [665402625926502]]], r := 4477061052805578, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[71707641603873583]], [[753706815305705, 0], [1159400547158516]], [[(-1615921217211), 0, 0], [12117219446843, 0], [(-1312725984962)]], [[19946112430, 0, 0, 0], [(-29385587774), 0, 0], [(-14425652180), 0], [7953148117]], [[(-369372463), 0, 0, 0, 0], [362656567, 0, 0, 0], [(-94598), 0, 0], [87397236, 0], [(-72301354)]]], r := 294894491, ok := true }, de := { p := [[[(-114955473100508133811)]], [[492921078184408039, 0], [241979438381436675]], [[(-9126551907198476), 0, 0], [1586821739825, 0], [(-2199423583586013)]], [[225346967737272, 0, 0, 0], [10405856, 0, 0], [5108330, 0], [26659680636952]], [[(-6259637992667), 0, 0, 0, 0], [69, 0, 0, 0], [94649, 0, 0], [17, 0], [(-363541099592)]]], r := 989950203438, ok := true }, dde := { p := [[[(-75180394542297286336036)]], [[2783966048768741618292, 0], [1366674242122836795417]], [[(-103109856891088510333), 0, 0], [(-50617567697273422188), 0], [(-24848623363174716746)]], [[3818883588537643019, 0, 0, 0], [1874724670715844451, 0, 0], [920319383805962302, 0], [451793152055217742]], [[(-141440132908797262), 0, 0, 0, 0], [(-69434247064317681), 0, 0, 0], [(-34085903104488609), 0, 0], [(-16733079705747282), 0], [(-8214420946457984)]]], r := 10544523875298086, ok := true }, nJu := { p := [[[(-229910946201016267621)]], [[985842156368816078, 0], [483958876762873350]], [[(-18253103814396951), 0, 0], [3173643479651, 0], [(-4398847167172025)]], [[450693935474544, 0, 0, 0], [20811713, 0, 0], [10216660, 0], [53319361273904]], [[(-12519275985333), 0, 0, 0, 0], [138, 0, 0, 0], [189299, 0, 0], [34, 0], [(-727082199184)]]], r := 1979900406869, ok := true }, Jd1 := { p := [[[(-150360789084594572672071)]], [[5567932097537483236584, 0], [2733348484245673590834]], [[(-206219713782177020665), 0, 0], [(-101235135394546844375), 0], [(-49697246726349433492)]], [[7637767177075286039, 0, 0, 0], [3749449341431688902, 0, 0], [1840638767611924604, 0], [903586304110435484]], [[(-282880265817594524), 0, 0, 0, 0], [(-138868494128635362), 0, 0, 0], [(-68171806208977218), 0, 0], [(-33466159411494564), 0], [(-16428841892915967)]]], r := 21089047750596167, ok := true }, term0 := { p := [[[425014661643149371261647013]], [[(-31474210700956995368465731), 0], [(-15447736638158503201740230)]], [[1748412596412886520417509, 0, 0], [1144124935339214919963918, 0], [421235185163497059731957]], [[(-86337543902232877125140), 0, 0, 0], [(-63559684320110616421621), 0, 0], [(-31199845350255676606755), 0], [(-10210953299050542530531)]], [[3997002433892533844100, 0, 0, 0, 0], [3138680408721335901699, 0, 0, 0], [1733273612826178428974, 0, 0], [756316711801646579449, 0], [232056091812246326097]]], r := 495720863409972069666, ok := true }, r0 := { p := [[[40811163901874248299855]], [[(-1414340282091660952771), 11580696004740793726735], [(-661735781029838917619)]], [[38314535068751292012, (-395457225056161639118), 804612006043253424945], [22832734983629902567, (-188092803735351934272)], [11458660675470258712]], [[(-991999930525379601), 10500383711600812819, (-25809951211276652358), (-3176813413599293387)], [(-606305977231792005), 6417652859081016169, (-13158178202651760393)], [(-394704017295576710), 3258615413968676749], [(-202040865076036322)]], [[26588440355966716, (-267312589541286262), 625155024094611620, 339214960133071053, (-104815834969466352)], [15286083761017036, (-167756266319732233), 428383854988921019, 39169210533041734], [10404644686192280, (-111109423279980210), 228410860421566378], [6952300350284461, (-57472292069312356)], [3592659088290042]]], r := 197658292113114959, ok := true }, r1 := { p := [[[53193191017939631101580]], [[(-1835257827171677667538), 0], [(-862946273005023959437)]], [[49422540232248755098, 0, 0], [29674421286976428153, 0], [14945050886525961985]], [[(-1273350017856890795), 0, 0, 0], [(-784283460216361731), 0, 0], [(-513209975228671165), 0], [(-263535603046605946)]], [[34049652380854903, 0, 0, 0, 0], [19693096666558597, 0, 0, 0], [13470083375666790, 0, 0], [9042016635033099, 0], [4686417409995160]]], r := 13718710210753590, ok := true }, r2 := { p := [[[106991279392783717644751701]], [[(-3714202718997854190460169), 15008826629582041042716], [(-3820145238299940130998932)]], [[114242673568202926496971, (-371178157694710134948), 455666873541252128], [130600382682852710005642, (-269807176793588460337)], [103059266315785450195260]], [[(-3611349214951555517159), 9442554596798585630, 254318109858505, (-14107652982950)], [(-3963886900869756466181), 6461694864120900946, 66820140157627], [(-3490181002039950402582), 4884045816960775434], [(-2479456632813744976414)]], [[119617312572227095042, (-262480788220006881), (-4251105176647), (-139481775664), (-84267107609)], [124155381786629392084, (-159144904896692442), 703533316417, (-720255262743)], [105052612254521387566, (-115471058826833343), (-854697697247)], [83403037644850727547, (-88562766371376854)], [56025295115258404009]]], r := 415710188760069771689, ok := true }, r3 := { p := [[[849397426242036985775749420]], [[(-62908544791581046466907417), 125160205434404834523551], [(-30883979607186866251286572)]], [[3494738114622858473495550, (-7912559974057863304216), 1773077379528631375], [2287524566335858812413170, (-2281272258001192607265)], [842261356951862093990589]], [[(-172575189047479417732849), 414407375352457942867, 4738931750457215, (-112090049534523)], [(-127081409170423927532614), 144139663348780234953, 90436447565352], [(-62386501562484802346528), 41515236337310315216], [(-20418105964428311713241)]], [[7989467858294080547296, (-19843668631565144188), (-198298983488274), (-8767481529640), (-1919464496838)], [6275543914976776812880, (-7547292681280112385), 14939267663380, (-15233454174414)], [3465856966102238883376, (-2622519199598642912), (-10040176496111)], [1512393599159012884683, (-755226700667384837)], [464043067466783801868]]], r := 43247144534104295145737, ok := true }, eta := { p := [[[(-107126041732454554640514285)]], [[3720314235961673524021620, 0], [3822559107055983911934463]], [[(-114480212328535534037023), 0, 0], [(-130709695078428271590408), 0], [(-103102909409123378469883)]], [[3620249077312205719078, 0, 0, 0], [3968128611775371543247, 0, 0], [3492156047427443667252, 0], [2480247480197632483431]], [[(-119947558355104729791), 0, 0, 0, 0], [(-124314169419942747357), 0, 0, 0], [(-105129207433179954750), 0, 0], [(-83438812751862062267), 0], [(-56039640563438134550)]]], r := 42876981575724729389, 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 6755399441055744 7881299347898368 13835058055282163712 18446744073709551616 6917529027641081856 8070450532247928832 :=
  (RegionPosI.split_b 7318349394477056 (RegionPosI.split_s 7493989779944505344 (RegionPosI.split_b 7036874417766400 (RegionPosI.of_check c0 q0 ok_0 6755399441055744 7036874417766400 13835058055282163712 18446744073709551616 6917529027641081856 7493989779944505344 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 7036874417766400 7318349394477056 13835058055282163712 18446744073709551616 6917529027641081856 7493989779944505344 (by decide +kernel))) (RegionPosI.split_b 7036874417766400 (RegionPosI.of_check c2 q2 ok_2 6755399441055744 7036874417766400 13835058055282163712 18446744073709551616 7493989779944505344 8070450532247928832 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 7036874417766400 7318349394477056 13835058055282163712 18446744073709551616 7493989779944505344 8070450532247928832 (by decide +kernel)))) (RegionPosI.split_s 7493989779944505344 (RegionPosI.split_s 7205759403792793600 (RegionPosI.of_check c4 q4 ok_4 7318349394477056 7881299347898368 13835058055282163712 18446744073709551616 6917529027641081856 7205759403792793600 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 7318349394477056 7881299347898368 13835058055282163712 18446744073709551616 7205759403792793600 7493989779944505344 (by decide +kernel))) (RegionPosI.split_b 7599824371187712 (RegionPosI.of_check c6 q6 ok_6 7318349394477056 7599824371187712 13835058055282163712 18446744073709551616 7493989779944505344 8070450532247928832 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 7599824371187712 7881299347898368 13835058055282163712 18446744073709551616 7493989779944505344 8070450532247928832 (by decide +kernel)))))

end CKLaneC.RSC2.S03_0129