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

import Definitions.Def_CK_CKLaneC_RSC2_S05_0057_part00

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

namespace CKLaneC.RSC2.S05_0057
open CKLaneC.TM3 CKLaneC.RSCell

theorem sF_2 : stageF w2 = true := by decide +kernel
theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

noncomputable def c3 : Cell := { bc := 25895697857380352, bh := 1125899906842624, tc := 11529215046068469760, th := 2305843009213693952, sc := 6629298651489370112, sh := 288230376151711744 }
noncomputable def q3 : Cert := { V0 := [[[959040556022099163]], [[(-33934504316685819), 191060939062291737], [5301912744446437]], [[401186522134105, (-6707642903180753), (-223122461939129)], [(-184219917503924), 1047999318383530], [(-85938053676856)]], [[(-5817212004836), 76500737898949, 23595497378198, (-14533465346303)], [2204048556496, (-35538915847560), (-3686550629813)], [3008603903096, (-17055231719846)], [2228829058052]], [[99416315143, (-1050872283019), (-1105971239031), 1512822179856, 50614701309], [(-37646246483), 379555230610, 386518029577, (-236362703892)], [(-36028212893), 587664518315, 39566710644], [(-78155121524), 442650474635], [(-67837526408)]]], r0 := 15012363599284, V1 := [[[1529827421880986364]], [[(-53805024292717404), 0], [8406474464768876]], [[618942637371129, 0, 0], [(-286728465285870), 0], [(-136678419891443)]], [[(-8623927738931), 0, 0, 0], [3154076493431, 0, 0], [4726693971443, 0], [3546771906471]], [[142696535717, 0, 0, 0, 0], [(-49173634933), 0, 0, 0], [(-53557254204), 0, 0], [(-122998765040), 0], [(-107986312213)]]], r1 := 6115422585604, V2 := [[[18412112392653994166]], [[(-440450710609616), 4452347559723], [(-1502703212825735)]], [[863500631310, (-51006992272), (-541569635)], [(-19359774371303), 390278637013], [74495291094]], [[(-15016844274), (-1509757833), 19337299, 64487], [42631474527, (-4429396793), (-71305841)], [(-5690375584), 8640618130], [(-1019710321)]], [[347777488, 4474682, 35547, (-3868), (-7)], [(-733872875), (-133962819), 2540191, 11321], [142355798, (-96024530), (-3148379)], [60941242, 3012718], [19279684]]], r2 := 159222782255, V3 := [[[18428117324459860578]], [[(-809521083303442), 4742241196736], [(-810486629761315)]], [[15053163801, 93493851943, (-1146246682)], [(-35209048289095), 415809435524], [(-27580131508)]], [[8692338, (-5023043979), 4879106, 271629], [1319089733, 8223518935, (-150874907)], [(-550539533), 9213325205], [(-9383682)]], [[(-117186), (-2812302), 1775426, (-7694), (-64)], [848419, (-440397752), 631084, 47663], [29181484, 183432755, (-6658780)], [(-267239), 3426725], [64755]]], r3 := 745500481542, Vm := [[[18412126999669380180]], [[(-440664633477692), 0], [(-1501415180612249)]], [[859785175087, 0, 0], [(-19378747107384), 0], [103390225746]], [[(-15009423845), 0, 0, 0], [42304238896, 0, 0], [(-6121309544), 0], [(-1002545840)]], [[347744165, 0, 0, 0, 0], [(-733139274), 0, 0, 0], [135024834, 0, 0], [60588491, 0], [19161277]]], rm := 22708506018 }
noncomputable def w3 : Wit := { Z0 := { p := [[[960914945357810664]], [[(-34133792622657713), 192182989071562132], [5333049465919985]], [[410622457797171, (-6826758524531543), 0], [(-187514105134918), 1066609893183997], [(-86269919540272)]], [[(-6103620780166), 82124491559434, 0, 0], [2359783985931, (-37502821026984), 0], [3043908453882, (-17253983908055)], [2236639354082]], [[106462009909, (-1220724156034), 0, 0, 0], [(-42419481055), 471956797186, 0, 0], [(-37700907288), 608781690776, 0], [(-78986167011), 447327870816], [(-68060920391)]]], r := 3534364106945, ok := true }, Z1 := { p := [[[1537463912572497063]], [[(-54614068196252340), 0], [8532879145471976]], [[656995932475473, 0, 0], [(-300022568215869), 0], [(-138031871264435)]], [[(-9765793248265), 0, 0, 0], [3775654377490, 0, 0], [4870253526211, 0], [3578622966532]], [[170339215854, 0, 0, 0, 0], [(-67871169688), 0, 0, 0], [(-60321451660), 0, 0], [(-126377867218), 0], [(-108897472625)]]], r := 1548530254588, ok := true }, Z2 := { p := [[[1705755682528608340467]], [[(-19011798375622619747), 192182989071562132], [(-64863308907145318228)]], [[266041253907633176, (-6826758524531543), 0], [725345522124574719, 1066609893183997], [2666076582759640656]], [[(-4355967250072710), 82124491559434, 0, 0], [(-9878245815666544), (-37502821026984), 0], [(-29862125769760875), (-17253983908055)], [(-111931046701667482)]], [[82890419039318, (-1220724156034), 0, 0, 0], [155846091750913, 471956797186, 0, 0], [403124164749420, 608781690776, 0], [1254853313024136, 447327870816], [4745361282819317]]], r := 1029002022458692, ok := true }, Z3 := { p := [[[2944953454827320455130]], [[(-113215656106514729341), 663226640513140314], [(-113350692707764488557)]], [[4673488147784173947, (-41655099096425202), 0], [4429744097085542399, 3357101320161203], [4678675780019348047]], [[(-196695545559871085), 1673241576238643, 0, 0], [(-183910516555479136), (-193818857642701), 0], [(-183899120924075827), (-55969168819391)], [(-196909699156084039)]], [[8353324137540730, (-69922310236289), 0, 0, 0], [7766369134549333, 7116868861127, 0, 0], [7651052419525916, 3318325060024, 0], [7765773701691939, 1462221834696], [8362337447034335]]], r := 17027799251405913, ok := true }, iE := { p := [[[1709594654920062227953]], [[(-19031096616958708408), 0], [(-64842002724157081798)]], [[266378520361985134, 0, 0], [725246117783917571, 0], [2665731923910355377]], [[(-4362110766454220), 0, 0, 0], [(-9875816201737188), 0, 0], [(-29860475442055499), 0], [(-111922111054687024)]], [[83017037089597, 0, 0, 0, 0], [155793435334292, 0, 0, 0], [403088038591996, 0, 0], [1254810248443117, 0], [4745089371142245]]], r := 1027791932808554, ok := true }, iHu := { p := [[[2949919566501406652118]], [[(-113325555388123281493), 0], [(-113325555388123281493)]], [[4678256693804041883, 0, 0], [4429315327254949817, 0], [4678256693804041883]], [[(-196898750324297411), 0, 0, 0], [(-183891321076904497), 0, 0], [(-183891321076904497), 0], [(-196898750324297411)]], [[8362002751475456, 0, 0, 0, 0], [7765565311521788, 0, 0, 0], [7650710552640258, 0, 0], [7765565311521788, 0], [8362002751475456]]], r := 17020980171470304, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[199042718074507255]], [[2215730604723458, 0], [7549350034797756]], [[(-6348242539620), 0, 0], [83639628169605, 0], [(-24028825869868)]], [[91957076444, 0, 0, 0], [(-276149861070), 0, 0], [(-276149861070), 0], [347837196498]], [[(-1999067388), 0, 0, 0, 0], [3998131721, 0, 0, 0], [(-6060269), 0, 0], [3998131721, 0], [(-7561689701)]]], r := 8027189834, ok := true }, de := { p := [[[(-101015736286021915514)]], [[578836066889184414, 0], [578836066889184414]], [[(-12577041311655926), 0, 0], [12702893609210, 0], [(-12577041311655926)]], [[364552015001109, 0, 0, 0], [278772377, 0, 0], [278772377, 0], [364552015001109]], [[(-11887565705028), 0, 0, 0, 0], [6118, 0, 0, 0], [6069446, 0, 0], [6118, 0], [(-11887565705028)]]], r := 4322751169020, ok := true }, dde := { p := [[[(-26389287290191018907248)]], [[1146781188731384714293, 0], [1146781188731384714037]], [[(-49860064393278621008), 0, 0], [(-49860077102583994695), 0], [(-49860064393278621474)]], [[2167828886385377907, 0, 0, 0], [2167828885827549316, 0, 0], [2167828885827549337, 0], [2167828886385377840]], [[(-94253429842846761), 0, 0, 0, 0], [(-94253429842864989), 0, 0, 0], [(-94253429855004486), 0, 0], [(-94253429842864987), 0], [(-94253429842847050)]]], r := 25943910533197974, ok := true }, nJu := { p := [[[(-202031472572043831028)]], [[1157672133778368828, 0], [1157672133778368828]], [[(-25154082623311851), 0, 0], [25405787218421, 0], [(-25154082623311851)]], [[729104030002218, 0, 0, 0], [557544754, 0, 0], [557544754, 0], [729104030002218]], [[(-23775131410056), 0, 0, 0, 0], [12237, 0, 0, 0], [12138893, 0, 0], [12237, 0], [(-23775131410056)]]], r := 8645502338033, ok := true }, Jd1 := { p := [[[(-52778574580382037814495)]], [[2293562377462769428587, 0], [2293562377462769428075]], [[(-99720128786557242015), 0, 0], [(-99720154205167989390), 0], [(-99720128786557242948)]], [[4335657772770755814, 0, 0, 0], [4335657771655098633, 0, 0], [4335657771655098675, 0], [4335657772770755680]], [[(-188506859685693521), 0, 0, 0, 0], [(-188506859685729978), 0, 0, 0], [(-188506859710008971), 0, 0], [(-188506859685729973), 0], [(-188506859685694100)]]], r := 51887821066395939, ok := true }, term0 := { p := [[[52434655372371422089246645]], [[(-4556089115380434431131427), 0], [(-4552898072072660142218636)]], [[297061456692088445879973, 0, 0], [395754600183186718155783, 0], [296783974594595418833044]], [[(-17218786182245842434366), 0, 0, 0], [(-25806830871504324261948), 0, 0], [(-25800798651995934724911), 0], [(-17200689523716016509212)]], [[935732906788797985861, 0, 0, 0, 0], [1495953913034460251237, 0, 0, 0], [1682519401507475040175, 0, 0], [1495429372207508628996, 0], [934683825134896115300]]], r := 487918950021725890840, ok := true }, r0 := { p := [[[8329060193535664991910]], [[(-320370063724431914123), 3310994864445377627343], [(-316249221521588041702)]], [[10021562823655825783, (-125919603149978672012), 322904758410636562373], [12000798766553614623, (-125942220346623454535)], [13004481892452932037]], [[(-308728916554745518), 3888198172335676784, (-11710745290399712822), (-1616318179399284914)], [(-363091262303321895), 4740197544948707305, (-12372147228387226171)], [(-491262154243812370), 5181214735442560222], [(-546069774896281929)]], [[10035233721252600, (-118731892365208379), 341529582570494142, 172220096818924166, (-75220807912407494)], [10770374757034872, (-142019548088262821), 450133997713695604, 44050739620830399], [14696215070693225, (-194286695122265535), 509921690098441536], [20573154518994790, (-217619353631078667)], [23153315386585462]]], r := 333809795200366805, ok := true }, r1 := { p := [[[21118626449258255357579]], [[(-798288371199369719316), 0], [(-804067654912586923903)]], [[24486446910573662145, 0, 0], [30128104884854356649, 0], [33087240953048654588]], [[(-744764489653958126), 0, 0, 0], [(-897940510741392837), 0, 0], [(-1235702100196709494), 0], [(-1389911381565150189)]], [[24133946647217149, 0, 0, 0, 0], [26361846404603109, 0, 0, 0], [36458536113920470, 0, 0], [51805455577026657, 0], [58947878358236754]]], r := 109583584154473039, ok := true }, r2 := { p := [[[11701175268234926671044872]], [[(-476285214456236734624610), 5082534658222936382652], [(-991141358996364882396093)]], [[17531233271648295684183, (-147572310150703145198), 459513297325162067], [39576410781637622174556, (-216700398301416790970)], [63645866288532612745434]], [[(-666856686487065780474), 4518175190366918040, 395179188511188, (-52814289928844)], [(-1435221931763887512357), 6017287215060741459, 199935238861579], [(-2511542492493585115373), 9354775810856529557], [(-3650004984178052960955)]], [[26483262813702150612, (-152880183871887681), (-7553815990235), 1253703336290, (-1241715430)], [54101526278020710484, (-177044130154890732), 4896513604635, (-2338218101097)], [90239584271272954391, (-255255680755282141), (-3243675890822)], [142822966042242635312, (-404976447830735455)], [196751070882859488931]]], r := 856241025723074817394, ok := true }, r3 := { p := [[[104522259006097474343176974]], [[(-9085963182670454845128698), 49147590847385754364391], [(-9090688506959043720637627)]], [[592499280456325495041286, (-3719128888655892566948), 1752174864449154615], [790368163119838897164205, (-2143995101903361028431)], [592910759124259171340076]], [[(-34345940516359220964342), 230490054668962822152, 8464702988386942, (-409200872140741)], [(-51543001852715197689749), 162117381262141775078, (-18676418962929)], [(-51551968212149001948247), 93329281039551197540], [(-34372797298436288629555)]], [[1866566976253320875702, (-13012873442272378244), (-408631399329298), 8568496495049, (-70404778912)], [2987920371064990191877, (-10043628569303595117), 74075148295097, (-18079059639865)], [3361965601843110180978, (-7054848133827916837), (-2463058508781)], [2988700485350697860691, (-4060550792430122063)], [1868124721311084344566]]], r := 61523250881932148572377, ok := true }, eta := { p := [[[(-11761324836118919531958606)]], [[479194447053814683978201, 0], [993702895827516353865940]], [[(-17658656791121838880124), 0, 0], [(-39699546285662530433630), 0], [(-63756422024164887435108)]], [[672354587523075357488, 0, 0, 0], [1440596544349212951219, 0, 0], [2516843581260439669689, 0], [3654790804463747257018]], [[(-26720483196087840643), 0, 0, 0, 0], [(-54333137764908057018), 0, 0, 0], [(-90470692765136623987), 0, 0], [(-143052097029098797630), 0], [(-196958516082504875545)]]], r := 92346903422042155377, ok := true } }
theorem sB_3 : stageB c3 w3 = true := by decide +kernel
theorem s0_3 : stageC0 w3 q3 = true := by decide +kernel
theorem s1_3 : stageC1 w3 q3 = true := by decide +kernel
theorem s2_3 : stageC2 w3 q3 = true := by decide +kernel
theorem s3_3 : stageC3 w3 q3 = true := by decide +kernel
theorem sE_3 : stageE w3 q3 = true := by decide +kernel
theorem sF_3 : stageF w3 = true := by decide +kernel
theorem ok_3 : (domOK c3 && cellCheck c3 q3) = true :=
  staged_check c3 q3 w3 (by decide +kernel) sB_3 s0_3 s1_3 s2_3 s3_3 sE_3 sF_3

theorem region : RegionPosI 22517998136852480 27021597764222976 9223372036854775808 13835058055282163712 5764607523034234880 6917529027641081856 :=
  (RegionPosI.split_b 24769797950537728 (RegionPosI.split_s 6341068275337658368 (RegionPosI.of_check c0 q0 ok_0 22517998136852480 24769797950537728 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 22517998136852480 24769797950537728 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel))) (RegionPosI.split_s 6341068275337658368 (RegionPosI.of_check c2 q2 ok_2 24769797950537728 27021597764222976 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 24769797950537728 27021597764222976 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel))))

end CKLaneC.RSC2.S05_0057