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

import Definitions.Def_CK_CKLaneC_RSC2_S01_0030_part01

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

namespace CKLaneC.RSC2.S01_0030
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def q7 : Cert := { V0 := [[[1146362656110063771]], [[(-9354233319276333), 227997030583111901], [2297199206556439]], [[39090338881513, (-1839653860322985), (-380141607451009)], [(-19096892639147), 451779557343709], [(-19846781951083)]], [[(-233075004954), 7433820615946, 9255645098389, (-24512476825586)], [92177279866, (-3630994946690), (-2272988052627)], [164492830731, (-3918487093120)], [258109233789]], [[2138511519, (-43032087047), (-113183632587), 583313953012, 122495535838], [(-705985308), 16066592213, 55489423714, (-143249404233)], [(-772067791), 31650950501, 15144281693], [(-2136713879), 51015605472], [(-3900232513)]]], r0 := 707880008200, V1 := [[[1826281620502902321]], [[(-14774585749359103), 0], [3628321584697602]], [[60196817086473, 0, 0], [(-29404034378663), 0], [(-31440241375910)]], [[(-351274037068), 0, 0, 0], [133204310421, 0, 0], [255517705736, 0], [409222910384]], [[3225745455, 0, 0, 0, 0], [(-992360945), 0, 0, 0], [(-1140834558), 0, 0], [(-3327297421), 0], [(-6186604792)]]], r1 := 134744952956, V2 := [[[18444926088637585876]], [[(-7365766049216), 19360217641], [(-38549223274808)]], [[7800656616, (-8442485), (-197681)], [(-158606792600), 826241991], [1666650772]], [[(-83392582), (-440275), 976, 2], [181785496, (-331425), (-12667)], [(-23995675), 8845975], [(-9403159)]], [[1219529, 1262, 4, (-1), 0], [(-1943215), (-19091), 62, 0], [200105, (-2868), (-271)], [134486, 481], [90594]]], r2 := 157532594, V3 := [[[18446291870985271913]], [[(-12919954426456), 9523031604], [(-9621946777405)]], [[3621444, 230944863, (-193122)], [(-274907515527), 406715244], [(-13081357)]], [[1205, (-1207285), (-3834), 4], [154379, 9870265, (-12375)], [(-317970), 4361247], [(-866)]], [[(-14), (-401), 45, 0, 0], [55, (-51469), (-246), 0], [1648, 106006, (-265)], [(-26), 294], [4]]], r3 := 1120463677, Vm := [[[18444926153424372076]], [[(-7365862251356), 0], [(-38546443999303)]], [[7799751540, 0, 0], [(-158610947495), 0], [1696742965]], [[(-83393658), 0, 0, 0], [181746574, 0, 0], [(-24041268), 0], [(-9398629)]], [[1219561, 0, 0, 0, 0], [(-1943260), 0, 0, 0], [199681, 0, 0], [134475, 0], [90575]]], rm := 17996137 }
noncomputable def w7 : Wit := { Z0 := { p := [[[1149567179108329646]], [[(-9432859350895559), 229913435821665929], [2316508074668396]], [[40064174347185, (-1886571870179112), 0], [(-19574336428959), 463301614933679], [(-19974686783844)]], [[(-242222466999), 8012834869437, 0, 0], [98233842649, (-3914867285792), 0], [167641719475, (-3994937356769)], [259632914127]], [[2222667587, (-48444493400), 0, 0, 0], [(-765838567), 19646768529, 0, 0], [(-811460480), 33528343895, 0], [(-2174185209), 51926582825], [(-3922054199)]]], r := 144031814638, ok := true }, Z1 := { p := [[[1839307486573327433]], [[(-15092574961432894), 0], [3706412919469434]], [[64102678955496, 0, 0], [(-31318938286335), 0], [(-31959498854150)]], [[(-387555947199), 0, 0, 0], [157174148239, 0, 0], [268226751160, 0], [415412662603]], [[3556268140, 0, 0, 0, 0], [(-1225341707), 0, 0, 0], [(-1298336768), 0, 0], [(-3478696334), 0], [(-6275286718)]]], r := 34385906135, ok := true }, Z2 := { p := [[[23763873245421682029137]], [[(-87472600317898864370), 229913435821665929], [(-457793633079312831538)]], [[432446388493397218, (-1886571870179112), 0], [1673283436457994337, 463301614933679], [9327239573263128482]], [[(-3050637458484178), 8012834869437, 0, 0], [(-8021541253878575), (-3914867285792), 0], [(-34004294705628341), (-3994937356769)], [(-193083619212446863)]], [[32144330666529, (-48444493400), 0, 0, 0], [54422258223923, 19646768529, 0, 0], [161120452243496, 33528343895, 0], [702832819749241, 51926582825], [4027070383925640]]], r := 285206308293667, ok := true }, Z3 := { p := [[[84744960593555867630881]], [[(-2224619552224197339155), 1639721132378229745], [(-1656752820090881566937)]], [[61207025992132637771, (-50462759402288541), 0], [43830252068870980789, 2834231819786461], [33944699927937370589]], [[(-1707232022290097985), 1379034965103581, 0, 0], [(-1209562251516381868), (-80645022637201), 0], [(-900735339630137120), (-25252293077996)], [(-705071269449055030)]], [[47929783905255914, (-38391215169781), 0, 0, 0], [33799754733862845, 2102460135665, 0, 0], [24887295296057879, 729903945041, 0], [18743573528775171, 331912759877], [14740626234120432]]], r := 34110289723903602, ok := true }, iE := { p := [[[23766984879297440412822]], [[(-87478851609341574821), 0], [(-457787362784605742692)]], [[432483864684803916, 0, 0], [1673269307203378745, 0], [9327185506034014930]], [[(-3050942241805466), 0, 0, 0], [(-8021427860694735), 0, 0], [(-34004175966439686), 0], [(-193082916441364370)]], [[32147871815681, 0, 0, 0, 0], [54421142850149, 0, 0, 0], [161119551633764, 0, 0], [702831289461482, 0], [4027059767759027]]], r := 285104149252705, ok := true }, iHu := { p := [[[84751957231690857090838]], [[(-2224766118460937056280), 0], [(-1656740726513478586695)]], [[61211105403618345994, 0, 0], [43830026804075302205, 0], [33944592177202653169]], [[(-1707346177627626839), 0, 0, 0], [(-1209556124231318212), 0, 0], [(-900733284031856276), 0], [(-705069853187821706)]], [[47932993637466669, 0, 0, 0, 0], [33799586749117620, 0, 0, 0], [24887239218735024, 0, 0], [18743546283442449, 0], [14740604697228580]]], r := 34106696599075235, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[14317439450106526]], [[52698024904816, 0], [275775109084274]], [[(-66567082575), 0, 0], [1022092109034, 0], [(-306940651087)]], [[633964446, 0, 0, 0], [(-1416338265), 0, 0], [(-1054719984), 0], [2176709149]], [[(-9056635), 0, 0, 0, 0], [13488606, 0, 0, 0], [(-369), 0, 0], [7480101, 0], [(-23156480)]]], r := 13730339, ok := true }, de := { p := [[[(-150489556868332964738)]], [[380190748205618050, 0], [283120769940353867]], [[(-5431229835038956), 0, 0], [99143678536, 0], [(-3011886169272395)]], [[103451996873425, 0, 0, 0], [34718, 0, 0], [25855, 0], [42721789641487]], [[(-2216828504431), 0, 0, 0, 0], [1, 0, 0, 0], [370, 0, 0], [1, 0], [(-681730685769)]]], r := 320084287121, ok := true }, dde := { p := [[[(-1085709328314428328441016)]], [[31019886327861422343886, 0], [23099915350535101729553]], [[(-886282466643463684691), 0, 0], [(-659997581642149789834), 0], [(-491487560723514248175)]], [[25322356189813256411, 0, 0, 0], [18857073758371480434, 0, 0], [14042501734957527505, 0], [10457182143053503410]], [[(-723495891137485745), 0, 0, 0, 0], [(-538773535953471045), 0, 0, 0], [(-401214335284496696), 0, 0], [(-298776632658671048), 0], [(-222493237086210941)]]], r := 69239282638906809, ok := true }, nJu := { p := [[[(-300979113736665929476)]], [[760381496411236101, 0], [566241539880707735]], [[(-10862459670077911), 0, 0], [198287357072, 0], [(-6023772338544790)]], [[206903993746851, 0, 0, 0], [69437, 0, 0], [51710, 0], [85443579282975]], [[(-4433657008861), 0, 0, 0, 0], [2, 0, 0, 0], [741, 0, 0], [2, 0], [(-1363461371538)]]], r := 640168574233, ok := true }, Jd1 := { p := [[[(-2171418656628856656882032)]], [[62039772655722844687772, 0], [46199830701070203459107]], [[(-1772564933286927369381), 0, 0], [(-1319995163284299579667), 0], [(-982975121447028496349)]], [[50644712379626512823, 0, 0, 0], [37714147516742960869, 0, 0], [28085003469915055011, 0], [20914364286107006821]], [[(-1446991782274971490), 0, 0, 0, 0], [(-1077547071906942089), 0, 0, 0], [(-802428670568993392), 0, 0], [(-597553265317342095), 0], [(-444986474172421882)]]], r := 138478565277813608, ok := true }, term0 := { p := [[[88594574125695248982065990846]], [[(-5062454029435983240282391736), 0], [(-3769743615731052782209893934)]], [[216960986123557841627843278, 0, 0], [215411940906173296962994640, 0], [120308431787938478293564452]], [[(-8265155101398403289961202), 0, 0, 0], [(-9231912038939619044115528), 0, 0], [(-6874725403234145579854736), 0], [(-3412969204316512164202166)]], [[295183568142304668133346, 0, 0, 0, 0], [351691348424163756818482, 0, 0, 0], [294630486888531029843093, 0, 0], [195025915345331400452424, 0], [90769883846899717498051]]], r := 51744429726743329199771, ok := true }, r0 := { p := [[[186720090395070519682068]], [[(-2842059340050938682121), 74041691700921922843011], [(-3557652939416028392049)]], [[44398133719020803188, (-1117134487132416514404), 7148160216570827696162], [52526664182588195909, (-1413284299167102843624)], [72186849783614400097]], [[(-884930043749192122), 17396006587323194943, (-103955013236700824277), (-50200073415181940737)], [(-788865158692832666), 20717627223682930373, (-137445889303786410316)], [(-1053397874942733850), 28692768470585349474], [(-1490612014147797468)]], [[21152507779394722, (-347796407853001295), 1597248769857172603, 1505394426834523285, (-2263462547842268459)], [15338598205330819, (-310298370527429308), 1955837294766152603, 765294507702002035], [15574361210672903, (-415930969127830013), 2796971325196011426], [21597002975926442, (-592682470598030325)], [31034034002168570]]], r := 854928201333019244, ok := true }, r1 := { p := [[[471647326438916731674549]], [[(-7083569067744298522532), 0], [(-9011067000728448793677)]], [[110144342557400995023, 0, 0], [131592140672087329446, 0], [183000169826319301428]], [[(-2205922247928380169), 0, 0, 0], [(-1968312649439323867), 0, 0], [(-2643351013991333980), 0], [(-3780747238610212635)]], [[53016800620511935, 0, 0, 0, 0], [38433094534644611, 0, 0, 0], [38928991937735449, 0, 0], [54246141197138128, 0], [78741261700555263]]], r := 65503499483296599, ok := true }, r2 := { p := [[[5424888866676617828325504782]], [[(-111230845574019668553407913), 128225246261060420433178], [(-224600180652688985143844402)]], [[2613711993299882462304924, (-1772584505918644129038), 445516944025462605], [4524693678356950643498140, (-2648189172133793542797)], [7048687312372391220773437]], [[(-68713523686429999712571), 34702207571767350237, (-189536374499450), (-605256675093978)], [(-105512081673163910085870), 34962697791236372732, (-309589563613390)], [(-140426836302168125328870), 55659283182014914056], [(-197585068513145490796673)]], [[1890174303918095014893, (-847647770585946228), (-575329666141023), 6829317829243, (-67547846086339)], [2768538990692163142304, (-667101714306251870), (-506433155210524), (-564457378523690)], [3258661698304125254443, (-720921148943786942), (-360737125247253)], [3904613803083742653441, (-1175617371227403567)], [5206685014277803397713]]], r := 12867242359847546903973, ok := true }, r3 := { p := [[[177157646014676684852075845097]], [[(-10123215652754385279068306528), 4482865144881065886348243], [(-7538816655874234367014608997)]], [[433850976940844889406148698, (-240938087086519385430917), 1244081526693037911], [430787858746045169024451190, (-95485924936284622469869)], [240602593174538399789794736]], [[(-16527635178595500864456375), 10109018320005757497809, (-148815895583315652), (-407258292125573914)], [(-18462313015733531917866936), 5130867622104965204468, (-202296612914698801)], [(-13748684271493628211528078), 2032123023914901411546], [(-6825634922791122945542598)]], [[590272173028079587821647, (-381327457449304093084), (-33024284979667426), (-367863789382681286), (-37501357482151350)], [703325770238981236487839, (-215578134259961161528), (-230658919493142563), (-378870066564227590)], [589228587326567749758808, (-109492528246107106919), (-65678037402093556)], [390035312228046819267813, (-43609557735693798283)], [181533152306512598658737]]], r := 5187457203021202009116800, ok := true }, eta := { p := [[[(-5427399395892048409884588057)]], [[111304399923940522905064678, 0], [224652851441522364649598876]], [[(-2615793701753656084637790), 0, 0], [(-4526233460056755441750723), 0], [(-7049801702236919385981944)]], [[68772667590280079783887, 0, 0, 0], [105555655001136419823742, 0, 0], [140459386264120400732886, 0], [197608697603444770108251]], [[(-1891859518603027351322), 0, 0, 0, 0], [(-2769777664950243933299), 0, 0, 0], [(-3259583273364593533827), 0, 0], [(-3905303879577087969151), 0], [(-5207186616171720170183)]]], r := 915261409247953677312, 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 1407374883553280 1688849860263936 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 :=
  (RegionPosI.split_b 1548112371908608 (RegionPosI.split_s 2449958197289549824 (RegionPosI.split_b 1477743627730944 (RegionPosI.of_check c0 q0 ok_0 1407374883553280 1477743627730944 9223372036854775808 13835058055282163712 2305843009213693952 2449958197289549824 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 1477743627730944 1548112371908608 9223372036854775808 13835058055282163712 2305843009213693952 2449958197289549824 (by decide +kernel))) (RegionPosI.split_b 1477743627730944 (RegionPosI.of_check c2 q2 ok_2 1407374883553280 1477743627730944 9223372036854775808 13835058055282163712 2449958197289549824 2594073385365405696 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 1477743627730944 1548112371908608 9223372036854775808 13835058055282163712 2449958197289549824 2594073385365405696 (by decide +kernel)))) (RegionPosI.split_s 2449958197289549824 (RegionPosI.split_b 1618481116086272 (RegionPosI.of_check c4 q4 ok_4 1548112371908608 1618481116086272 9223372036854775808 13835058055282163712 2305843009213693952 2449958197289549824 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 1618481116086272 1688849860263936 9223372036854775808 13835058055282163712 2305843009213693952 2449958197289549824 (by decide +kernel))) (RegionPosI.split_b 1618481116086272 (RegionPosI.of_check c6 q6 ok_6 1548112371908608 1618481116086272 9223372036854775808 13835058055282163712 2449958197289549824 2594073385365405696 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 1618481116086272 1688849860263936 9223372036854775808 13835058055282163712 2449958197289549824 2594073385365405696 (by decide +kernel)))))

end CKLaneC.RSC2.S01_0030