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

import Definitions.Def_CK_CKLaneC_RSC2_S06_0012_part00

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

namespace CKLaneC.RSC2.S06_0012
open CKLaneC.TM3 CKLaneC.RSCell

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 := 69805794224242688, bh := 2251799813685248, tc := 11529215046068469760, th := 2305843009213693952, sc := 2738188573441261568, sh := 144115188075855872 }
noncomputable def q7 : Cert := { V0 := [[[1726271643388868817]], [[(-28358926908963509), 340907042651254342], [8073796570683500]], [[247508053530702, (-5458020121547920), (-1284852613174713)], [(-134656712755019), 1553900268565757], [(-92480408405359)]], [[(-3236449543362), 44144080919066, 62546952092075, (-79315177050437)], [1384870436402, (-23928057872935), (-17807139491873)], [1539894212130, (-18082008068566)], [1760681030475]], [[62053823382, (-543254395456), (-1541756816574), 3654020414733, 915890543090], [(-23363014440), 200060012761, 864038613590, (-1040300910836)], [(-15035212062), 287582119777, 123250682978], [(-29280795331), 344917075218], [(-39499831406)]]], r0 := 7691812604236, V1 := [[[2735368522849638120]], [[(-44077817587967352), 0], [12548970334010096]], [[364113845546731, 0, 0], [(-197574253512975), 0], [(-145409202787344)]], [[(-4573461135332), 0, 0, 0], [1771351659414, 0, 0], [2338566556461, 0], [2772566864834]], [[87801270475, 0, 0, 0, 0], [(-28611115628), 0, 0, 0], [(-20957781464), 0, 0], [(-44675651840), 0], [(-62261982635)]]], r1 := 2020804048773, V2 := [[[18370471967025609466]], [[(-659894761395191), 35727043965044], [(-2443342873436705)]], [[1866668923048, (-12493596149), (-15752434742)], [(-21848384826614), 2323818575474], [318696911575]], [[(-36782129483), (-3749679194), 148278556, 6783420], [69193374611, (-433684169), (-1540965159)], [(-11720849204), 38212493944], [(-3128087675)]], [[998842832, 25157142, 1629614, (-125525), (-2884)], [(-1357788602), (-251644353), 14326467, 885232], [189375405, 6766790, (-50616659)], [85145369, 11421250], [43227945]]], r2 := 76376063468, V3 := [[[18425963559018637528]], [[(-1093234631182011), 19022618748859], [(-672208821183044)]], [[26420205307, 841459065605, (-16522721689)], [(-35348706142014), 1240084751399], [(-61053781548)]], [[33199669, (-8849369341), (-587881289), 14066587], [1711987306, 54950609238, (-1616905478)], [(-2719550380), 20509929775], [(-19559780)]], [[(-633583), (-10909377), 14261351, 377045, (-11847)], [2407727, (-574823502), (-57678259), 1835048], [27912164, 912206979, (-53159331)], [(-1035757), 8297656], [78773]]], r3 := 752465546482, Vm := [[[18370598288411184423]], [[(-660311288083348), 0], [(-2435030899243579)]], [[1859007412420, 0, 0], [(-21875893204055), 0], [458918292491]], [[(-36781840500), 0, 0, 0], [68678250326, 0, 0], [(-12187124577), 0], [(-3036517934)]], [[999450737, 0, 0, 0, 0], [(-1357523481), 0, 0, 0], [180218124, 0, 0], [84847713, 0], [42815223]]], rm := 15433145552 }
noncomputable def w7 : Wit := { Z0 := { p := [[[1737262319873698165]], [[(-28903418813435484), 347452463974739633], [8228813609417124]], [[261322135742084, (-5780683762687097), 0], [(-142401989535473), 1645762721883424], [(-93521526134096)]], [[(-3508985821952), 52264427148416, 0, 0], [1587149766020, (-28480397907095), 0], [1591365488794, (-18704305226820)], [1778864431106]], [[67403807759, (-701797164391), 0, 0, 0], [(-27596141538), 317429953204, 0, 0], [(-16328154842), 318273097758, 0], [(-30179826847), 355772886221], [(-39882697588)]]], r := 1408501650870, ok := true }, Z1 := { p := [[[2779619711797917065]], [[(-46245470101496775), 0], [13166101775067398]], [[418115417187335, 0, 0], [(-227843183256757), 0], [(-149634441814554)]], [[(-5614377315123), 0, 0, 0], [2539439625633, 0, 0], [2546184782071, 0], [2846183089769]], [[107846092415, 0, 0, 0, 0], [(-44153826460), 0, 0, 0], [(-26125047746), 0, 0], [(-48287722954), 0], [(-63812316140)]]], r := 527851284912, ok := true }, Z2 := { p := [[[857784452874885362783]], [[(-6417605135065652542), 347452463974739633], [(-23761985529542521456)]], [[70417544254123265, (-5780683762687097), 0], [174546897540048856, 1645762721883424], [719606761344314942]], [[(-1088949270976975), 52264427148416, 0, 0], [(-1799169505019350), (-28480397907095), 0], [(-5264064046279314), (-18704305226820)], [(-22326475780504183)]], [[23322896193661, (-701797164391), 0, 0, 0], [26055505227895, 317429953204, 0, 0], [53224154504489, 318273097758, 0], [162911184316748, 355772886221], [700358307524167]]], r := 110597561139198, ok := true }, Z3 := { p := [[[2673479042532253990160]], [[(-124219105921493198917), 2161450640027584034], [(-76379924654981629064)]], [[6203731124788878915, (-120178153462119133), 0], [3608909598273508981, 8220398373330009], [2337423340106823038]], [[(-315963683939265824), 5932489317492659, 0, 0], [(-181294329175071217), (-405929077275565), 0], [(-111097098936528822), (-101286112747049)], [(-72960588554186686)]], [[16239633421947314, (-301244400778337), 0, 0, 0], [9265173128123741, 18694761710133, 0, 0], [5592989693841807, 5198001326327, 0], [3479738373072090, 1961212478431], [2298305528396284]]], r := 13544851469812869, ok := true }, iE := { p := [[[862575471712995763413]], [[(-6437422442747621419), 0], [(-23739292122469211478)]], [[70691238818422956, 0, 0], [174437871692602655, 0], [719348847851141464]], [[(-1093717935546119), 0, 0, 0], [(-1797099143710321), 0, 0], [(-5262899555943313), 0], [(-22321570031440049)]], [[23432840544318, 0, 0, 0, 0], [26012955786876, 0, 0, 0], [53204407829990, 0, 0], [162889281174962, 0], [700248319093940]]], r := 109897960746899, ok := true }, iHu := { p := [[[2682977527454944015415]], [[(-124560937090167759640), 0], [(-76343800152038279758)]], [[6221152596780565406, 0, 0], [3607834244757866814, 0], [2336978238748971328]], [[(-316855538520859158), 0, 0, 0], [(-181240661358950720), 0, 0], [(-111082985994201078), 0], [(-72951970014946608)]], [[16285579534110686, 0, 0, 0, 0], [9262497710707184, 0, 0, 0], [5592285615335784, 0, 0], [3479460638451656, 0], [2298110178800224]]], r := 13516047584513663, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[394495760753744709]], [[2944131785711072, 0], [10857079076235196]], [[(-10358251883527), 0, 0], [82274781101195, 0], [(-30189473323599)]], [[181621583098, 0, 0, 0], [(-334324952596), 0, 0], [(-204908841914), 0], [323520328541]], [[(-4779516855), 0, 0, 0, 0], [5858757042, 0, 0, 0], [(-6061310), 0, 0], [2200844217, 0], [(-5218135837)]]], r := 8246634655, ok := true }, de := { p := [[[(-99585352623670041501)]], [[700736408194959445, 0], [429483605022717079]], [[(-18430067721073682), 0, 0], [12704348198694, 0], [(-6923261651724870)]], [[646669247227811, 0, 0, 0], [375801221, 0, 0], [230329781, 0], [148887394405544]], [[(-25526417649195), 0, 0, 0, 0], [11117, 0, 0, 0], [6071530, 0, 0], [4176, 0], [(-3602114380139)]]], r := 6152819176413, ok := true }, dde := { p := [[[(-23702431611594767550339)]], [[1246795270367261804423, 0], [764164843128321751824]], [[(-65620824443336990740), 0, 0], [(-40219227692888514081), 0], [(-24650486601503281681)]], [[3453727601667401685, 0, 0, 0], [2116800787366705643, 0, 0], [1297394030966690639, 0], [795176987004020089]], [[(-181775136929880311), 0, 0, 0, 0], [(-111410567795765353), 0, 0, 0], [(-68283896403096057), 0, 0], [(-41851420368648089), 0], [(-25650870548517188)]]], r := 24777645147328640, ok := true }, nJu := { p := [[[(-199170705247340083001)]], [[1401472816389918890, 0], [858967210045434158]], [[(-36860135442147364), 0, 0], [25408696397388, 0], [(-13846523303449739)]], [[1293338494455623, 0, 0, 0], [751602443, 0, 0], [460659563, 0], [297774788811089]], [[(-51052835298389), 0, 0, 0, 0], [22234, 0, 0, 0], [12143061, 0, 0], [8352, 0], [(-7204228760278)]]], r := 12305638352817, ok := true }, Jd1 := { p := [[[(-47404863223189535100677)]], [[2493590540734523608847, 0], [1528329686256643503648]], [[(-131241648886673981480), 0, 0], [(-80438455385777028162), 0], [(-49300973203006563362)]], [[6907455203334803370, 0, 0, 0], [4233601574733411287, 0, 0], [2594788061933381279, 0], [1590353974008040179]], [[(-363550273859760621), 0, 0, 0, 0], [(-222821135591530705), 0, 0, 0], [(-136567792806192113), 0, 0], [(-83702840737296178), 0], [(-51301741097034376)]]], r := 49555290294657272, ok := true }, term0 := { p := [[[42403627293240544657069045]], [[(-4459792321697583833161758), 0], [(-2728273042504744625786589)]], [[351990436483378036384612, 0, 0], [287065978503654439186696, 0], [131893202789185307194065]], [[(-24697629534382422979477), 0, 0, 0], [(-22659928357871020371174), 0, 0], [(-13879602848347305108605), 0], [(-5670245088828024967114)]], [[1624707716961932242291, 0, 0, 0, 0], [1590059000511341079204, 0, 0, 0], [1095655693761967287448, 0, 0], [596742349826050102127, 0], [228576475252991886673]]], r := 391826821691889370884, ok := true }, r0 := { p := [[[6865902251627624358965]], [[(-226990639970261320046), 2693444804400836559101], [(-184974733161301823589)]], [[7605908915360151120, (-87455122797645926923), 248643249296642616146], [5772830109541020666, (-73043581858200703369)], [5568312444204380948]], [[(-300104223612339769), 2912110489307991914, (-7453184151864840266), (-3958230169387019745)], [(-181354070866039885), 2251535146384623471, (-6929871304610847679)], [(-170701620973667517), 2201808812878514946], [(-172110403482370458)]], [[13440856296085323, (-115396797397394822), 241407925340319719, 241332062930519931, (-153999137895910958)], [6884864566003866, (-70437474348107190), 202480438624461374, 73280009515718897], [5251590586033939, (-66734789797317213), 210082567175379379], [5219714126851320, (-68108392640573599)], [5384485673099408]]], r := 246618504457873116, ok := true }, r1 := { p := [[[17065912056646487907776]], [[(-549381043637040474359), 0], [(-464244718151928734829)]], [[18255174812251236675, 0, 0], [14217671704351678996, 0], [14004295968314241386]], [[(-725282962620194173), 0, 0, 0], [(-443943967645283479), 0, 0], [(-421942235211861320), 0], [(-433371546690012492)]], [[32767645242311415, 0, 0, 0, 0], [16959106780406895, 0, 0, 0], [12903047310126782, 0, 0], [12929424634862354, 0], [13568944102247630]]], r := 39652858449929402, ok := true }, r2 := { p := [[[3761508687196987239017880]], [[(-165693919338770839278723), 3395608651991202999035], [(-230584685645137542966401)]], [[7573955795317583979849, (-106678419380653371483), 454072003322132301], [9916703576099992470828, (-102979138043099579530)], [10824215502659819079445]], [[(-370439732336227719576), 4207264271849593768, 637989235432788, (-189987266954189)], [(-448765624589882014068), 3006177563635846222, 74109938305802], [(-458616179680462029639), 3250638864080198852], [(-455811255621168415663)]], [[18756338915004467101, (-192694848446666069), (-18485566390009), 1576759495100, 77743791713], [21887571463644718261, (-114301755113643434), 7483120808229, (-6242802526314)], [20623868700105662998, (-92200567156933089), (-1341135133351)], [19105685375984495775, (-103502108077341246)], [18086210372529020483]]], r := 99025070408494684839, ok := true }, r3 := { p := [[[84169583815508934023923111]], [[(-8856748099455248809274072), 90349214226261577217481], [(-5435950542699441453879098)]], [[699132344719137663908658, (-8915162180081772800622), 1340818127324899206], [572102779657093863514187, (-2923688318461538311877)], [263121718366041493977388]], [[(-49058935009802263156371), 688283526065709698159, 43771679769175600, (-1303022380380579)], [(-45163303522288239621745), 288311495236926737965, (-2795839322264037)], [(-27693723772745878493203), 94417703951746697838], [(-11319042868792351321684)]], [[3227443115807817303960, (-47760200756571008001), (-2980849880052542), (-5141773029101), 1020124400509], [3169259328066890286906, (-22252041526669106340), 260661300972840, (-41291101744327)], [2186259577474041936779, (-9308584155062823256), 27434164925757], [1191371920832454983441, (-3047662178101588987)], [456460974617691214556]]], r := 45099279398316690973607, ok := true }, eta := { p := [[[(-3820771427441817120095984)]], [[168948690874636741468429, 0], [232431399239441541452694]], [[(-7743962621192504345558), 0, 0], [(-10017550544453525952940), 0], [(-10883094708302725425153)]], [[379324997456219813740, 0, 0, 0], [454026742354885462535, 0, 0], [461824882442585590985, 0], [457697579902653224135]], [[(-19222020959943153744), 0, 0, 0, 0], [(-22162598154848141383), 0, 0, 0], [(-20791219124407067924), 0, 0], [(-19208360447304622264), 0], [(-18146770178615978283)]]], r := 10026683470971369424, 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 54043195528445952 72057594037927936 9223372036854775808 13835058055282163712 2305843009213693952 2882303761517117440 :=
  (RegionPosI.split_b 63050394783186944 (RegionPosI.split_s 2594073385365405696 (RegionPosI.split_b 58546795155816448 (RegionPosI.of_check c0 q0 ok_0 54043195528445952 58546795155816448 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 58546795155816448 63050394783186944 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 (by decide +kernel))) (RegionPosI.split_b 58546795155816448 (RegionPosI.of_check c2 q2 ok_2 54043195528445952 58546795155816448 9223372036854775808 13835058055282163712 2594073385365405696 2882303761517117440 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 58546795155816448 63050394783186944 9223372036854775808 13835058055282163712 2594073385365405696 2882303761517117440 (by decide +kernel)))) (RegionPosI.split_s 2594073385365405696 (RegionPosI.split_b 67553994410557440 (RegionPosI.of_check c4 q4 ok_4 63050394783186944 67553994410557440 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 67553994410557440 72057594037927936 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 (by decide +kernel))) (RegionPosI.split_b 67553994410557440 (RegionPosI.of_check c6 q6 ok_6 63050394783186944 67553994410557440 9223372036854775808 13835058055282163712 2594073385365405696 2882303761517117440 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 67553994410557440 72057594037927936 9223372036854775808 13835058055282163712 2594073385365405696 2882303761517117440 (by decide +kernel)))))

end CKLaneC.RSC2.S06_0012