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

import Definitions.Def_CK_CKLaneC_RSC2_S02_0060_part00

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

namespace CKLaneC.RSC2.S02_0060
open CKLaneC.TM3 CKLaneC.RSCell

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

noncomputable def c7 : Cell := { bc := 4362862139015168, bh := 140737488355328, tc := 6917529027641081856, th := 2305843009213693952, sc := 4467570830351532032, sh := 144115188075855872 }
noncomputable def q7 : Cert := { V0 := [[[607296145014606933]], [[(-10120605312887971), 202115651018629042], [2032181442088990]], [[70582329257888, (-3357721230523434), (-157907125801889)], [(-33948954108988), 674218444591314], [(-25978891056104)]], [[(-620603738438), 23153801285578, 7882655001988, (-17383594061907)], [258566242565, (-11157510302175), (-1582809003435)], [433886951839, (-8629655457739)], [508346353716]], [[6898703029, (-200766037044), (-185842834924), 862398069119, 40223563517], [(-2792902529), 82401542356, 78997638607, (-173166455720)], [(-3235897174), 143130220596, 14957724204], [(-8489011187), 168914142555], [(-11593897201)]]], r0 := 3198720834462, V1 := [[[1611786902708052762]], [[(-26607084574376880), 0], [5342607663129162]], [[179300937475901, 0, 0], [(-86737833862322), 0], [(-68550940686594)]], [[(-1511501979199), 0, 0, 0], [600512276087, 0, 0], [1120945187294, 0], [1342631386560]], [[16403871352, 0, 0, 0, 0], [(-5990630013), 0, 0, 0], [(-7782785884), 0, 0], [(-21993119226), 0], [(-30637687255)]]], r1 := 1086726375609, V2 := [[[18441446429103512948]], [[(-37621911222646), 132113738224], [(-170467311113914)]], [[47077548251, (-413210626), (-3146259)], [(-1226073310158), 8562062441], [8108304225]], [[(-594611962), (-10923035), 42117, 73], [1679934203, (-26321448), (-306149)], [(-243996618), 139490830], [(-71684902)]], [[10013686, 26568, 161, (-2), 0], [(-21159552), (-716524), 4086, 9], [3165326, (-412344), (-9964)], [2019868, 18798], [1035330]]], r2 := 4119312990, V3 := [[[18444630290317007685]], [[(-68181337863932), 104433508631], [(-68203565148776)]], [[172181064, 2323688265, (-4944540)], [(-2199777346925), 6771249993], [(-551756364)]], [[57641, (-34450039), (-59983), 230], [11152650, 150847528, (-481082)], [(-12329011), 110429506], [(-78427)]], [[(-649), (-11449), 2766, 0, 0], [4094, (-2231875), (-5851), 30], [181456, 2466758, (-15654)], [(-2233), 16542], [459]]], r3 := 19029163298, Vm := [[[18441447128759083251]], [[(-37624826199471), 0], [(-170421827542554)]], [[47029501734, 0, 0], [(-1226262741311), 0], [8854323981]], [[(-594547092), 0, 0, 0], [1676793191, 0, 0], [(-247100029), 0], [(-71518376)]], [[10013176, 0, 0, 0, 0], [(-21155011), 0, 0, 0], [3113147, 0, 0], [2019253, 0], [1034356]]], rm := 470790709 }
noncomputable def w7 : Wit := { Z0 := { p := [[[607771398031403976]], [[(-10144380884471990), 202590466010467992], [2036955492044934]], [[71144999822595, (-3381460294823997), 0], [(-34188082692825), 678985164014978], [(-26023920343991)]], [[(-629815834226), 23714999940865, 0, 0], [264284159476, (-11396027564275), 0], [436140675175, (-8674640114664)], [509149431579]], [[7029481258, (-209938611409), 0, 0, 0], [(-2889195425), 88094719825, 0, 0], [(-3289403259), 145380225058, 0], [(-8529198531), 169716477193], [(-11611202301)]]], r := 746831574549, ok := true }, Z1 := { p := [[[1620723728083743936]], [[(-27051682358591972), 0], [5431881312119826]], [[189719999526920, 0, 0], [(-91168220514200), 0], [(-69397120917310)]], [[(-1679508891268), 0, 0, 0], [704757758604, 0, 0], [1163041800467, 0], [1357731817545]], [[18745283355, 0, 0, 0, 0], [(-7704521132), 0, 0, 0], [(-8771742023), 0, 0], [(-22744529415), 0], [(-30963206135)]]], r := 275961946743, ok := true }, Z2 := { p := [[[9038974914357847005242]], [[(-57691506040523610578), 202590466010467992], [(-261403942256941208941)]], [[463438481952928511, (-3381460294823997), 0], [1665404349376178246, 678985164014978], [8044952250151458927]], [[(-4589844120658220), 23714999940865, 0, 0], [(-13045857038267228), (-11396027564275), 0], [(-51224199104258559), (-8674640114664)], [(-251937283304401775)]], [[57233255559462, (-209938611409), 0, 0, 0], [124813221774346, 88094719825, 0, 0], [397626373746293, 145380225058, 0], [1603579500679909, 169716477193], [7954224376593252]]], r := 957479965952110, ok := true }, Z3 := { p := [[[20724237164211292836446]], [[(-606463713251813096458), 928921834284421838], [(-606661421922894582982)]], [[18747870988879201374, (-36758730064800771), 0], [17938181762601549548, 2783004151496534], [18753656362486765861]], [[(-588676361845983633), 1120526587040830, 0, 0], [(-556667867910675656), (-101787033392384), 0], [(-556660089125819648), (-36548134472067)], [(-588855208016210315)]], [[18620647989628950, (-35047918641699), 0, 0, 0], [17519527496283512, 2917515993788, 0, 0], [17300546964128081, 1361759022586, 0], [17519220451482507, 721315403637], [18626263698526077]]], r := 29322240276498015, ok := true }, iE := { p := [[[9042644516922593317222]], [[(-57708659151608435791), 0], [(-261391643525671370623)]], [[463586623838771839, 0, 0], [1665345719132172599, 0], [8044795122907320123]], [[(-4591386133592020), 0, 0, 0], [(-13045218233153465), 0, 0], [(-51223453930125105), 0], [(-251934209161613852)]], [[57253308178936, 0, 0, 0, 0], [124805087586922, 0, 0, 0], [397618691488221, 0, 0], [1603564944236063, 0], [7954154270468022]]], r := 957064667644446, ok := true }, iHu := { p := [[[20731256748794081302504]], [[(-606640391592553892674), 0], [(-606640391592553892674)]], [[18753380179161322306, 0, 0], [17937715468244008961, 0], [18753380179161322306]], [[(-588849757251356022), 0, 0, 0], [(-556653776325461952), 0, 0], [(-556653776325461952), 0], [(-588849757251356022)]], [[18626138750482880, 0, 0, 0, 0], [17519094630284737, 0, 0, 0], [17300355232363778, 0, 0], [17519094630284737, 0], [18626138750482880]]], r := 29319809837130531, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[37630846406062624]], [[240153827209504, 0], [1087777891847323]], [[(-396587709766), 0, 0], [6953722232386, 0], [(-2034404721216)]], [[4264139698, 0, 0, 0], [(-12793884762), 0, 0], [(-12793884762), 0], [21870909136]], [[(-68776446), 0, 0, 0, 0], [137552893, 0, 0, 0], [(-23641), 0, 0], [137552893, 0], [(-352756613)]]], r := 248167962, ok := true }, de := { p := [[[(-129971375236144669933)]], [[429266946432983718, 0], [429266946432983718]], [[(-6923263815910810), 0, 0], [793220855276, 0], [(-6923263815910810)]], [[148887394379139, 0, 0, 0], [1465754, 0, 0], [1465754, 0], [148887394379139]], [[(-3602114380139), 0, 0, 0, 0], [3, 0, 0, 0], [23646, 0, 0], [3, 0], [(-3602114380139)]]], r := 960563838618, ok := true }, dde := { p := [[[(-232319492966664430538956)]], [[7493747900936766648714, 0], [7493747900936766648399]], [[(-241733804049291011804), 0, 0], [(-241733804842557307218), 0], [(-241733804049291011903)]], [[7797864646749872367, 0, 0, 0], [7797864646746943997, 0, 0], [7797864646746944000, 0], [7797864646749871482]], [[(-251544020862888580), 0, 0, 0, 0], [(-251544020862896378), 0, 0, 0], [(-251544020862937127), 0, 0], [(-251544020862896350), 0], [(-251544020862890546)]]], r := 50597968985090332, ok := true }, nJu := { p := [[[(-259942750472289339866)]], [[858533892865967437, 0], [858533892865967437]], [[(-13846527631821619), 0, 0], [1586441710553, 0], [(-13846527631821619)]], [[297774788758279, 0, 0, 0], [2931508, 0, 0], [2931508, 0], [297774788758279]], [[(-7204228760278), 0, 0, 0, 0], [6, 0, 0, 0], [47292, 0, 0], [6, 0], [(-7204228760278)]]], r := 1921127677228, ok := true }, Jd1 := { p := [[[(-464638985933328861077912)]], [[14987495801873533297428, 0], [14987495801873533296799]], [[(-483467608098582023608), 0, 0], [(-483467609685114614435), 0], [(-483467608098582023805)]], [[15595729293499744735, 0, 0, 0], [15595729293493887994, 0, 0], [15595729293493888001, 0], [15595729293499742965]], [[(-503088041725777159), 0, 0, 0, 0], [(-503088041725792755), 0, 0, 0], [(-503088041725874254), 0, 0], [(-503088041725792699), 0], [(-503088041725781091)]]], r := 101195937970180654, ok := true }, term0 := { p := [[[4057276429862162980798209222]], [[(-261737284132013181962882726), 0], [(-261706342205196410786376732)]], [[12664344696012569891640777, 0, 0], [16883554940868695102972154, 0], [12662348442663001555931635]], [[(-544695199813313750881560), 0, 0, 0], [(-816934510018988973274836), 0, 0], [(-816902312384318534591193), 0], [(-544598606909302367000467)]], [[21963327463488584426171, 0, 0, 0, 0], [35136716628838810176637, 0, 0, 0], [39527153928370919237335, 0, 0], [35134639362085875879619, 0], [21959172929982787426256]]], r := 8338995187245549415637, ok := true }, r0 := { p := [[[19913906722318763747354]], [[(-461865704690546594883), 13243099066761265242949], [(-572820383399391250829)]], [[9134353856516245801, (-306081801052456282862), 2185351249960727891020], [13014151578546864827, (-381153150876421782166)], [17598278849907790777]], [[(-193521210354808803), 6034666468561661341, (-49799894266730402595), (-7237039191408366417)], [(-248591304493471793), 8635980719725238770, (-63041726112569692653)], [(-396833703899037377), 11711850181015909642], [(-550528338265152659)]], [[4658458594038221, (-127721043606313178), 969418335907553484, 401011048619224083, (-586380879380621170)], [5091078913706403, (-164545674252527003), 1412665759189754833, 160642351502938029], [7482119285931720, (-263436373408048865), 1938441960563065266], [12358204089156963, (-366418478190882642)], [17368429850061704]]], r := 481763581349966303, ok := true }, r1 := { p := [[[139505000918978189277701]], [[(-3168314658594589715585), 0], [(-4026547785310514215328)]], [[61517032110978140605, 0, 0], [89978499494339122183, 0], [123831982759981848280]], [[(-1296283008566271916), 0, 0, 0], [(-1692874421501844519), 0, 0], [(-2750207799099055696), 0], [(-3876129271733257096)]], [[31381254731510959, 0, 0, 0, 0], [34508907605695635, 0, 0, 0], [51122431243590475, 0, 0], [85764112202033388, 0], [122335965818567821]]], r := 131773500803331851, ok := true }, r2 := { p := [[[531541176352260304563082007]], [[(-13780863481149322542609603), 37038669107515878478662], [(-33487812137943727631175623)]], [[356361561610769648231963, (-670095667521317966816), 450546971019999263], [852876361072676530063391, (-1169375743216848920025)], [1597243250439479353121305]], [[(-10068468989714097988812), 14200864351885528667, 177278615172419, (-13999763230067)], [(-21795204276996967617097), 20301353479296351727, 86497310342659], [(-40229681469959727024428), 37397889904988831328], [(-68003891524473766871744)]], [[302046324653590204174, (-358882807966240982), (-6639482321591), (-1312921650470), (-1239266489427)], [612477569427939020938, (-415879168134153489), (-4136421233364), (-7762553021815)], [1020402487871068112719, (-638308362914081023), (-6822304833317)], [1699151245800715984253, (-1200045571797864402)], [2720803668215645456017]]], r := 7200809570345976900462, ok := true }, r3 := { p := [[[8109218244752973967648649430]], [[(-523163727615081768181553773), 590301597264846821501560], [(-523240437701025214088118774)]], [[25314185852881389853307644, (-34417129549935095264877), 1676446164770811569], [33757075179564633776451160, (-19075070511858078290780)], [25319138601633166623409551]], [[(-1088778125130362258700783), 1606263522243922111418, 7837806123621874, (-665670443785007)], [(-1633400847125658324143231), 1111745227211594352872, (-401416916148971)], [(-1633480834166017678350595), 615712397271303970279], [(-1089017878809031573222375)]], [[43902244509997705380131, (-67820017921299851258), (-998070670739730), (-953455720007317), (-120663272414011)], [70253669940363105494532, (-51878525850759390279), (-477775649775146), (-660836461980582)], [79039201687295097370747, (-35881698079031120307), (-92560232317475)], [70258831418017900050695, (-19869995547858095238)], [43912559505968464065464]]], r := 933791310173765339661981, ok := true }, eta := { p := [[[(-532146783126484695368479339)]], [[13800459568424042853759372, 0], [33507039372541511940380364]], [[(-356975119239176583231676), 0, 0], [(-853494709140335143313492), 0], [(-1597859638986063129762235)]], [[10087895662123363373995, 0, 0, 0], [21814532026543403924492, 0, 0], [40249456559093341654767, 0], [68023700300079078236045]], [[(-302666725805288424469), 0, 0, 0, 0], [(-613089550362240297009), 0, 0, 0], [(-1021020228618283233451), 0, 0], [(-1699785828581781518895), 0], [(-2721440966107637299403)]]], r := 648762143626572053253, 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 3940649673949184 4503599627370496 4611686018427387904 9223372036854775808 3458764513820540928 4611686018427387904 :=
  (RegionPosI.split_s 4035225266123964416 (RegionPosI.split_s 3746994889972252672 (RegionPosI.split_b 4222124650659840 (RegionPosI.of_check c0 q0 ok_0 3940649673949184 4222124650659840 4611686018427387904 9223372036854775808 3458764513820540928 3746994889972252672 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 4222124650659840 4503599627370496 4611686018427387904 9223372036854775808 3458764513820540928 3746994889972252672 (by decide +kernel))) (RegionPosI.split_b 4222124650659840 (RegionPosI.of_check c2 q2 ok_2 3940649673949184 4222124650659840 4611686018427387904 9223372036854775808 3746994889972252672 4035225266123964416 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 4222124650659840 4503599627370496 4611686018427387904 9223372036854775808 3746994889972252672 4035225266123964416 (by decide +kernel)))) (RegionPosI.split_b 4222124650659840 (RegionPosI.split_s 4323455642275676160 (RegionPosI.of_check c4 q4 ok_4 3940649673949184 4222124650659840 4611686018427387904 9223372036854775808 4035225266123964416 4323455642275676160 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 3940649673949184 4222124650659840 4611686018427387904 9223372036854775808 4323455642275676160 4611686018427387904 (by decide +kernel))) (RegionPosI.split_s 4323455642275676160 (RegionPosI.of_check c6 q6 ok_6 4222124650659840 4503599627370496 4611686018427387904 9223372036854775808 4035225266123964416 4323455642275676160 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 4222124650659840 4503599627370496 4611686018427387904 9223372036854775808 4323455642275676160 4611686018427387904 (by decide +kernel)))))

end CKLaneC.RSC2.S02_0060