Prove2Me

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

Definition
CK_CKLaneC_RSC2_S06_0081

by tianyipeng · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneC.RSC2.S06_0081 of the machine-checked proof of the general Courtade–Kumar theorem (the most informative Boolean function conjecture), so that the complete proof can be verified on this platform.

It is the original source with only two mechanical changes. Imports of project modules are redirected to their transplanted bundles Definitions.Def_CK_*. Declarations that already exist in earlier platform definition bundles of this mission are removed, and those bundles are imported instead, so every constant keeps a single platform identity.

The module contains both definitions and the lemmas proved alongside them in the source. They are kept together so the transplant stays faithful and every proof is re-checked by the server.

Source: Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff, A Proof of the Most Informative Boolean Function Conjecture, arXiv:2609.24931 (2026). Lean development: https://github.com/dpwoodru/general-courtade-kumar-lean (Apache-2.0), module CKLaneC.RSC2.S06_0081 from release v1.0 (sources_v3.tar.zst).

Definition code
import Definitions.Def_CK_CKLaneC_RSC2_S06_0081_part00

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

namespace CKLaneC.RSC2.S06_0081
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def q4 : Cert := { V0 := [[[293719447472282202]], [[(-31621444682790519), 97870675384459845], [2893738781251880]], [[548538842651361, (-10528917483145785), (-17895831678630)], [(-305247252180566), 963521342912001], [(-67800921856673)]], [[(-11519630185056), 181400909114619, 5777882884493, (-1984138026518)], [4805163414324, (-101409631629146), (-528745095114)], [7216576879132, (-22585936472112)], [2663700567484]], [[267415915558, (-3747837042322), (-721719083758), 639679594267, 1070768027], [(-113876602157), 1559724398772, 169522344291, (-58538301084)], [(-118629907109), 2400869301823, 7183988299], [(-283963086568), 887380337196], [(-123381615017)]]], r0 := 57322792348984, V1 := [[[782378301208048623]], [[(-84042103212724764), 0], [7690853335900575]], [[1427654528182707, 0, 0], [(-805740417677305), 0], [(-180451491276360)]], [[(-28497812719320), 0, 0, 0], [11797682661043, 0, 0], [19130560986850, 0], [7090510321665]], [[625130517136, 0, 0, 0, 0], [(-240597953750), 0, 0, 0], [(-302095819260), 0, 0], [(-753129726273), 0], [(-328465598257)]]], r1 := 34328963068714, V2 := [[[18335171952586248010]], [[(-2186787093298495), 20584310638639], [(-7440476835829139)]], [[5120536613619, (-1459543420663), (-3564467385)], [(-146208841048264), 2779721527946], [(-269236598153)]], [[(-96782520752), (-38299017548), 575897160, 602043], [407103844697, (-196942008002), (-723110089)], [(-6817433365), 95427274382], [(-3377482176)]], [[2530563389, 95990544, (-16191361), (-151895), (-100)], [(-7373825327), (-5197947564), 116798691, 162819], [3191806244, (-6753732408), (-49357130)], [611949208, 85701127], [88839087]]], r2 := 4498887178607, V3 := [[[18357916614718900027]], [[(-4215227635184773), 32624501574528], [(-5932954569573375)]], [[714522095465, (-1386864202617), (-11266200903)], [(-280545664916541), 4407415781027], [(-753741985994)]], [[448516048, (-142939750826), 1496452069, 3797866], [96566068370, (-187374577492), (-2285935790)], [31774515394, 151526374103], [(-650470927)]], [[(-6679036), (-67332383), 6851599, (-848088), (-1263)], [64200637, (-19320517108), 303587248, 1027245], [3319579156, (-6458000519), (-156118242)], [27042418, 148330219], [6029551]]], r3 := 14193933349710, Vm := [[[18335277758182621813]], [[(-2194601852541609), 0], [(-7426160272298040)]], [[4951649306297, 0, 0], [(-147268384703679), 0], [224371814278]], [[(-96267261439), 0, 0, 0], [384370647807, 0, 0], [(-43528170180), 0], [(-2876663587)]], [[2522675938, 0, 0, 0, 0], [(-7296442875), 0, 0, 0], [2418054492, 0, 0], [568300987, 0], [83999905]]], rm := 761770605901 }
noncomputable def w4 : Wit := { Z0 := { p := [[[293773175511767631]], [[(-31638800155550597), 97924391837255877], [2895327013702884]], [[550709077331111, (-10546266718516866), 0], [(-305756889885778), 965109004567628], [(-67822481265452)]], [[(-11657979967033), 183569692443703, 0, 0], [4868264797926, (-101918963295260), 0], [7223563130989, (-22607493755151)], [2664480509183]], [[272991188566, (-3885993322345), 0, 0, 0], [(-117846083855), 1622754932642, 0, 0], [(-119507426163), 2407854376996, 0], [(-284215626762), 888160169727], [(-123415540404)]]], r := 14109190186366, ok := true }, Z1 := { p := [[[783395134698047018]], [[(-84370133748134925), 0], [7720872036541025]], [[1468557539549629, 0, 0], [(-815351706362073), 0], [(-180859950041204)]], [[(-31087946578754), 0, 0, 0], [12982039461137, 0, 0], [19262835015971, 0], [7105281357823]], [[727976502842, 0, 0, 0, 0], [(-314256223612), 0, 0, 0], [(-318686469766), 0, 0], [(-757908338030), 0], [(-329108107743)]]], r := 8599443411143, ok := true }, Z2 := { p := [[[618045941453283244144]], [[(-10403058909675303164), 97924391837255877], [(-35396092777578632745)]], [[215736508732392225, (-10546266718516866), 0], [606758577990734306, 965109004567628], [2214251471581861835]], [[(-4963948346202766), 183569692443703, 0, 0], [(-12342813230231030), (-101918963295260), 0], [(-38195187821880922), (-22607493755151)], [(-141945546609567768)]], [[124116162366322, (-3885993322345), 0, 0, 0], [275923936175178, 1622754932642, 0, 0], [772952468762270, 2407854376996, 0], [2457151310606020, 888160169727], [9200813977606874]]], r := 3036897412657176, ok := true }, Z3 := { p := [[[752014813699800209757]], [[(-30774944658305725062), 238188140085320341], [(-43315892839286503503)]], [[1378335202154972387, (-31380342202148044), 0], [1817107709949704316, 2261584448691230], [2714741965814372244]], [[(-63187677427087675), 1319985800425496, 0, 0], [(-82032738912649324), (-282486799517023), 0], [(-114808555343998843), (-53821749290656)], [(-174215127378776890)]], [[2927855312239944, (-59587316552435), 0, 0, 0], [3777824933173122, 10235511779768, 0, 0], [5197434069022124, 6873889750113, 0], [7401599369940243, 2120507150241], [11300802086076099]]], r := 15587330118830468, ok := true }, iE := { p := [[[622310103606923750073]], [[(-10447943130495058169), 0], [(-35354066667288824210)]], [[216773496160140267, 0, 0], [606404237434832697, 0], [2213267017990160285]], [[(-4988829645868559), 0, 0, 0], [(-12332158487781191), 0, 0], [(-38185998169734167), 0], [(-141906871271267799)]], [[124756918136766, 0, 0, 0, 0], [275624564889636, 0, 0, 0], [772709910844136, 0, 0], [2456784043066897, 0], [9199022582338592]]], r := 3038292409841297, ok := true }, iHu := { p := [[[756843536903348067588]], [[(-30907174538967106417), 0], [(-43270044354553944922)]], [[1384515740902886963, 0, 0], [1816165771930280335, 0], [2713650852169661682]], [[(-63473811558178750), 0, 0, 0], [(-81987909757293568), 0, 0], [(-114783073660208583), 0], [(-174172138915640182)]], [[2941172228868682, 0, 0, 0, 0], [3775802170044759, 0, 0, 0], [5196254231853920, 0, 0], [7400572253291260, 0], [11298807234431556]]], r := 15609965469136870, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[546805145776444889]], [[9180292965551643, 0], [31064553613623723]], [[(-36344716583991), 0, 0], [510254324601601, 0], [(-179922347909378)]], [[575510482325, 0, 0, 0], [(-2428818185436), 0, 0], [(-3400345459611), 0], [3985583382377]], [[(-13702710246), 0, 0, 0, 0], [38366919082, 0, 0, 0], [(-390076109), 0, 0], [75199161400, 0], [(-132854173303)]]], r := 186047955184, ok := true }, de := { p := [[[(-80218623972052311307)]], [[635169958946257284, 0], [889237942524760199]], [[(-15086661987843625), 0, 0], [102010363788337, 0], [(-29569857496173505)]], [[478944436665661, 0, 0, 0], [11702283296, 0, 0], [16383196614, 0], [1314223534210575]], [[(-17105158212622), 0, 0, 0, 0], [1342446, 0, 0, 0], [392895247, 0, 0], [2631195, 0], [(-65711175789611)]]], r := 22195653518524, ok := true }, dde := { p := [[[(-5550199790600255647236)]], [[263658528009418615444, 0], [369121939213186061478]], [[(-12555241040528317113), 0, 0], [(-17577439712851382710), 0], [(-24608272439435502795)]], [[597868612598629166, 0, 0, 0], [837016034177130776, 0, 0], [1171822447847983206, 0], [1640551472970636986]], [[(-28469933934228622), 0, 0, 0, 0], [(-39857907511957601), 0, 0, 0], [(-55801071302540498), 0, 0], [(-78121498723437243), 0], [(-109370098201734375)]]], r := 23969418598298302, ok := true }, nJu := { p := [[[(-160437247944104622613)]], [[1270339917892514569, 0], [1778475885049520398]], [[(-30173323975687249), 0, 0], [204020727576674, 0], [(-59139714992347010)]], [[957888873331323, 0, 0, 0], [23404566592, 0, 0], [32766393228, 0], [2628447068421151]], [[(-34210316425244), 0, 0, 0, 0], [2684893, 0, 0, 0], [785790495, 0, 0], [5262391, 0], [(-131422351579221)]]], r := 44391307037038, ok := true }, Jd1 := { p := [[[(-11100399581200511294471)]], [[527317056018837230889, 0], [738243878426372122957]], [[(-25110482081056634225), 0, 0], [(-35154879425702765420), 0], [(-49216544878871005590)]], [[1195737225197258332, 0, 0, 0], [1674032068354261553, 0, 0], [2343644895695966413, 0], [3281102945941273973]], [[(-56939867868457243), 0, 0, 0, 0], [(-79715815023915202), 0, 0, 0], [(-111602142605080996), 0, 0], [(-156242997446874486), 0], [(-218740196403468750)]]], r := 47938837196596596, ok := true }, term0 := { p := [[[2329011156592010672228902]], [[(-221013242296122371808208), 0], [(-308856067688151227366002)]], [[15767828069620152960406, 0, 0], [29362133413422018081300, 0], [30829946376640078353377]], [[(-1000534072215080263885), 0, 0, 0], [(-2096039668233349947918), 0, 0], [(-2932669901320445531129), 0], [(-2737965830281741914446)]], [[59534247086173963162, 0, 0, 0, 0], [133042025803321907002, 0, 0, 0], [209392719941826472474, 0, 0], [260524286006973082280, 0], [228040126817208093332]]], r := 92056227413079521187, ok := true }, r0 := { p := [[[712411692853036185835]], [[(-38403334255223888998), 474661697772613280934], [(-40711960074043644743)]], [[1651203817553554249, (-25527181253873650513), 78924117067327966753], [2213771284771431153, (-27130833932845889890)], [2552846235937868965]], [[(-65274679571213392), 1092692524134283715, (-4204561150577984603), (-61974481803249741)], [(-93036130860023049), 1473013444800174751, (-4514825957978340643)], [(-139156748996932204), 1701312107812846724], [(-163836349420231386)]], [[2521550643260203, (-42995627971185960), 176721116753211734, 16617280063187404, (-5130901240415674)], [3567979623721219, (-61715263876734702), 243613913781884420, 2325127093378449], [5811568004025411, (-92612653277163490), 283161883140957409], [8943609054167306, (-109189282221319170)], [10627632082753791]]], r := 158557271121112450, ok := true }, r1 := { p := [[[5047896155108885379773]], [[(-268233632886472550318), 0], [(-288825891290955704874)]], [[11220573468077408487, 0, 0], [15558266493725566429, 0], [18115486798236585961]], [[(-431132083421871123), 0, 0, 0], [(-641595254399454698), 0, 0], [(-979261517848702807), 0], [(-1162784311329475608)]], [[16270466819028248, 0, 0, 0, 0], [24094699760171669, 0, 0, 0], [40207442158695283, 0, 0], [62983727006293649, 0], [75434190981239633]]], r := 145859004265684690, ok := true }, r2 := { p := [[[964483322634350245712274]], [[(-51941742355642614305101), 1263514099410367144258], [(-126124492316500584905319)]], [[2313064224332059329896, (-48715500198712675367), 472864934872554084], [6681315627420050016617, (-83844792970029613633)], [12469117987486355802699]], [[(-99641927828800102448), 1822811022918851779, 617683664269067, (-76531778287079)], [(-293028441130648727152), 3111803255065248641, 634949610994703], [(-653934889748776668751), 5583303689751369332], [(-1099645166512902091062)]], [[4319766913110104858, (-69831680075940131), (-12037949441017), 6870500865398, 12205370572], [12467858453036684705, (-112282630328391051), 14919573197537, (-5269147855024)], [28412891750125936214, (-204341913206891771), (-10999533078159)], [57261733494831080733, (-371915151197602215)], [91092970928967183754]]], r := 621644716973911304168, ok := true }, r3 := { p := [[[4595860697852009092614251]], [[(-437271970142211354649224), 6822766778355236898688], [(-613560932824603016840448)]], [[31223633912570534726256, (-524060102904624067467), 1862768801853074032], [58406478511243489775504, (-457610739332850583700)], [61382795265552373449023]], [[(-1982133575052746391152), 34425446918404969402, 6454398441277735, (-604378421369989)], [(-4171234218031807987436), 35098241563022490378, 1918254592924411], [(-5844137267158759822120), 30577037906509311236], [(-5457446005298685715519)]], [[117972716930410993971, (-2090170689881994639), (-252352584269989), 53268405475099, 193738678609], [264819393932651793608, (-2303657516252220246), 131021501674108, (-41403370793532)], [417394809346713844865, (-2343260589816845943), (-36575614178761)], [519634428809015889114, (-2040961764270756997)], [454847323795976321601]]], r := 12889494959670375823570, ok := true }, eta := { p := [[[(-978789013496991370827770)]], [[52705646178070034549502, 0], [127058751558931979259622]], [[(-2349903152547962644279), 0, 0], [(-6730754585771082615208), 0], [(-12531035127213796979285)]], [[101374073719559345024, 0, 0, 0], [295391503784149717936, 0, 0], [657196276234644440455, 0], [1103758515383799812525]], [[(-4400892454050357884), 0, 0, 0, 0], [(-12578371290567648730), 0, 0, 0], [(-28568293297506053989), 0, 0], [(-57477810812930953783), 0], [(-91366526384540081373)]]], r := 74490599082359065159, ok := true } }
theorem sB_4 : stageB c4 w4 = true := by decide +kernel
theorem s0_4 : stageC0 w4 q4 = true := by decide +kernel
theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel
theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

noncomputable def c5 : Cell := { bc := 67553994410557440, bh := 4503599627370496, tc := 6917529027641081856, th := 2305843009213693952, sc := 13258597302978740224, sh := 576460752303423488 }
noncomputable def q5 : Cert := { V0 := [[[232582630292763375]], [[(-29557474308047442), 77509763957904464], [2301600267741701]], [[485340034080995, (-9845713268099238), (-8887332351296)], [(-287301681401270), 766672282543283], [(-53822050701452)]], [[(-9623526254717), 160807405909516, 3387556406055, (-986146118305)], [4188937704450, (-95567205120298), (-263784403564)], [6771923897259, (-17933563560484)], [2113794813026]], [[209632307202, (-3140878512145), (-485889430466), 375546861885, 333586821], [(-92525721642), 1367885567201, 99935699652, (-29243322650)], [(-104172722264), 2254585521199, 3559575703], [(-266321734154), 704340566917], [(-97888627084)]]], r0 := 49308573729191, V1 := [[[619786276019052840]], [[(-78654584515136060), 0], [6124725370390021]], [[1270557618015452, 0, 0], [(-761265215499081), 0], [(-143351520096935)]], [[(-24039803719362), 0, 0, 0], [10480142855483, 0, 0], [17991977872299, 0], [5630491761845]], [[495894743329, 0, 0, 0, 0], [(-200314314770), 0, 0, 0], [(-268218512975), 0, 0], [(-707787673464), 0], [(-260762597370)]]], r1 := 28505330039194, V2 := [[[18330818124496557983]], [[(-2167390985782051), 17512764943931], [(-7731322188795515)]], [[4595049977993, (-1611648230091), (-2482413791)], [(-144663184233375), 2365154872640], [(-270408750679)]], [[(-79218311366), (-37767579584), 503681840, 343168], [367057155455, (-217572171909), (-503634418)], [5500254671, 81203886932], [(-2279836302)]], [[1899780618, 81776199, (-19903529), (-107701), (-46)], [(-6038844043), (-5119180843), 102172630, 92812], [2974065049, (-7467455559), (-34378700)], [487772377, 72611368], [58612062]]], r2 := 4429672368218, V3 := [[[18349489021022493392]], [[(-4212364367654909), 29278496431586], [(-6493659137286074)]], [[717063419751, (-1959389761555), (-8281825979)], [(-280158661440714), 3955321403571], [(-676896693424)]], [[400216578, (-143313180484), 1469920247, 2286097], [96928249361, (-264749821140), (-1680449615)], [45079413577, 135951567344], [(-584374526)]], [[(-5458116), (-57474148), (-20151696), (-658866), (-622)], [56772949, (-19365579114), 298242384, 618358], [3332540151, (-9117286231), (-114760620)], [39027023, 130289114], [5574903]]], r3 := 12810839740863, Vm := [[[18330907629026336732]], [[(-2175875350553514), 0], [(-7719215044223152)]], [[4429077730621, 0, 0], [(-145812767553499), 0], [146708922802]], [[(-78759900427), 0, 0, 0], [344762111056, 0, 0], [(-34267231875), 0], [(-1867808206)]], [[1893383570, 0, 0, 0, 0], [(-5969879266), 0, 0, 0], [2219094153, 0, 0], [442728141, 0], [54562276]]], rm := 756420743004 }
noncomputable def w5 : Wit := { Z0 := { p := [[[232609304912954021]], [[(-29567644998082260), 77536434970984673], [2302392245522458]], [[486799872635093, (-9855881666027420), 0], [(-287601883943044), 767464081840819], [(-53832731673045)]], [[(-9724112508355), 162266624211697, 0, 0], [4231623864996, (-95867294647682), 0], [6776008191060, (-17944243891015)], [2114181419655]], [[213600144479, (-3241370836119), 0, 0, 0], [(-95422822148), 1410541288332, 0, 0], [(-104761559284), 2258669397020, 0], [(-266469458717), 704727139885], [(-97905440320)]]], r := 12178010653332, ok := true }, Z1 := { p := [[[620291479767877391]], [[(-78847053328219359), 0], [6139712654726555]], [[1298132993693583, 0, 0], [(-766938357181449), 0], [(-143553951128120)]], [[(-25930966688947), 0, 0, 0], [11284330306656, 0, 0], [18069355176160, 0], [5637817119080]], [[569600385279, 0, 0, 0, 0], [(-254460859061), 0, 0, 0], [(-279364158089), 0, 0], [(-710585223244), 0], [(-261081174186)]]], r := 7132794702240, ok := true }, Z2 := { p := [[[598064942753491199667]], [[(-9595958762869218938), 77536434970984673], [(-34229841035980898536)]], [[188685416964430831, (-9855881666027420), 0], [560497805297060765, 767464081840819], [2140822149156870283]], [[(-4090840271435854), 162266624211697, 0, 0], [(-10834666825904874), (-95867294647682), 0], [(-35296545243565538), (-17944243891015)], [(-137221209693594651)]], [[95732881223085, (-3241370836119), 0, 0, 0], [228766476063393, 1410541288332, 0, 0], [679264482705240, 2258669397020, 0], [2271169913735116, 704727139885], [8893822841551539]]], r := 2769243004321444, ok := true }, Z3 := { p := [[[695515615407531456169]], [[(-25935978876775441598), 180270840486695375], [(-39982155273854719749)]], [[1059912355348893851, (-26736870463750339), 0], [1529281404116129975, 1734331182058755], [2504159833805934482]], [[(-44348257790817344), 1019336918387459, 0, 0], [(-63005244491039098), (-246246047438641), 0], [(-96576312614989588), (-41049313453508)], [(-160641002048538062)]], [[1875741944251067, (-41930890233265), 0, 0, 0], [2648494232804594, 8010700673065, 0, 0], [3990140274753408, 5937286778351, 0], [6224406634494706, 1615624629060], [10417593942053278]]], r := 11803673727816654, ok := true }, iE := { p := [[[602243295082483151541]], [[(-9636974426660151459), 0], [(-34188483249348365491)]], [[189587195181504019, 0, 0], [560182754294164117, 0], [2139855153791632253]], [[(-4111227689859084), 0, 0, 0], [(-10825615755015833), 0, 0], [(-35288253403494022), 0], [(-137183232731056402)]], [[96224047048197, 0, 0, 0, 0], [228528254416001, 0, 0, 0], [679056860058401, 0, 0], [2270837904268311, 0], [8892064169753208]]], r := 2770834729644915, ok := true }, iHu := { p := [[[700102506793248482954]], [[(-26046538813333409892), 0], [(-39938026180444558071)]], [[1064652089389061513, 0, 0], [1528497153237562118, 0], [2503115356830284119]], [[(-44548749909493726), 0, 0, 0], [(-62970637665122638), 0, 0], [(-96554977753186081), 0], [(-160599893377420862)]], [[1884263503755525, 0, 0, 0, 0], [2647066174472678, 0, 0, 0], [3989230945785896, 0, 0], [6223546694650867, 0], [10415687568484390]]], r := 11821102490361687, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[565024749464970700]], [[9041410847551599, 0], [32075640094763874]], [[(-33191921775859), 0, 0], [500972163057473, 0], [(-186724599491108)]], [[479772831709, 0, 0, 0], [(-2218634544256), 0, 0], [(-3401906301193), 0], [4135981446551]], [[(-10429917001), 0, 0, 0, 0], [31984408734, 0, 0, 0], [(-390344722), 0, 0], [75198898756, 0], [(-137867538478)]]], r := 186614904402, ok := true }, de := { p := [[[(-79005053507352196838)]], [[580070876134051360, 0], [889442010072212085]], [[(-12576956919532921), 0, 0], [102057189035802, 0], [(-29569823157479622)]], [[364552021654941, 0, 0, 0], [11710341671, 0, 0], [17955857229, 0], [1314223539992789]], [[(-11887565704453), 0, 0, 0, 0], [1343679, 0, 0, 0], [393435185, 0, 0], [3159139, 0], [(-65711175788637)]]], r := 20935997470945, ok := true }, dde := { p := [[[(-5068736658442825317454)]], [[219798252980935860614, 0], [337023987904101652519]], [[(-9556512516471272164), 0, 0], [(-14653421518449512314), 0], [(-22468422760948014174)]], [[415500536537069316, 0, 0, 0], [637100799207679515, 0, 0], [976887892118441710, 0], [1497894823124893461]], [[(-18065240719880968), 0, 0, 0, 0], [(-27700035774526438), 0, 0, 0], [(-42473388974488766), 0, 0], [(-65125861887665081), 0], [(-99859654879849142)]]], r := 19126355409093952, ok := true }, nJu := { p := [[[(-158010107014704393675)]], [[1160141752268102720, 0], [1778884020144424171]], [[(-25153913839065841), 0, 0], [204114378071604, 0], [(-59139646314959244)]], [[729104043309883, 0, 0, 0], [23420683342, 0, 0], [35911714458, 0], [2628447079985578]], [[(-23775131408905), 0, 0, 0, 0], [2687359, 0, 0, 0], [786870370, 0, 0], [6318279, 0], [(-131422351577273)]]], r := 41871994941881, ok := true }, Jd1 := { p := [[[(-10137473316885650634907)]], [[439596505961871721229, 0], [674047975808203305039]], [[(-19113025032942544328), 0, 0], [(-29306843036899024627), 0], [(-44936845521896028347)]], [[831001073074138633, 0, 0, 0], [1274201598415359030, 0, 0], [1953775784236883420, 0], [2995789646249786922]], [[(-36130481439761936), 0, 0, 0, 0], [(-55400071549052876), 0, 0, 0], [(-84946777948977531), 0, 0], [(-130251723775330161), 0], [(-199719309759698284)]]], r := 38252710818187896, ok := true }, term0 := { p := [[[1942906325571510663276056]], [[(-168283163491799237322011), 0], [(-257565281081066167070751)]], [[10960654855639372064801, 0, 0], [22353022871103849039277, 0], [25707196587595476741617]], [[(-634984780857866652971), 0, 0, 0], [(-1456850141093764158895), 0, 0], [(-2232477734638795197058), 0], [(-2282891570207454801668)]], [[34496493507399219842, 0, 0, 0, 0], [84427380619668273119, 0, 0, 0], [145532663940966783901, 0, 0], [198316932867308957976, 0], [190131335649834069684]]], r := 65746554952140639639, ok := true }, r0 := { p := [[[641725081348606478301]], [[(-32508283258746749672), 427658709080387140479], [(-36630002903453067149)]], [[1313070767657516160, (-21624102409631225314), 71171153330578714546], [1880542356210864726, (-24414106198662924013)], [2296134335405613726]], [[(-48478229739563799), 869841613635268925, (-3571983471953282573), (-35070719407157910)], [(-74469255935594624), 1251886597283496265, (-4065087962764526468)], [(-118320887358425048), 1530426797422081928], [(-147332863175275272)]], [[1736911471544792, (-31969962255308780), 141286709450953640, 10661859249031248, (-2910619792495752)], [2674683928417128, (-49435635211884380), 207442655299857171, 1309409443241287], [4661011105149681, (-78779488970816843), 254851557696898833], [7608676591095696, (-98202246665871182)], [9555826304371065]]], r := 125149189139504195, ok := true }, r1 := { p := [[[4553103974957188940793]], [[(-228049794907287160111), 0], [(-260096156797911937889)]], [[8979728917826803164, 0, 0], [13255126067779897098, 0], [16306617905566750414]], [[(-322449494709299034), 0, 0, 0], [(-515897044058802418), 0, 0], [(-834816806625491328), 0], [(-1046420119893010743)]], [[11275096864955875, 0, 0, 0, 0], [18157135290478099, 0, 0, 0], [32380390787878696, 0, 0], [53713374921915419, 0], [67873704967443025]]], r := 110088989664246586, ok := true }, r2 := { p := [[[869118484897400687641904]], [[(-43760703626994527403409), 1172856759453448151593], [(-113842112912829404481576)]], [[1805473991945775232725, (-42181656988406427652), 474054973634242289], [5643370698374113759037, (-78039385193210605074)], [11266056436566408325010]], [[(-71522286300351118231), 1462366037729015506, 573673602256991, (-62755384770307)], [(-229422753032610072112), 2707963980712282977, 663984613922124], [(-553201344907809973784), 5201722736378424255], [(-994242059779158408165)]], [[2836512909289248905, (-51517657798022785), (-10056700579031), 6905290083884, 8207234433], [8976747200923181417, (-90702268525712558), 14142434346526, (-4324745253942)], [22287006613273823533, (-178158454686367131), (-11291612729658)], [48494085489676597243, (-346690823447715848)], [82405369760587051261]]], r := 524897283570098876970, ok := true }, r3 := { p := [[[3832047691231813921079126]], [[(-332863411241413128813195), 5897367441695791086017], [(-511540620495798341573904)]], [[21700809187116480126506, (-408047596944306892981), 1874762859499977071], [44458513860357086617597, (-395626793982597827363)], [51174742935234262017861]], [[(-1257796052433551492888), 24323212307563957134, 5582496785204569, (-497090078025210)], [(-2898968178393347779806), 27334448016862275437, 2168961807165470], [(-4448439967473537954552), 26438709561513639998], [(-4549795119244637476857)]], [[68351238132905988367, (-1343604914181358744), (-187881589501037), 53997333899698, 130215661769], [168041625859264315083, (-1627887497724821853), 120232786293683, (-34120173161651)], [290082490431100278521, (-1825018506639669917), (-39815543366565)], [395532315989295179179, (-1764842830609543394)], [379196302479311271411]]], r := 8670023417277557285849, ok := true }, eta := { p := [[[(-882031053332810870927392)]], [[44395715024294398291507, 0], [114686137888037476961459]], [[(-1833600477428745965175), 0, 0], [(-5684535789808626182564), 0], [(-11322019326347963434689)]], [[72733138138776894486, 0, 0, 0], [231229664169949705209, 0, 0], [555918485967067780755, 0], [997960854054391378966]], [[(-2888335533591605897), 0, 0, 0, 0], [(-9054086791558065984), 0, 0, 0], [(-22405894871131133697), 0, 0], [(-48674166672050455616), 0], [(-82652732189903442442)]]], r := 63761122164274657657, ok := true } }
theorem sB_5 : stageB c5 w5 = true := by decide +kernel
theorem s0_5 : stageC0 w5 q5 = true := by decide +kernel
theorem s1_5 : stageC1 w5 q5 = true := by decide +kernel
theorem s2_5 : stageC2 w5 q5 = true := by decide +kernel
theorem s3_5 : stageC3 w5 q5 = true := by decide +kernel
theorem sE_5 : stageE w5 q5 = true := by decide +kernel
theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

theorem region : RegionPosI 54043195528445952 72057594037927936 4611686018427387904 9223372036854775808 11529215046068469760 13835058055282163712 :=
  (RegionPosI.split_b 63050394783186944 (RegionPosI.split_s 12682136550675316736 (RegionPosI.split_b 58546795155816448 (RegionPosI.of_check c0 q0 ok_0 54043195528445952 58546795155816448 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 58546795155816448 63050394783186944 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel))) (RegionPosI.split_b 58546795155816448 (RegionPosI.of_check c2 q2 ok_2 54043195528445952 58546795155816448 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 58546795155816448 63050394783186944 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel)))) (RegionPosI.split_s 12682136550675316736 (RegionPosI.of_check c4 q4 ok_4 63050394783186944 72057594037927936 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 63050394783186944 72057594037927936 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel))))

end CKLaneC.RSC2.S06_0081
Source
arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneC.RSC2.S06_0081 (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneC/RSC2/S06_0081.lean)

View graph