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

import Definitions.Def_CK_CKLaneC_RSC2_S10_0043_part00

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

namespace CKLaneC.RSC2.S10_0043
open CKLaneC.TM3 CKLaneC.RSCell

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

noncomputable def c6 : Cell := { bc := 684547143360315392, bh := 36028797018963968, tc := 6917529027641081856, th := 2305843009213693952, sc := 12682136550675316736, sh := 1152921504606846976 }
noncomputable def q6 : Cert := { V0 := [[[400723794740555813]], [[(-92285536343166448), 133483676092747510], [4836265645893333]], [[2944909510802336, (-30699035783939978), (-45424587362302)], [(-1078728894847331), 1608796979537874], [(-66800880170465)]], [[(-127884024740849), 965171723214093, 31362822237167, (-5026921834405)], [28337361483280, (-357326498750785), (-1643583011535)], [15377219448402, (-22261208537165)], [2076845993300]], [[6173029304009, (-40509365275136), (-8211706429534), 3461447552246, 5053429390], [(-1548731449005), 8865770375751, 1122381335031, (-181398738583)], [(-484510492607), 5121190399575, 2898473989], [(-475513468499), 691806002366], [(-74478552117)]]], r0 := 118930076249032, V1 := [[[1066382385028696484]], [[(-244568771906844984), 0], [12816738098948927]], [[7455212767136635, 0, 0], [(-2822174766278713), 0], [(-177990065448494)]], [[(-290504424267455), 0, 0, 0], [61660187553346, 0, 0], [40889131660235, 0], [5526646647427]], [[12652443623658, 0, 0, 0, 0], [(-2425183740092), 0, 0, 0], [(-1254687308949), 0, 0], [(-1259960498451), 0], [(-198227860936)]]], r1 := 65578840141639, V2 := [[[17286389395203485808]], [[(-43439804101854428), 2156797577761411], [(-61595474404641721)]], [[382872139710975, (-350106470488325), (-3647708594030)], [(-2220231827474505), 234395846845035], [(-29944598116903)]], [[(-10982151317050), (-16992001838940), 1324160483276, 5909994594], [28573914189884, (-38349919338275), (-594453525742)], [4208461649321, 6655399823257], [(-79798736245)]], [[533073608944, 168486114578, (-90549422943), (-3335310158), (-9317309)], [(-738157612369), (-1806362813016), 216684878905, 1278489241], [388587259048, (-1116712162876), (-32931295446)], [23578439031, 13005467063], [988352197]]], r2 := 70807021750931, V3 := [[[17488005419162693231]], [[(-83675292955367665), 3556586238113682], [(-51438610648361222)]], [[322041461587278, (-396956099252916), (-12057258190261)], [(-4295797851282351), 389494270119478], [(-53870369412007)]], [[(-135908317857), (-64207674590205), 3766029247925, 39276015701], [34787635123429, (-44574513103680), (-1980283128638)], [6108908368210, 11314126585231], [(-106794640165)]], [[(-25108875335), 248375290239, (-52907458840), (-20200471215), (-124816599)], [(-63847177900), (-6919402439726), 624417617065, 8570148933], [967190166938, (-1392013538212), (-111481638307)], [21689242861, 32144129961], [587625166]]], r3 := 501479307163970, Vm := [[[17297557557079907142]], [[(-45340775032573994), 0], [(-60378757475596768)]], [[311997710379532, 0, 0], [(-2429430508355926), 0], [4774157840801]], [[(-10017696095136), 0, 0, 0], [21154729707789, 0, 0], [(-1930126278012), 0], [(-8019012182)]], [[509820456146, 0, 0, 0, 0], [(-607865521938), 0, 0, 0], [201631139686, 0, 0], [4577821122, 0], [548019510]]], rm := 22795156028100 }
noncomputable def w6 : Wit := { Z0 := { p := [[[400860260132660251]], [[(-92379845455908709), 133620086710886750], [4841207957983867]], [[2969653288768904, (-30793281818636237), 0], [(-1082109268633094), 1613735985994622], [(-66809456231189)]], [[(-131074944072484), 989884429589634, 0, 0], [29210159254739, (-360703089544365), 0], [15383986304857, (-22269818743730)], [2077560254060]], [[6422683725766, (-43691648024162), 0, 0, 0], [(-1658660406861), 9736719751579, 0, 0], [(-486614289184), 5127995434952, 0], [(-476011075297), 692520084686], [(-74501982721)]]], r := 26054129261290, ok := true }, Z1 := { p := [[[1068960693687094004]], [[(-246346254549089889), 0], [12909887887956979]], [[7919075436717079, 0, 0], [(-2885624716354916), 0], [(-178158549949837)]], [[(-349533184193289), 0, 0, 0], [77893758012639, 0, 0], [41023963479618, 0], [5540160677494]], [[17127156602043, 0, 0, 0, 0], [(-4423094418296), 0, 0, 0], [(-1297638104490), 0, 0], [(-1269362867458), 0], [(-198671953921)]]], r := 15857792198692, ok := true }, Z2 := { p := [[[85737680269847617439]], [[(-2691226311937103713), 133620086710886750], [(-3816024607876711551)]], [[115392655908975521, (-30793281818636237), 0], [122424250078702846, 1613735985994622], [182460119216814011]], [[(-5550260408682774), 989884429589634, 0, 0], [(-4991893053270871), (-360703089544365), 0], [(-5952197464544921), (-22269818743730)], [(-9102311820679799)]], [[289873545223646, (-43691648024162), 0, 0, 0], [227375894657420, 9736719751579, 0, 0], [240502229952542, 5127995434952, 0], [298911598097388, 692520084686], [461377431327375]]], r := 542127660156132, ok := true }, Z3 := { p := [[[100594002433257026165]], [[(-7342436881513553465), 312087463869874187], [(-4513695006240372391)]], [[613883502617453701, (-84616066246533041), 0], [343061965875334686, 3573850298512313], [216584079634022485]], [[(-53056306486603808), 6302933206667425, 0, 0], [(-29100137106184690), (-894051095370313), 0], [(-16771961046457357), (-51897141903852)], [(-10821568008923111)]], [[4653311280327994, (-533779709127036), 0, 0, 0], [2534471209566167, 50180802686379, 0, 0], [1429163665280373, 13954693288505, 0], [844848376212293, 1600439576998], [549110909629856]]], r := 4975209930146909, ok := true }, iE := { p := [[[92178168449312358819]], [[(-2807192807675889963), 0], [(-3738242533351770752)]], [[121435817176256936, 0, 0], [121563017659249412, 0], [181386713953366247]], [[(-5853634932237275), 0, 0, 0], [(-4911251498862022), 0, 0], [(-5933071028516007), 0], [(-9068932352597897)]], [[306174770225559, 0, 0, 0, 0], [222697093519910, 0, 0, 0], [239586044839746, 0, 0], [298355092488149, 0], [460180432805007]]], r := 549710900270417, ok := true }, iHu := { p := [[[107647179116716182796]], [[(-7656872163671444352), 0], [(-4432925989493994116)]], [[642673096908639514, 0, 0], [341154524648348672, 0], [215411204226995443]], [[(-55580049130637181), 0, 0, 0], [(-28883969868091901), 0, 0], [(-16722298344684841), 0], [(-10785398074482937)]], [[4876119043576023, 0, 0, 0, 0], [2516267922391393, 0, 0, 0], [1425075567653274, 0, 0], [843402821632556, 0], [547810858702674]]], r := 5036620625052705, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[3691572230663875168]], [[112423095286755815, 0], [149709986212151939]], [[(-1439557633032934), 0, 0], [4250148808422699, 0], [(-1192797817156728)]], [[42480881870939, 0, 0, 0], [(-77749798122364), 0, 0], [(-45013041018210), 0], [20224407657159]], [[(-1932308280135), 0, 0, 0, 0], [2232688488780, 0, 0, 0], [(-107133631385), 0, 0], [748352651364, 0], [(-532861010553)]]], r := 4544586816844, ok := true }, de := { p := [[[(-48472105083637033131)]], [[1241353276821662964, 0], [718678212896752242]], [[(-54947902782114310), 0, 0], [1710495558692008, 0], [(-18417441098714214)]], [[3332519880184502, 0, 0, 0], [4071077992628, 0, 0], [2356939890469, 0], [646680851512695]], [[(-227213080498853), 0, 0, 0, 0], [9689400208, 0, 0, 0], [115548110514, 0, 0], [3247693699, 0], [(-25526405656676)]]], r := 96558710325601, ok := true }, dde := { p := [[[(-535219265459108578774)]], [[47382444167482150653, 0], [27431941360121245084]], [[(-4310526767127068831), 0, 0], [(-2497323405753335008), 0], [(-1444802600615998108)]], [[391858853778233277, 0, 0, 0], [226857296864608378, 0, 0], [131338435026878542, 0], [76040841868906349]], [[(-35623549336059550), 0, 0, 0, 0], [(-20624189971153735), 0, 0, 0], [(-11940551899564872), 0, 0], [(-6912817137145688), 0], [(-4002151501517351)]]], r := 8846827495504727, ok := true }, nJu := { p := [[[(-96944210167274066261)]], [[2482706553643325928, 0], [1437356425793504485]], [[(-109895805564228620), 0, 0], [3420991117384016, 0], [(-36834882197428428)]], [[6665039760369004, 0, 0, 0], [8142155985257, 0, 0], [4713879780939, 0], [1293361703025390]], [[(-454426160997706), 0, 0, 0, 0], [19378800417, 0, 0, 0], [231096221028, 0, 0], [6495387398, 0], [(-51052811313352)]]], r := 193117420651196, ok := true }, Jd1 := { p := [[[(-1070438530918217157547)]], [[94764888334964301307, 0], [54863882720242490168]], [[(-8621053534254137662), 0, 0], [(-4994646811506670016), 0], [(-2889605201231996215)]], [[783717707556466554, 0, 0, 0], [453714593729216757, 0, 0], [262676870053757085, 0], [152081683737812698]], [[(-71247098672119099), 0, 0, 0, 0], [(-41248379942307470), 0, 0, 0], [(-23881103799129744), 0, 0], [(-13825634274291376), 0], [(-8004303003034701)]]], r := 17693654991009447, ok := true }, term0 := { p := [[[22835128916645022166596]], [[(-3996919379667645172109), 0], [(-2274104951034967496666)]], [[538600634949880181155, 0, 0], [406018828035876459172, 0], [176325128550988289994]], [[(-64892979590979352912), 0, 0, 0], [(-55024096401115947241), 0, 0], [(-31665018087496931199), 0], [(-12260772650947594608)]], [[7347484801619916611, 0, 0, 0, 0], [6648972912675289470, 0, 0, 0], [4300053910488243176, 0, 0], [2208493095744773644, 0], [802172854366325461]]], r := 3182835759268249798, ok := true }, r0 := { p := [[[99939093038575332613]], [[(-10085621877658070608), 66553178995946050982], [(-4117913534291884632)]], [[900189484656654827, (-6682964478157804747), 11043666674674982162], [427988699891356597, (-2744026929951504693)], [200116848528329392]], [[(-74127676219463085), 591244453964826360, (-1086698456413675723), (-16137413881460351)], [(-35842557536284189), 284603062969337976, (-456504904713652588)], [(-20879408553912477), 133351331387025037], [(-10019956008813397)]], [[5941995089859306, (-48300184727218713), 92645774452941633, 9003052555463378, (-1328484752427777)], [2780041840256243, (-23731305518286824), 46951631073252417, 277911230217449], [1741468033239670, (-13885371647446263), 22185300907910177], [1048459687421477, (-6677205563649570)], [508943389258067]]], r := 60847876191094171, ok := true }, r1 := { p := [[[705962017816849303113]], [[(-69096979093863535051), 0], [(-29201302628694245393)]], [[5837833826876778212, 0, 0], [2996142991296490222, 0], [1419156199394414040]], [[(-458109155495183677), 0, 0, 0], [(-244122891088238607), 0, 0], [(-146252181217497661), 0], [(-71073077749012400)]], [[35418190566669877, 0, 0, 0, 0], [18386865212542635, 0, 0, 0], [11888461604109383, 0, 0], [7352918772387892, 0], [3610518054102822]]], r := 47702842325646891, ok := true }, r2 := { p := [[[9910341196739298308438]], [[(-1120246759593530260295), 123397060890591670351], [(-1016838520190758800244)]], [[103436433921520439192, (-10251923766679985245), 526640294854858788], [112646303561819008331, (-6266754476409964303)], [78805857983870323594]], [[(-9063034338822230276), 810982719257358153, 4718865931569806, (-868268233948902)], [(-10207895969516432107), 489496643653926786, 2746333552617770], [(-8617726007885829438), 331917070011956262], [(-5459673216972356638)]], [[784426715303258088, (-64441776003294272), (-93790617277159), 164379449811586, 1422016353077], [881037389729760013, (-36707120049759822), 228770313698553, (-55383832205545)], [771568404856745866, (-25285080632377816), 904470671408], [591346252245898786, (-17476232703692389)], [355718887427659908]]], r := 10707192818349737459, ok := true }, r3 := { p := [[[39921094039665347374935]], [[(-7178013237448770305114), 616958284331460052343], [(-4251689822001709612980)]], [[974916965929894703310, (-89284201158658179321), 2019338612724948534], [768648980192977102902, (-32389382323346220329)], [336953428415229145781]], [[(-117943379638101038335), 11213540311483021999, 38325890465727621, (-6606664206861975)], [(-104633999805803215414), 4763925445999633755, 7080518322326834], [(-61045520972896405320), 1721039129187180596], [(-23693937616320755888)]], [[13387199263891197704, (-1300446062626421666), (-1097209894814210), 1179630999644453, 21402523936758], [12671805206142630974, (-596254775487105965), 1611458955317097, (-405795716119167)], [8314813890354226085, (-251590937129651413), (-24465087290516)], [4296645044777951455, (-90869517523154276)], [1560738141728888436]]], r := 467911953872235231284, ok := true }, eta := { p := [[[(-11379649026136003528501)]], [[1271181044362139012825, 0], [1088126271899759749874]], [[(-117796312443092123128), 0, 0], [(-120120671053149135307), 0], [(-82535584285303322053)]], [[10377556166856500006, 0, 0, 0], [10903931112341717835, 0, 0], [9003920970740982129, 0], [5654858391529852072]], [[(-903276314271475110), 0, 0, 0, 0], [(-943954135521677643), 0, 0, 0], [(-807385643871094767), 0, 0], [(-611460254519360279), 0], [(-365951177079935716)]]], r := 1861262338565297973, ok := true } }
theorem sB_6 : stageB c6 w6 = true := by decide +kernel
theorem s0_6 : stageC0 w6 q6 = true := by decide +kernel
theorem s1_6 : stageC1 w6 q6 = true := by decide +kernel
theorem s2_6 : stageC2 w6 q6 = true := by decide +kernel
theorem s3_6 : stageC3 w6 q6 = true := by decide +kernel
theorem sE_6 : stageE w6 q6 = true := by decide +kernel
theorem sF_6 : stageF w6 = true := by decide +kernel
theorem ok_6 : (domOK c6 && cellCheck c6 q6) = true :=
  staged_check c6 q6 w6 (by decide +kernel) sB_6 s0_6 s1_6 s2_6 s3_6 sE_6 sF_6

theorem region : RegionPosI 576460752303423488 720575940379279360 4611686018427387904 9223372036854775808 9223372036854775808 13835058055282163712 :=
  (RegionPosI.split_s 11529215046068469760 (RegionPosI.split_b 648518346341351424 (RegionPosI.split_s 10376293541461622784 (RegionPosI.of_check c0 q0 ok_0 576460752303423488 648518346341351424 4611686018427387904 9223372036854775808 9223372036854775808 10376293541461622784 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 576460752303423488 648518346341351424 4611686018427387904 9223372036854775808 10376293541461622784 11529215046068469760 (by decide +kernel))) (RegionPosI.split_s 10376293541461622784 (RegionPosI.of_check c2 q2 ok_2 648518346341351424 720575940379279360 4611686018427387904 9223372036854775808 9223372036854775808 10376293541461622784 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 648518346341351424 720575940379279360 4611686018427387904 9223372036854775808 10376293541461622784 11529215046068469760 (by decide +kernel)))) (RegionPosI.split_b 648518346341351424 (RegionPosI.split_s 12682136550675316736 (RegionPosI.of_check c4 q4 ok_4 576460752303423488 648518346341351424 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 576460752303423488 648518346341351424 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel))) (RegionPosI.of_check c6 q6 ok_6 648518346341351424 720575940379279360 4611686018427387904 9223372036854775808 11529215046068469760 13835058055282163712 (by decide +kernel))))

end CKLaneC.RSC2.S10_0043