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

import Definitions.Def_CK_CKLaneC_RSC2_S04_0119_part00

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

namespace CKLaneC.RSC2.S04_0119
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def q3 : Cert := { V0 := [[[299616021866163260]], [[(-28426630713361409), 99834000210420828], [1184896738481706]], [[528809096311217, (-9464726331291979), (-18995010949475)], [(-110412904079789), 394514688485346], [(-14418520158535)]], [[(-11566457706265), 175042339250914, 5404574683694, (-2105821171105)], [1936203308618, (-36676742067034), (-225276888429)], [1351731647365, (-4802469521681)], [278280690055]], [[279335957831, (-3780477224602), (-612837047931), 598262467369, 1182566157], [(-47295119953), 631046430127, 63699954715, (-24937153247)], [(-24188528131), 449523191518, 1851213848], [(-26128536476), 92695376077], [(-6295408142)]]], r0 := 7470200225312, V1 := [[[798048902657083580]], [[(-75540830471954418), 0], [3148740508538241]], [[1380343356491509, 0, 0], [(-291334065898315), 0], [(-38359009112701)]], [[(-29033244947217), 0, 0, 0], [4815994771338, 0, 0], [3578929514038, 0], [740499301518]], [[670872783727, 0, 0, 0, 0], [(-105314592295), 0, 0, 0], [(-61596134593), 0, 0], [(-69226064790), 0], [(-16754080333)]]], r1 := 3007654114540, V2 := [[[18419050167108558265]], [[(-566871850906438), 1515523652378], [(-893034772081463)]], [[1198619060098, (-85066118433), (-78569413)], [(-18368493853112), 98591094441], [3500068607]], [[(-26123819782), (-2484500782), 10437530, 3990], [44079040191, (-5525699527), (-7674601)], [(-1514539956), 1620321107], [(-89682814)]], [[752384520, 6043654, (-208092), (-836), 0], [(-942649625), (-162523542), 1018994, 520], [114947148, (-90529211), (-251363)], [15049538, 425502], [1251075]]], r2 := 93710127494, V3 := [[[18426009187844223344]], [[(-1090450106078433), 2259308353000], [(-669237383468618)]], [[46107522287, (-53202385976), (-233588649)], [(-35167168122310), 146976740268], [(-12060570176)]], [[25722009, (-9224231704), 23351056, 23672], [3001342681, (-3452173417), (-22812221)], [280479572, 2415845089], [(-3045439)]], [[(-389352), (-4780115), 544825, (-4178), (-2)], [1845463, (-600536064), 2278739, 3082], [49391346, (-56467904), (-746965)], [45060, 650560], [16012]]], r3 := 737433595584, Vm := [[[18419057960061240416]], [[(-567329948840816), 0], [(-892526895680803)]], [[1187430011630, 0, 0], [(-18398389567848), 0], [11879912678]], [[(-26094507585), 0, 0, 0], [43351308538, 0, 0], [(-2009342371), 0], [(-87040964)]], [[751881957, 0, 0, 0, 0], [(-940585084), 0, 0, 0], [102993303, 0, 0], [14871120, 0], [1237020]]], rm := 14411057363 }
noncomputable def w3 : Wit := { Z0 := { p := [[[299673051679791180]], [[(-28442865680004068), 99891017226597060], [1185573454594082]], [[530652033247992, (-9480955226668023), 0], [(-110604422467214), 395191151531360], [(-14424077571746)]], [[(-11679202731859), 176884011082664, 0, 0], [1957772552067, (-36868140822405), 0], [1353313455560, (-4808025857249)], [278377998918]], [[284012039555, (-3893067577287), 0, 0, 0], [(-48603714433), 652590850689, 0, 0], [(-24368039577), 451104485186, 0], [(-26156246657), 92792666306], [(-6297478605)]]], r := 1715723557623, ok := true }, Z1 := { p := [[[799128137812776480]], [[(-75847641813344180), 0], [3161529212250886]], [[1415072088661313, 0, 0], [(-294945126579237), 0], [(-38464206857989)]], [[(-31144540618291), 0, 0, 0], [5220726805513, 0, 0], [3608835881494, 0], [742341330448]], [[757365438813, 0, 0, 0, 0], [(-129609905154), 0, 0, 0], [(-64981438871), 0, 0], [(-69749991085), 0], [(-16793276280)]]], r := 749076850682, ok := true }, Z2 := { p := [[[2075637429899693096716]], [[(-37363590951097124007), 99891017226597060], [(-58861603157404241757)]], [[803541909522802931, (-9480955226668023), 0], [1072135724264999797, 395191151531360], [1798391492666014138]], [[(-19124031740205280), 176884011082664, 0, 0], [(-22730677334912792), (-36868140822405), 0], [(-32890836100338477), (-4808025857249)], [(-56078844973642388)]], [[496982971536942, (-3893067577287), 0, 0, 0], [528747209909823, 652590850689, 0, 0], [694192834619198, 451104485186, 0], [1028065176400133, 92792666306], [1765267611002377]]], r := 1007931552427321, ok := true }, Z3 := { p := [[[2678674455997274421510]], [[(-124420650522062002708), 257787691012464150], [(-76360165532286101887)]], [[6213936732987870059, (-31797971963510722), 0], [3608265988192738240, 980414484892569], [2337179881744073251]], [[(-316485293537155253), 1518371950697366, 0, 0], [(-181262746061926876), (-114835430211191), 0], [(-111088696681856767), (-12079995098272)], [(-72955874447128439)]], [[16266485656212583, (-76424720889117), 0, 0, 0], [9263604152556687, 4900234397212, 0, 0], [5592575802490486, 1438349861385, 0], [3479573237524355, 233906075409], [2298198677469002]]], r := 13514227513341500, ok := true }, iE := { p := [[[2079271926141860820517]], [[(-37405923453279159364), 0], [(-58847224279352369936)]], [[804533507167422988, 0, 0], [1071991556641728145, 0], [1798216554494438865]], [[(-19148583377604386), 0, 0, 0], [(-22726530917479168), 0, 0], [(-32888989164004144), 0], [(-56075468748168331)]], [[497640540109166, 0, 0, 0, 0], [528627287167016, 0, 0, 0], [694143467097406, 0, 0], [1028029071419373, 0], [1765191233890066]]], r := 1007837083884442, 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 := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[163654576701923061]], [[2944131785711072, 0], [4631725874061304]], [[(-10358251883527), 0, 0], [82274781101195, 0], [(-10447001885472)]], [[181621583098, 0, 0, 0], [(-334324952596), 0, 0], [(-204908841914), 0], [112243085087]], [[(-4779516855), 0, 0, 0, 0], [5858757042, 0, 0, 0], [(-6061310), 0, 0], [2200844217, 0], [(-1810373571)]]], r := 6509775300, 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 := [[[(-23702431611594767549576)]], [[1246795270367261804614, 0], [764164843128321751799]], [[(-65620824443336990168), 0, 0], [(-40219227692888514088), 0], [(-24650486601503281680)]], [[3453727601667401876, 0, 0, 0], [2116800787366705624, 0, 0], [1297394030966690640, 0], [795176987004020087]], [[(-181775136929880311), 0, 0, 0, 0], [(-111410567795765358), 0, 0, 0], [(-68283896403096056), 0, 0], [(-41851420368648089), 0], [(-25650870548517190)]]], r := 24777645147330799, 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 := [[[(-47404863223189535099152)]], [[2493590540734523609228, 0], [1528329686256643503599]], [[(-131241648886673980336), 0, 0], [(-80438455385777028175), 0], [(-49300973203006563360)]], [[6907455203334803752, 0, 0, 0], [4233601574733411249, 0, 0], [2594788061933381280, 0], [1590353974008040175]], [[(-363550273859760621), 0, 0, 0, 0], [(-222821135591530716), 0, 0, 0], [(-136567792806192111), 0, 0], [(-83702840737296178), 0], [(-51301741097034379)]]], r := 49555290294661591, ok := true }, term0 := { p := [[[42283934947285287521079409]], [[(-4447193123404463130876839), 0], [(-2724411996646227328174967)]], [[350995762934097823078694, 0, 0], [286659552752480031977972, 0], [131768652962212504974742]], [[(-24627827881801349113430), 0, 0, 0], [(-22627842114345839308176), 0, 0], [(-13866492340237910463662), 0], [(-5666227352472634610975)]], [[1620115502976335280555, 0, 0, 0, 0], [1587807334299048408795, 0, 0, 0], [1094620653648252397809, 0, 0], [596319430209693489376, 0], [228446870854430973144]]], r := 390478692124826876810, ok := true }, r0 := { p := [[[2585361352815668356674]], [[(-149479605384440907625), 1722519740693419243577], [(-73458241497416029716)]], [[6709973043209431473, (-99392761261247352019), 286384103323520954504], [4257810706659246316, (-48950521860007008425)], [2247525698708049188]], [[(-276979322859026320), 4446030824128229084, (-16392128675047049046), (-233856107797831550)], [(-187737204808113398), 2833176928524245246, (-8144000226922519971)], [(-130377626251017318), 1497755160389263376], [(-70138737976308176)]], [[11252870169560346, (-182855666541799993), 722855978081441890, 57638781301413920, (-19355955639446579)], [7560158171638381, (-124594336695534954), 468623098550200962, 4802689292005811], [5714986836155169, (-86770753668877032), 249229143031067968], [4070640780882869, (-46741755623016998)], [2209028178748872]]], r := 170523756918589001, ok := true }, r1 := { p := [[[18316337819935234376959]], [[(-1046121232780509499613), 0], [(-520962751210111850011)]], [[45960827598466059532, 0, 0], [29929714805108537855, 0], [15943691278275473849]], [[(-1855312736036604738), 0, 0, 0], [(-1298577254002745394), 0, 0], [(-917544391228102259), 0], [(-497632470843710426)]], [[74045445714416945, 0, 0, 0, 0], [51384695114205927, 0, 0, 0], [39635435946671076, 0, 0], [28666370629707022, 0], [15674622715107327]]], r := 57950006755363971, ok := true }, r2 := { p := [[[15382292083579711743996848]], [[(-855611199337544012942067), 5254626658300679336144], [(-976849119684102144774676)]], [[39942588609259962466018, (-208747436767053013589), 462152505329666475], [53565231971449740852232, (-168639716755081693039)], [46826694368976713595716]], [[(-1834415806903682758887), 8138060122765592621, 448896003336073, (-22605174210618)], [(-2467222738523214642033), 6503112630999090295, 175497153872098], [(-2545471888216394087109), 5429257529603266737], [(-2000966298225741053069)]], [[86036632289534993470, (-329940530568816185), (-10373716475185), 1714245218060, (-1796400753)], [112088883096323010666, (-245906302658026635), 3650967701883, (-749950554151)], [116275570222289684296, (-206994430576891375), (-1983446634523)], [108101236865774689953, (-174921002804434290)], [80286105966375929245]]], r := 821450433779026295999, ok := true }, r3 := { p := [[[84284208638277936648028145]], [[(-8870049145983569789246188), 31277863838658880878817], [(-5439657139997004090288405)]], [[700215524483469319028714, (-2688836953747379511946), 1822214294315852567], [572532832285346977646204, (-1012901193558530764434)], [263241380932899335977807]], [[(-49136123354803829454974), 196330171313105212762, 5475501929520315, (-179000897242457)], [(-45198319016921837620272), 86976637496396040378, 510668642947973], [(-27707607770528545306284), 32718189316443599144], [(-11322904755433296218729)]], [[3232568182433235041546, (-13218183026763323337), (-273772008061022), 13256030580648, (-37591246646)], [3171754219908314089693, (-6348148289194049981), 38052943141927, (-5848650923364)], [2187389969132982567926, (-2808354540636995710), (-6188324980908)], [1191820003537620999082, (-1056221606383836593)], [456585591946391410178]]], r := 43906408421548138352260, ok := true }, eta := { p := [[[(-15442803556068472265897866)]], [[859105011219730106657093, 0], [978774580797681356927691]], [[(-40125917461777493066383), 0, 0], [(-53675460796442371977464), 0], [(-46888507601007412523522)]], [[1843868741925378241091, 0, 0, 0], [2472971242744094269976, 0, 0], [2548997953110076914854, 0], [2002954542698266629896]], [[(-86524496012080138172), 0, 0, 0, 0], [(-112384295034518894477), 0, 0, 0], [(-116459031911853664303), 0, 0], [(-108214410570613660784), 0], [(-80350113711093009610)]]], r := 92789273995078376297, 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 15762598695796736 18014398509481984 4611686018427387904 9223372036854775808 9223372036854775808 11529215046068469760 :=
  (RegionPosI.split_s 10376293541461622784 (RegionPosI.split_b 16888498602639360 (RegionPosI.of_check c0 q0 ok_0 15762598695796736 16888498602639360 4611686018427387904 9223372036854775808 9223372036854775808 10376293541461622784 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 16888498602639360 18014398509481984 4611686018427387904 9223372036854775808 9223372036854775808 10376293541461622784 (by decide +kernel))) (RegionPosI.split_b 16888498602639360 (RegionPosI.of_check c2 q2 ok_2 15762598695796736 16888498602639360 4611686018427387904 9223372036854775808 10376293541461622784 11529215046068469760 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 16888498602639360 18014398509481984 4611686018427387904 9223372036854775808 10376293541461622784 11529215046068469760 (by decide +kernel))))

end CKLaneC.RSC2.S04_0119