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

import Definitions.Def_CK_CKLaneC_RSC2_BD_0063_part01

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

namespace CKLaneC.RSC2.BD_0063
open CKLaneC.TM3 CKLaneC.RSCell

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

noncomputable def c7 : Cell := { bc := 9079256848778919936, bh := 144115188075855872, tc := 8935141660703064064, th := 288230376151711744, sc := 15294224334550204416, sh := 126100789566373888 }
noncomputable def q7 : Cert := { V0 := [[[760036404027969701]], [[(-31020008435975631), 24457297922476203], [10565276364563910]], [[36670184386750, (-993301501018143), (-2895111118531)], [(-388790442076672), 338314056014947], [94689637771699]], [[(-504729245786), 874822379992, 353643086370, (-30681217551)], [(-973032608362), (-12245629567768), (-120449256153)], [(-2758101080155), 2997354244526], [1325554017134]], [[1401245227, (-11398807833), (-14766107261), 3711159199, 10784445], [(-14284764314), (-43047857707), 14206162063, (-1264004254)], [(-30586721995), (-82522550113), (-2743957673)], [(-34546450438), 41663180825], [14780084861]]], r0 := 66218660768, V1 := [[[1562887223253926433]], [[(-63283578298840512), 0], [21554104198448472]], [[44277614740399, 0, 0], [(-772368420045582), 0], [189633319240911]], [[(-563230390366), 0, 0, 0], [(-3177892406850), 0, 0], [(-5042472045621), 0], [2625181370212]], [[1053849404, 0, 0, 0, 0], [(-14895004372), 0, 0, 0], [(-85626648605), 0, 0], [(-59603005654), 0], [28569036007]]], r1 := 58444137696, V2 := [[[1050339330533275381]], [[(-31181163266777927), 24375529934790832], [(-279822966293759501)]], [[39879741449982, (-987119794960535), (-3979123398262)], [(-226735154185695), 431033942955767], [177430275334321]], [[(-508992964134), 749388900502, 441019571487, (-30075063544)], [(-4078218198523), (-18811655379098), 924856022997], [(-3551952730787), (-7784507590539)], [3940943228552]], [[1446198785, (-10914088207), (-16566553515), 3616381289, 14675288], [(-10259310308), 80611389165, (-69892750843), (-1931168546)], [(-135168857160), 295595392166, 36100434103], [(-142262644134), (-129134592260)], [(-24433649546)]]], r2 := 362198569880, V3 := [[[1823440666278989301]], [[(-63669919597598418), 48663335643481958], [(-271730202405765873)]], [[132765174281820, (-1964173859171532), (-27677225440152)], [(-445374036714173), 908136339424664], [336144141039111]], [[(-1811893163952), 1043240159446, 3215900517595, (-229106971464)], [(-7284665453269), (-41726131595139), 3156506042954], [(-5747588975142), (-14873410219610)], [7950393130156]], [[6062071342, (-10166771820), (-128377220290), 26665626997, 401124382], [(-49830069574), 275633562772, (-212444546729), (-17420214410)], [(-293059728982), 543992313782, 143718456695], [(-293667560585), (-247664695550)], [(-46212357706)]]], r3 := 943181868540, Vm := [[[2410156483741284060]], [[(-87835639254082955), 0], [(-186236139490872634)]], [[25706249929289, 0, 0], [(-1927015132554372), 0], [7387557466486211]], [[226808403650, 0, 0, 0], [(-20579628270292), 0, 0], [215841696950107, 0], [572539613581485]], [[15610807946, 0, 0, 0, 0], [(-688267943116), 0, 0, 0], [5808119718976, 0, 0], [43340115832574, 0], [32939971351845]]], rm := 320605198955503 }
noncomputable def w7 : Wit := { Z0 := { p := [[[760968506181384298]], [[(-31134251342866959), 24547371167141428], [10604186988540345]], [[41479665853714, (-1004330688479580), 0], [(-393406489580195), 342070548017430], [95580626856158]], [[(-581873779260), 1338053737216, 0, 0], [(-790044324456), (-12690531921942), 0], [(-2859060022062), 3083246027618], [1342693629638]], [[1812538037, (-18770121912), 0, 0, 0], [(-16831673516), (-25485300789), 0, 0], [(-26926377565), (-92227742648), 0], [(-36397961044), 43312697730], [15082643939]]], r := 13440786017, ok := true }, Z1 := { p := [[[1571031754697051455]], [[(-64277164062693076), 0], [21892515073115552]], [[85635439181863, 0, 0], [(-812194043004273), 0], [197327745767553]], [[(-1201287802343), 0, 0, 0], [(-1631059250488), 0, 0], [(-5902575529419), 0], [2772012654737]], [[3742014013, 0, 0, 0, 0], [(-34749261452), 0, 0, 0], [(-55589940778), 0, 0], [(-75144177639), 0], [31138361680]]], r := 12774418535, ok := true }, Z2 := { p := [[[1052802794945063335]], [[(-31400982468092624), 24547371167141428], [(-281795646415855533)]], [[46718028957564, (-1004330688479580), 0], [(-110644581440120), 342070548017430], [706757697092945]], [[(-595490041428), 1338053737216, 0, 0], [(-5942662802409), (-12690531921942), 0], [(-18774538878512), 3083246027618], [(-44499132103376)]], [[1963002716, (-18770121912), 0, 0, 0], [(-2698560539), (-25485300789), 0, 0], [(-109567959314), (-92227742648), 0], [(-146893874720), 43312697730], [233586857190]]], r := 31667165417, ok := true }, Z3 := { p := [[[1836405483757881966]], [[(-65035946795344466), 49707399157966882], [(-277560127263238381)]], [[184009305457389, (-2080293136859387), 0], [(-41843744726292), 611896136772572], [1224838754441378]], [[(-2648772402260), 5572812065988, 0, 0], [(-15258327044101), (-20107984524523), 0], [(-36068695697151), 4204437577638], [(-40402962504916)]], [[13769967825, (-83879162821), 0, 0, 0], [4923377136, (-131715738709), 0, 0], [(-172776563952), (-50732131478), 0], [(-150901206071), 53121736559], [367655045224]]], r := 64135128282, ok := true }, iE := { p := [[[18677394480875458359]], [[(-17070792014442596), 0], [(-36194857005877868)]], [[335255238646346, 0, 0], [1025970106522222, 0], [2920475489276496]], [[(-871440778743), 0, 0, 0], [5487656057338, 0, 0], [7379459709435, 0], [(-13401357636427)]], [[9629739447, 0, 0, 0, 0], [33078451798, 0, 0, 0], [198594825384, 0, 0], [307721234168, 0], [582912011666]]], r := 66894994360, ok := true }, iHu := { p := [[[18910471031098151941]], [[(-34999011373023651), 0], [(-67379049105889067)]], [[720136410351172, 0, 0], [2217230261145417, 0], [2669027024323905]], [[(-3105174709194), 0, 0, 0], [4927505126088, 0, 0], [9486285378797, 0], [(-22156101325727)]], [[37574697664, 0, 0, 0, 0], [141485270709, 0, 0, 0], [447681995895, 0, 0], [524383999529, 0], [516145206032]]], r := 108799612514, ok := true }, T := { p := [[[8935141660703064064]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18218942008713655353]], [[16651774961031067, 0], [35306423574176322]], [[(-311806701408344), 0, 0], [(-936247968852952), 0], [(-2780369750048121)]], [[266169185436, 0, 0, 0], [(-8361362595043), 0, 0], [(-16097044995899), 0], [2163681206638]], [[(-2776301586), 0, 0, 0, 0], [(-8704687745), 0, 0, 0], [(-91497027044), 0, 0], [(-32262008275), 0], [(-104327736481)]]], r := 48711876707, ok := true }, de := { p := [[[(-4949164280481323963)]], [[185347519124692031, 0], [356825496001958127]], [[(-237328758321966), 0, 0], [2028227669483323, 0], [(-879606780750983)]], [[3300638563495, 0, 0, 0], [11528625407517, 0, 0], [22194564560049, 0], [23550778716549]], [[(-11900706888), 0, 0, 0, 0], [65529726168, 0, 0, 0], [280730828120, 0, 0], [242871499794, 0], [(-163474177847)]]], r := 39171632874, ok := true }, dde := { p := [[[(-55088140650139759146)]], [[141075532928692984, 0], [271594393325306896]], [[(-2943002025812499), 0, 0], [(-9092264647004033), 0], [(-10907588932634432)]], [[14148294360953, 0, 0, 0], [(-11715017288068), 0, 0], [(-22553400629409), 0], [100951177568041]], [[(-174157048406), 0, 0, 0, 0], [(-667399444046), 0, 0, 0], [(-2020262477331), 0, 0], [(-2473569071883), 0], [(-2392310017546)]]], r := 991929582256, ok := true }, nJu := { p := [[[(-9898328560962647926)]], [[370695038249384062, 0], [713650992003916254]], [[(-474657516643932), 0, 0], [4056455338966647, 0], [(-1759213561501965)]], [[6601277126991, 0, 0, 0], [23057250815034, 0, 0], [44389129120098, 0], [47101557433098]], [[(-23801413775), 0, 0, 0, 0], [131059452336, 0, 0, 0], [561461656240, 0, 0], [485742999588, 0], [(-326948355693)]]], r := 78343265743, ok := true }, Jd1 := { p := [[[(-110176281300279518292)]], [[282151065857385969, 0], [543188786650613793]], [[(-5886004051624997), 0, 0], [(-18184529294008066), 0], [(-21815177865268864)]], [[28296588721907, 0, 0, 0], [(-23430034576136), 0, 0], [(-45106801258817), 0], [201902355136082]], [[(-348314096811), 0, 0, 0, 0], [(-1334798888092), 0, 0, 0], [(-4040524954661), 0, 0], [(-4947138143766), 0], [(-4784620035092)]]], r := 1983859164505, ok := true }, term0 := { p := [[[341764662365814707937]], [[(-1738464649658067009), 0], [(-3019263360183032345)]], [[38696504193012613, 0, 0], [107732751526677973, 0], [117108243275395320]], [[(-267706664950381), 0, 0, 0], [(-219125298525019), 0, 0], [(-449055682881468), 0], [(-1544866487427396)]], [[3576478084122, 0, 0, 0, 0], [13175810293768, 0, 0, 0], [33984876005056, 0, 0], [42866373154326, 0], [37586628296113]]], r := 8694316528869, ok := true }, r0 := { p := [[[26622426624934623750]], [[(-130585815265170341), 1710837978140718270], [(-116266196390324450)]], [[2890711223570613, (-7845839535658434), 27161346697892461], [3324978411458036, (-7657576435304510)], [3575235875182018]], [[(-16291976235980), 171619531423296, (-89503985240891), (-13840265576479)], [28518005592165, 226414849875057, (-133511773118575)], [(-4058504328121), 227648411905026], [(-36909643940069)]], [[206174565378, (-909447214678), 1828864136198, 1174616875945, (-106750151510)], [326967342694, 1611017947413, 4404146864490, (-316486816766)], [1139582621595, (-56287352829), 3480319377227], [717378262449, (-2429337570214)], [682007479543]]], r := 2385182498459, ok := true }, r1 := { p := [[[112039003227647660538]], [[(-435167700735338419), 0], [(-528260697495309101)]], [[9332319352688504, 0, 0], [16573454720082061, 0], [14619889790175859]], [[(-45778545558785), 0, 0, 0], [82017830420090, 0, 0], [22403636745479, 0], [(-166954544456860)]], [[564498093555, 0, 0, 0, 0], [1385760643881, 0, 0, 0], [4475493904482, 0, 0], [3561818019227, 0], [2756785974521]]], r := 4698728379931, ok := true }, r2 := { p := [[[27225497053181007545]], [[(-154542369980549461), 1723172021814890370], [(-778117412720838974)]], [[3024413192687943, (-8354897396451341), 26894457580447221], [27466164173319501, (-20044108568498932)], [62922538175497324]], [[(-18330872289579), 173200462836671, (-77806928784638), (-16335652646048)], [(-113744715893486), 726197863711504, 146950076051740], [(-205173667167436), 276449607975376], [(-620720019275452)]], [[218792000546, (-932474514630), 1729700894584, 1275644705934, (-102676548480)], [2368944534867, 109609604532, (-7313877666440), 2110396969608], [9616243277340, 9374411543316, (-10084733370592)], [17178408073861, 1276408446144], [18194443746897]]], r := 20574802796032, ok := true }, r3 := { p := [[[114569694901200839129]], [[(-1104027164760819027), 7161471203773794655], [(-3187833631936753034)]], [[24635139751829538, (-55792949705949586), 105876981218291510], [120849485595369650, (-81496817444378740)], [178325263203339804]], [[(-202884594085602), 1230446863018500, (-151495576039426), (-242098337917660)], [(-679450884882367), 2708367625477539, 1003640499001991], [(-1055027143285039), 1022731012244649], [(-2206983725922088)]], [[2706927689847, (-7764347453651), 951520861525, 19731374538504, (-1379409629351)], [15664884543355, 11176015828983, (-52879348555934), 12399099780673], [42958957635219, 41636687673813, (-38013205426975)], [61029397796469, 4369912894680], [53866733313832]]], r := 187589578616522, ok := true }, eta := { p := [[[(-224139539724842846050)]], [[854502716348495717, 0], [1664304945139570263]], [[(-18118929063087841), 0, 0], [(-56347680209723935), 0], [(-77063079903236044)]], [[97466629004127, 0, 0, 0], [(-9037179505657), 0, 0], [60152068174523, 0], [854216858528376]], [[(-1213327561374), 0, 0, 0, 0], [(-4724155264437), 0, 0, 0], [(-15324827136305), 0, 0], [(-22607242418063), 0], [(-24181354112927)]]], r := 115036622444145992, 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 8646911284551352320 9223372036854775808 6917529027641081856 9223372036854775808 14915921965851082752 15420325124116578304 :=
  (RegionPosI.split_t 8070450532247928832 (RegionPosI.split_s 15168123544983830528 (RegionPosI.of_check c0 q0 ok_0 8646911284551352320 9223372036854775808 6917529027641081856 8070450532247928832 14915921965851082752 15168123544983830528 (by decide +kernel)) (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c1 q1 ok_1 8646911284551352320 8935141660703064064 6917529027641081856 8070450532247928832 15168123544983830528 15420325124116578304 (by decide +kernel)) (RegionPosI.of_check c2 q2 ok_2 8935141660703064064 9223372036854775808 6917529027641081856 8070450532247928832 15168123544983830528 15420325124116578304 (by decide +kernel)))) (RegionPosI.split_s 15168123544983830528 (RegionPosI.of_check c3 q3 ok_3 8646911284551352320 9223372036854775808 8070450532247928832 9223372036854775808 14915921965851082752 15168123544983830528 (by decide +kernel)) (RegionPosI.split_t 8646911284551352320 (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c4 q4 ok_4 8646911284551352320 8935141660703064064 8070450532247928832 8646911284551352320 15168123544983830528 15420325124116578304 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 8935141660703064064 9223372036854775808 8070450532247928832 8646911284551352320 15168123544983830528 15420325124116578304 (by decide +kernel))) (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c6 q6 ok_6 8646911284551352320 8935141660703064064 8646911284551352320 9223372036854775808 15168123544983830528 15420325124116578304 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 8935141660703064064 9223372036854775808 8646911284551352320 9223372036854775808 15168123544983830528 15420325124116578304 (by decide +kernel))))))

end CKLaneC.RSC2.BD_0063