Prove2Me

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

Definition
CK_CKLaneC_RSC2_S05_0060

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

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneC.RSC2.S05_0060 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.S05_0060 from release v1.0 (sources_v3.tar.zst).

Definition code
import Definitions.Def_CK_CKLaneC_RSC2_S05_0060_part00

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

namespace CKLaneC.RSC2.S05_0060
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def q4 : Cert := { V0 := [[[1476527710487321226]], [[(-49997947202416812), 208987693960420731], [5422833289600521]], [[630850126646143, (-6945323644191725), (-412224757321227)], [(-179719225602279), 753297572644180], [(-62305205537127)]], [[(-9885748482652), 80981480767325, 41501403330752, (-18564757187449)], [2289590225735, (-23522377497078), (-4501288635633)], [2085289279512, (-8733196139765)], [1130833651763]], [[190359641183, (-1131574789904), (-1897379342430), 1797240805723, 110997963334], [(-42094615271), 228007497489, 447171694629, (-194930748483)], [(-26770812460), 280886829594, 35556834671], [(-37925176029), 158790328388], [(-24046733938)]]], r0 := 6762804696500, V1 := [[[1685084728638373209]], [[(-56899991069402407), 0], [6171436689188962]], [[709859576869076, 0, 0], [(-202776712923270), 0], [(-71001242930779)]], [[(-10958454057848), 0, 0, 0], [2496799627825, 0, 0], [2362434629066, 0], [1289012274386]], [[208896371396, 0, 0, 0, 0], [(-44444872433), 0, 0, 0], [(-29633850265), 0, 0], [(-43001372360), 0], [(-27414587115)]]], r1 := 2013210962346, V2 := [[[18423157879618950664]], [[(-320222124290492), 2371501165341], [(-712721913749393)]], [[743388328581, (-19992074654), (-226093993)], [(-9822169282305), 144689702009], [37746310546]], [[(-15507255405), (-798359637), 6898406, 21121], [25346537110, (-1201244549), (-20719397)], [(-2250988496), 2225338063], [(-286738625)]], [[430693830, 3138120, 34963, (-1111), (-2)], [(-525996876), (-49384276), 630154, 2581], [53391248, (-17835131), (-636102)], [16462561, 429000], [3817513]]], r2 := 32939253010, V3 := [[[18435711579495846780]], [[(-580610389177825), 2193979083719], [(-334385385460202)]], [[2549587322, 68253593504, (-415304861)], [(-17596361127592), 133888648367], [(-2059020834)]], [[1774579, (-2550359076), (-3880441), 77159], [155437903, 4175442080, (-38041490)], [(-64595586), 2060187410], [(-397160)]], [[(-29930), (-1764459), 771914, (-967), (-14)], [120714, (-155508620), (-358788), 9422], [2386175, 64606766, (-1167009)], [(-17445), 409268], [2105]]], r3 := 354934969660, Vm := [[[18423160990624785704]], [[(-320275472506172), 0], [(-712529053784257)]], [[743045534973, 0, 0], [(-9825531586933), 0], [40818173163]], [[(-15509958207), 0, 0, 0], [25326095092, 0, 0], [(-2306368348), 0], [(-284757832)]], [[430856491, 0, 0, 0, 0], [(-526153090), 0, 0, 0], [53090177, 0, 0], [16405003, 0], [3807706]]], rm := 5673951349 }
noncomputable def w4 : Wit := { Z0 := { p := [[[1483390623876048872]], [[(-50697780803414122), 211912946268006981], [5498738024915051]], [[663604289979429, (-7242540114773446), 0], [(-187424447220340), 785534003559293], [(-62895869393992)]], [[(-10908186941148), 94800612854204, 0, 0], [2650328484316, (-26774921031478), 0], [2145555590358, (-8985124199142)], [1140552796144]], [[217171335113, (-1558312420164), 0, 0, 0], [(-53511631736), 378618354902, 0, 0], [(-29595371684), 306507941479, 0], [(-38917032209), 162936113734], [(-24241085212)]]], r := 1388201092313, ok := true }, Z1 := { p := [[[1695303570144055853]], [[(-57940320918187568), 0], [6284272028474344]], [[758404902833634, 0, 0], [(-214199368251817), 0], [(-71880993593134)]], [[(-12466499361312), 0, 0, 0], [3028946839219, 0, 0], [2452063531837, 0], [1303488909879]], [[248195811557, 0, 0, 0, 0], [(-61156150555), 0, 0, 0], [(-33823281924), 0, 0], [(-44476608238), 0], [(-27704097385)]]], r := 509862737776, ok := true }, Z2 := { p := [[[2390808852209370008527]], [[(-28614455185745615345), 211912946268006981], [(-63687508494510380637)]], [[434793477767891561, (-7242540114773446), 0], [762060260276832304, 785534003559293], [1828178985939060063]], [[(-7933601621621214), 94800612854204, 0, 0], [(-11245252898992991), (-26774921031478), 0], [(-21885235591036161), (-8985124199142)], [(-53556822731394679)]], [[173959312848550, (-1558312420164), 0, 0, 0], [197300403238051, 378618354902, 0, 0], [319796905056555, 306507941479, 0], [641281650085958, 162936113734], [1583786412165362]]], r := 476380067550509, ok := true }, Z3 := { p := [[[4688289583304428168589]], [[(-219806232264899483199), 830591882352143181], [(-126590899977750743544)]], [[11011967511662902804, (-57376259267222253), 0], [6021329823153764168, 2761736563678176], [3651397557796282017]], [[(-561890835305493955), 2814700826853005, 0, 0], [(-303230778704223712), (-174806473757584), 0], [(-174584973660886461), (-32655400792219)], [(-107271345170949839)]], [[28916914833251366, (-142822398046522), 0, 0, 0], [15519833999536441, 7928276470637, 0, 0], [8808970736170336, 2120384362667, 0], [5144685636799356, 597523917079], [3178501612067484]]], r := 21815830373823891, ok := true }, iE := { p := [[[2394147658407237051862]], [[(-28621405499515199366), 0], [(-63675131969876524219)]], [[435006045322127843, 0, 0], [762035634580109065, 0], [1828037420315566920]], [[(-7938683214103003), 0, 0, 0], [(-11243999781888941), 0, 0], [(-21884949976866783), 0], [(-53554255582402721)]], [[174092792279136, 0, 0, 0, 0], [197266702832395, 0, 0, 0], [319784317976538, 0, 0], [641276449250026, 0], [1583731850484680]]], r := 475870687192125, ok := true }, iHu := { p := [[[4691925729989391995408]], [[(-219847406336326459970), 0], [(-126578809708794196861)]], [[11014449471142736350, 0, 0], [6021262835366476389, 0], [3651254599708369417]], [[(-562023083019879734), 0, 0, 0], [(-303224751207309829), 0, 0], [(-174583947664753406), 0], [(-107268729344023959)]], [[28923853605466202, 0, 0, 0, 0], [15519503786887662, 0, 0, 0], [8808893403669691, 0, 0], [5144665626240480, 0], [3178445719115901]]], r := 21798629745462286, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[142130902296694306]], [[1699137550835936, 0], [3780136086827868]], [[(-5511814126369), 0, 0], [45142079213150, 0], [(-7986117197732)]], [[96669574184, 0, 0, 0], [(-167074621948), 0, 0], [(-96194479304), 0], [80599615474]], [[(-2543936389), 0, 0, 0, 0], [2929380512, 0, 0, 0], [(-1514133), 0, 0], [971080225, 0], [(-1221207277)]]], r := 3485650026, ok := true }, de := { p := [[[(-107980294333657048763)]], [[700552243560187418, 0], [403348261443744271]], [[(-18430071894322744), 0, 0], [6348835634035, 0], [(-6109509599495418)]], [[646669247130304, 0, 0, 0], [99932783, 0, 0], [57537057, 0], [123424447395908]], [[(-25526417649197), 0, 0, 0, 0], [1573, 0, 0, 0], [1515492, 0, 0], [522, 0], [(-2805101077104)]]], r := 6023174893434, ok := true }, dde := { p := [[[(-44520137535961641313805)]], [[2342464371716529223003, 0], [1348691607958001674850]], [[(-123287609541619100369), 0, 0], [(-70983781541363538996), 0], [(-40869446321877406092)]], [[6488821554648442850, 0, 0, 0], [3735988167627966237, 0, 0], [2151023490452466431, 0], [1238468070326785542]], [[(-341516923928866091), 0, 0, 0, 0], [(-196630956201470954), 0, 0, 0], [(-113211762664484771), 0, 0], [(-65182530017197887), 0], [(-37529335464447314)]]], r := 43170377984925886, ok := true }, nJu := { p := [[[(-215960588667314097526)]], [[1401104487120374836, 0], [806696522887488543]], [[(-36860143788645488), 0, 0], [12697671268071, 0], [(-12219019198990836)]], [[1293338494260608, 0, 0, 0], [199865566, 0, 0], [115074114, 0], [246848894791817]], [[(-51052835298393), 0, 0, 0, 0], [3147, 0, 0, 0], [3030984, 0, 0], [1044, 0], [(-5610202154208)]]], r := 12046349786863, ok := true }, Jd1 := { p := [[[(-89040275071923282627609)]], [[4684928743433058446006, 0], [2697383215916003349700]], [[(-246575219083238200737), 0, 0], [(-141967563082727077991), 0], [(-81738892643754812184)]], [[12977643109296885700, 0, 0, 0], [7471976335255932474, 0, 0], [4302046980904932863, 0], [2476936140653571084]], [[(-683033847857732181), 0, 0, 0, 0], [(-393261912402941908), 0, 0, 0], [(-226423525328969542), 0, 0], [(-130365060034395774), 0], [(-75058670928894628)]]], r := 86340755969851767, ok := true }, term0 := { p := [[[149147270865940897400804838]], [[(-15692678322571491425767599), 0], [(-9030635466941469073944559)]], [[1238710725746609080171734, 0, 0], [950380255811464475698026, 0], [410353293414252213507614]], [[(-86920579651889547337732), 0, 0, 0], [(-75024416209878562542146), 0, 0], [(-43188630446817112861061), 0], [(-16577302018329709311300)]], [[5718203049931353045157, 0, 0, 0, 0], [5264674682017838292097, 0, 0, 0], [3409458901841641073283, 0, 0], [1744783612234105846073, 0], [627868356102390766890]]], r := 1258140155937638505331, ok := true }, r0 := { p := [[[25474336744186020986477]], [[(-1070335025000180792469), 7172506612403258697084], [(-677694764034270955554)]], [[37486614832029358305, (-294390147591033513089), 482564217075393431409], [28022489934826515652, (-191574993777661302427)], [19452807744243804624]], [[(-1349617105066227998), 10071296031090695391, (-17851074409933088296), (-4112675995377074281)], [(-948158920222397373), 7785481918861037846, (-13103579866984149591)], [(-799818839446928929), 5504899534928751432], [(-569822366668913054)]], [[53278448522931578, (-358503185962868810), 544221560219097062, 429797251109213987, (-122800209472628653)], [32867922991381736, (-258665337063609643), 494023530753714054, 81214720790863855], [26731965041556060, (-222813198899102165), 378193682286179630], [23349028343816455, (-161349358357472419)], [16849457243721818]]], r := 488969374562667103, ok := true }, r1 := { p := [[[33125174068190204168412]], [[(-1382135566709757612113), 0], [(-882289546973239285071)]], [[48078734577188129171, 0, 0], [36293172473527556321, 0], [25333729168958171756]], [[(-1725496518029330761), 0, 0, 0], [(-1221421687659310375), 0, 0], [(-1036712887375328750), 0], [(-742224333976298493)]], [[68161555577842449, 0, 0, 0, 0], [42227855988573710, 0, 0, 0], [34477383623358186, 0, 0], [30278419187445003, 0], [21950028584123290]]], r := 69557035367336869, ok := true }, r2 := { p := [[[26593833584943434826054442]], [[(-1237524107507382169748382), 7962559560335734542730], [(-1567235853838756325678115)]], [[54126592538650926955822, (-262658883017038032647), 456232286123675006], [71514435449491816410587, (-235679581111969654908)], [70067521623554094625623]], [[(-2500098347671138025211), 9526068515562905215, 432553919422143, (-41267435765464)], [(-3084469043117129856360), 7421369021587681373, 108202190861130], [(-3158703661504347303161), 7079480507757123447], [(-2798448225848265015239)]], [[121369487573031958265, (-393154988422070490), (-10096081634520), 874700110914, (-6228036091)], [141415431492893210884, (-258799246192660989), 3631331792687, (-1291440326764)], [135049736116494755567, (-218825495725311472), (-1424331586861)], [125063892842507166872, (-213394749676078422)], [105073147459779070345]]], r := 767694097117315620430, ok := true }, r3 := { p := [[[297809677078873382992794274]], [[(-31340145668106754544859222), 95960597363949090568691], [(-18046571754501181505078051)]], [[2474005332723711529709885, (-8964433112803778332798), 1710805944217620602], [1899389890234583555403660, (-2915872154647062260635)], [820261068572276923027463]], [[(-173606803027719312817788), 677836791700616503860, 12327018105813040, (-317401468921623)], [(-149945274455212670742662), 272240721478346753871, (-272266812549811)], [(-86335720591251984348715), 88448340170079967163], [(-33141101950879167601298)]], [[11421199810195726658871, (-46522015300684321184), (-760032873428925), 3969946230567, (-1243399149275)], [10522245184376187003428, (-20579693187883715023), 68992684239675, (-10241390728422)], [6815779254333724806476, (-8256042284152600297), 482055164546], [3488308315550327531202, (-2681786719923362281)], [1255327524703469534074]]], r := 138500957898429993990887, ok := true }, eta := { p := [[[(-26680697553475404518866899)]], [[1242898347794575862840293, 0], [1569817199650621602272071]], [[(-54418123616136959570501), 0, 0], [(-71673811297191401521043), 0], [(-70145192687306342485727)]], [[2515515547932002522309, 0, 0, 0], [3093099929854386135989, 0, 0], [3163494946674648537399, 0], [2800792014728154769064]], [[(-122180660060334397453), 0, 0, 0, 0], [(-141871563811398444539), 0, 0, 0], [(-135309064629574261222), 0, 0], [(-125208397757430667529), 0], [(-105143962927395038316)]]], r := 77753108096046852060, 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 := 19703248369745920, bh := 562949953421312, tc := 16140901064495857664, th := 2305843009213693952, sc := 5476377146882523136, sh := 288230376151711744 }
noncomputable def q5 : Cert := { V0 := [[[1487132835124008121]], [[(-50349335549165714), 210460574947577464], [5186454979025891]], [[635325960807265, (-6991284276258510), (-421089610142503)], [(-171808744839499), 720168017092872], [(-56055900882715)]], [[(-9968103995575), 81425792846692, 42381856078774, (-18948379273394)], [2188036632578, (-22457164660562), (-4365729678111)], [1875724150409, (-7855749811385)], [958700265233]], [[192271852060, (-1137329142921), (-1936984410138), 1832741118989, 114965817783], [(-40292336548), 216512555958, 433499575128, (-188789567891)], [(-24080103076), 252504045037, 32306789335], [(-32145999910), 134596505035], [(-19214654026)]]], r0 := 5924353797809, V1 := [[[1697153489845027934]], [[(-57296424759651962), 0], [5902070488793237]], [[714738789764891, 0, 0], [(-193815283101125), 0], [(-63877888625000)]], [[(-11045362522872), 0, 0, 0], [2384403505550, 0, 0], [2124828919255, 0], [1092773100870]], [[210894253209, 0, 0, 0, 0], [(-42497725990), 0, 0, 0], [(-26646641573), 0, 0], [(-36445780352), 0], [(-21905231013)]]], r1 := 1680343221976, V2 := [[[18421732584541887634]], [[(-339875338517225), 2669785318791], [(-712574252118235)]], [[794291922111, (-22465865437), (-270130158)], [(-9830982447750), 153596132978], [36112644680]], [[(-16563373383), (-900262819), 8237279, 26778], [25555572993, (-1272527005), (-23343265)], [(-2157216954), 2227860544], [(-258581956)]], [[460064983, 3558187, 42037, (-1409), (-2)], [(-530091059), (-52520677), 709511, 3086], [51165471, (-17806285), (-675847)], [14838848, 412117], [3242945]]], r2 := 28995656028, V3 := [[[18435042800485698756]], [[(-615803369953499), 2470000371302], [(-334393626243812)]], [[2870010934, 76863043838, (-496152871)], [(-17596619716465), 142134243690], [(-2061354985)]], [[2025245, (-2870932984), (-4643677), 97807], [164987244, 4434077119, (-42855042)], [(-64698168), 2062594290], [(-381169)]], [[(-34103), (-2013166), 922253, (-1223), (-19)], [129976, (-165066914), (-404931), 11262], [2388480, 64710070, (-1239793)], [(-16761), 393302], [1897]]], r3 := 338193169263, Vm := [[[18421736093570796076]], [[(-339935633317373), 0], [(-712369081238908)]], [[793907040488, 0, 0], [(-9834566953208), 0], [39196164652]], [[(-16566396651), 0, 0, 0], [25533927140, 0, 0], [(-2212935257), 0], [(-256675690)]], [[460248393, 0, 0, 0, 0], [(-530255285), 0, 0, 0], [50864615, 0, 0], [14783551, 0], [3234094]]], rm := 5310213698 }
noncomputable def w5 : Wit := { Z0 := { p := [[[1494145270102820056]], [[(-51064346158992473), 213449324300402865], [5260107794836562]], [[668790659935311, (-7294906594141782), 0], [(-179284201867924), 751443970690937], [(-56592593211147)]], [[(-11013033900428), 95541522847901, 0, 0], [2538006105353, (-25612028838275), 0], [1930482676207, (-8084656173021)], [967021607981]], [[219694547787, (-1573290557204), 0, 0, 0], [(-51372140779), 362572300764, 0, 0], [(-26646614101), 275783239458, 0], [(-32995174551), 138145943997], [(-19371465084)]]], r := 1174308638197, ok := true }, Z1 := { p := [[[1707594594403222921]], [[(-58359252753134255), 0], [6011551765527499]], [[764332182783213, 0, 0], [(-204896230706198), 0], [(-64677249384168)]], [[(-12586324457631), 0, 0, 0], [2900578406118, 0, 0], [2206265915665, 0], [1105167551978]], [[251079483185, 0, 0, 0, 0], [(-58711018033), 0, 0, 0], [(-30453273258), 0, 0], [(-37708770915), 0], [(-22138817239)]]], r := 425333246150, ok := true }, Z2 := { p := [[[2270342015148821117590]], [[(-27173031794826818649), 213449324300402865], [(-56970308270843875883)]], [[413511772822436056, (-7294906594141782), 0], [681649853108872548, 751443970690937], [1541392823019163209]], [[(-7559930113082586), 95541522847901, 0, 0], [(-10069688752759194), (-25612028838275), 0], [(-18451359922015926), (-8084656173021)], [(-42566773818583030)]], [[166070428811935, (-1573290557204), 0, 0, 0], [176941935902085, 362572300764, 0, 0], [269887125452068, 275783239458, 0], [509669902179286, 138145943997], [1186696560861321]]], r := 378621026402044, ok := true }, Z3 := { p := [[[4448903200908597301252]], [[(-208423061695459596156), 835989318821944959], [(-113177918137157233739)]], [[10438779370590939885, (-57717690503007965), 0], [5380177725092311235, 2637899063195334], [3077107760503380852]], [[(-532556064049950194), 2830178489033038, 0, 0], [(-270883572296503585), (-166768547182449), 0], [(-147048884799670346), (-29354611314394)], [(-85220024604145321)]], [[27404091086941650, (-143579204527708), 0, 0, 0], [13862427821731702, 7556086645007, 0, 0], [7418106930595503, 1904571368536, 0], [4085096830369750, 506164743733], [2380544240683809]]], r := 18488204025914209, ok := true }, iE := { p := [[[2273705027836131909401]], [[(-27180030257445327792), 0], [(-56958468853616767557)]], [[413726797954028516, 0, 0], [681626310810552729, 0], [1541265444769681613]], [[(-7565077828938803), 0, 0, 0], [(-10068483480291315), 0, 0], [(-18451103044814078), 0], [(-42564597252487604)]], [[166205788132840, 0, 0, 0, 0], [176909491782087, 0, 0, 0], [269875757419526, 0, 0], [509665494354422, 0], [1186652959690705]]], r := 378191508094753, ok := true }, iHu := { p := [[[4452562976370995593629]], [[(-208464365791791610864), 0], [(-113166370001258356384)]], [[10441273086868416290, 0, 0], [5380114614548895732, 0], [3076979252538293395]], [[(-532688955996422429), 0, 0, 0], [(-270877837658828610), 0, 0], [(-147047969014885603), 0], [(-85217808727378309)]], [[27411063696696403, 0, 0, 0, 0], [13862113513293942, 0, 0, 0], [7418037608627651, 0, 0], [4085079982307669, 0], [2380499613078476]]], r := 18471791671996890, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[149659855942167947]], [[1789044472802301, 0], [3749121429102591]], [[(-5845969426906), 0, 0], [44768503845138, 0], [(-7530153681016)]], [[102528335109, 0, 0, 0], [(-167080678645), 0, 0], [(-90700939835), 0], [71651406064]], [[(-2698114353), 0, 0, 0, 0], [2929380414, 0, 0, 0], [(-1514216), 0, 0], [863270473, 0], [(-1023592440)]]], r := 3476511873, ok := true }, de := { p := [[[(-107197091263608198594)]], [[700564941461607884, 0], [380306682507729994]], [[(-18430071688394994), 0, 0], [6349065788517, 0], [(-5431229289396402)]], [[646669247133644, 0, 0, 0], [105995078, 0, 0], [57540186, 0], [103451996876727]], [[(-25526417649197), 0, 0, 0, 0], [1770, 0, 0, 0], [1515656, 0, 0], [522, 0], [(-2216828504430)]]], r := 5933340612251, ok := true }, dde := { p := [[[(-41976890517602682717486)]], [[2208609240083482252194, 0], [1198959301759604652990]], [[(-116242603282698498302), 0, 0], [(-63103133847401738937), 0], [(-34255983498003392694)]], [[6118031751525661247, 0, 0, 0], [3321217236330445767, 0, 0], [1802946499722241062, 0], [978742385625994920]], [[(-322001671132930178), 0, 0, 0, 0], [(-174800907186453713), 0, 0, 0], [(-94891921047103998), 0, 0], [(-51512757138208580), 0], [(-27964068160741345)]]], r := 38192024857179491, ok := true }, nJu := { p := [[[(-214394182527216397188)]], [[1401129882923215768, 0], [760613365015459989]], [[(-36860143376789987), 0, 0], [12698131577035, 0], [(-10862458578792804)]], [[1293338494267289, 0, 0, 0], [211990157, 0, 0], [115080372, 0], [206903993753454]], [[(-51052835298393), 0, 0, 0, 0], [3541, 0, 0, 0], [3031313, 0, 0], [1044, 0], [(-4433657008859)]]], r := 11866681224492, ok := true }, Jd1 := { p := [[[(-83953781035205365434971)]], [[4417218480166964504388, 0], [2397918603519209305980]], [[(-232485206565396996604), 0, 0], [(-126206267694803477873), 0], [(-68511966996006785388)]], [[12236063503051322495, 0, 0, 0], [6642434472660891535, 0, 0], [3605892999444482125, 0], [1957484771251989840]], [[(-644003342265860355), 0, 0, 0, 0], [(-349601814372907426), 0, 0, 0], [(-189783842094207995), 0, 0], [(-103025514276417160), 0], [(-55928136321482690)]]], r := 76384049714358974, ok := true }, term0 := { p := [[[132604158323773485445781152]], [[(-13951699620150579587979902), 0], [(-7569741194042733420138092)]], [[1101275606229791795395675, 0, 0], [796625553238894982352242, 0], [324308401500221472798264]], [[(-77276380651038559515504), 0, 0, 0], [(-62886509215809167181647), 0, 0], [(-34132317634207108748519), 0], [(-12352528090232346565477)]], [[5083730909999171471356, 0, 0, 0, 0], [4412913565114639115018, 0, 0, 0], [2694514317450636635938, 0, 0], [1300111576489861416893, 0], [441117195768189798269]]], r := 1033707750468029002051, ok := true }, r0 := { p := [[[24192454332068208174376]], [[(-1017312931214354268950), 6810157509503695436322], [(-606219611558096275122)]], [[35691371410611310811, (-279661226017883217416), 457785905461259169235], [25082888304208358684, (-171349447704725986190)], [16401494455765095268]], [[(-1287338399219213537), 9581648501149813170, (-16917085346435442842), (-3958225688506228908)], [(-849849108677090671), 6966673657537925463, (-11714348582052465855)], [(-674754699287141985), 4640937327487163583], [(-452901189048903322)]], [[50892442821098923, (-341674163134648881), 515725362163513704, 413493818202118999, (-117855076412052453)], [29504561316669710, (-231741114181388241), 441466995114716452, 73443056262458547], [22580533393869869, (-187923776579525434), 318702522699391313], [18568349534072282, (-128230205372281720)], [12625186607437489]]], r := 431738112081375529, ok := true }, r1 := { p := [[[31456323588287106942664]], [[(-1313467340237578857941), 0], [(-789207637667685369079)]], [[45766246339156520393, 0, 0], [32483051333673423080, 0], [21359284073757313537]], [[(-1645488037187355924), 0, 0, 0], [(-1094634432372282185), 0, 0], [(-874538539081581674), 0], [(-589911395047538223)]], [[65094593561009832, 0, 0, 0, 0], [37901348622625857, 0, 0, 0], [29119721956869517, 0, 0], [24077239167316714, 0], [16446572174014757]]], r := 56959964456660807, ok := true }, r2 := { p := [[[23718812124253173984164716]], [[(-1106199158600524899509582), 7517908365926627037288], [(-1317464631596456126895770)]], [[48458291098589649827478, (-248642222379611256980), 456443352710030916], [60243490823579384423080, (-209730758404564032137)], [55524241671014884274107]], [[(-2240119314851201992359), 9036829096470659684, 439700093887198, (-43794077869690)], [(-2602240180488750305746), 6618513412460016975, 102933323110744], [(-2508144267321585395447), 5939457106650444862], [(-2090606323693246707307)]], [[108786968684742992225, (-373429753759352153), (-10266696104900), 926353798538, (-4995113846)], [119401090942776089971, (-231229531611205312), 3504778477660, (-1289969369565)], [107391996019003114888, (-183953355274594119), (-1268421855649)], [93613955383804168643, (-168791724824664752)], [74003215644238639528]]], r := 587173220619745033450, ok := true }, r3 := { p := [[[264751170124256816156266869]], [[(-27860772840582697272380535), 90462418549704222286329], [(-15126415425994030055694733)]], [[2199330372869701284496550, (-8451087932389533868439), 1710269147361800767], [1592032674027554749844636, (-2591842441307800427767)], [648243385721145106949170]], [[(-154331801377242047133178), 639030926892576657353, 12464041558401379, (-336405487536449)], [(-125680959001545900815944), 241994452909577469672, (-266950440809338)], [(-68229817535338220703671), 74128149051653936652], [(-24694385883963423138012)]], [[10153124739129655316191, (-43859051983760755711), (-768118267239637), 5356723106991, (-1530789848787)], [8819511754244826129900, (-18293442365432951539), 66253800056359, (-10728636878466)], [5386398001615078932422, (-6919508481636666736), (-329456479281)], [2599228270619879638009, (-2119179764072145900)], [881929500712369868656]]], r := 109922160656032299706980, ok := true }, eta := { p := [[[(-23800806403544618498461187)]], [[1111272722144552979675542, 0], [1319761312202244609398303]], [[(-48733538727635656336376), 0, 0], [(-60385305764877064682666), 0], [(-55589392607242065181956)]], [[2254675944479353205839, 0, 0, 0], [2609920556997621268085, 0, 0], [2512163598896626431163, 0], [2092459871627747180709]], [[(-109552869792283216836), 0, 0, 0, 0], [(-119806998844191775653), 0, 0, 0], [(-107609554434557165781), 0, 0], [(-93728244753898834789), 0], [(-74056016928652244334)]]], r := 59954122208687544173, 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 18014398509481984 20266198323167232 13835058055282163712 18446744073709551616 4611686018427387904 5764607523034234880 :=
  (RegionPosI.split_s 5188146770730811392 (RegionPosI.split_b 19140298416324608 (RegionPosI.split_s 4899916394579099648 (RegionPosI.of_check c0 q0 ok_0 18014398509481984 19140298416324608 13835058055282163712 18446744073709551616 4611686018427387904 4899916394579099648 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 18014398509481984 19140298416324608 13835058055282163712 18446744073709551616 4899916394579099648 5188146770730811392 (by decide +kernel))) (RegionPosI.split_s 4899916394579099648 (RegionPosI.of_check c2 q2 ok_2 19140298416324608 20266198323167232 13835058055282163712 18446744073709551616 4611686018427387904 4899916394579099648 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 19140298416324608 20266198323167232 13835058055282163712 18446744073709551616 4899916394579099648 5188146770730811392 (by decide +kernel)))) (RegionPosI.split_b 19140298416324608 (RegionPosI.of_check c4 q4 ok_4 18014398509481984 19140298416324608 13835058055282163712 18446744073709551616 5188146770730811392 5764607523034234880 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 19140298416324608 20266198323167232 13835058055282163712 18446744073709551616 5188146770730811392 5764607523034234880 (by decide +kernel))))

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

View graph