Prove2Me

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

Definition
CK_CKLaneC_RSC2_S01_0103

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

general-courtade-kumartransplant

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

Definition code
import Definitions.Def_CK_CKLaneC_RSC2_S01_0103_part00

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

namespace CKLaneC.RSC2.S01_0103
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def q6 : Cert := { V0 := [[[163462252422213533]], [[(-2783237347863513), 163443735265634486], [388612431272701]], [[18043142170102, (-2782291503899086), (-27772024301685)], [(-6607224315089), 388480366818010], [(-4058226506821)]], [[(-141193043358), 18020906594461, 1418450061067, (-9251158044861)], [45612644572, (-6600481904130), (-198052576184)], [69022643972, (-4057161327658)], [63672210311]], [[1330245027, (-140844884422), (-33340559183), 472290317034, 4635986066], [(-427465245), 45453254040, 10109862783, (-65944030434)], [(-469908055), 68968245821, 1597517853], [(-1083066671), 63656880578], [(-1160252179)]]], r0 := 1074992404948, V1 := [[[1303060929903501222]], [[(-22030027385650807), 0], [3075965659167998]], [[138841908259071, 0, 0], [(-51188068591655), 0], [(-32199366254276)]], [[(-1044439951000), 0, 0, 0], [325919765401, 0, 0], [538640922052, 0], [505540985202]], [[9550475873, 0, 0, 0, 0], [(-2809915937), 0, 0, 0], [(-3443041056), 0, 0], [(-8469475741), 0], [(-9215679546)]]], r1 := 340232474190, V2 := [[[18445003741436882369]], [[(-11565215548493), 12659905809], [(-44552629729142)]], [[10691117463, (-54226836), (-88314)], [(-298660185198), 651688550], [1072845938]], [[(-115345673), (-1008344), 1345, 0], [300180582, (-2768820), (-6824)], [(-32331716), 8424631], [(-7585490)]], [[1638190, 1665, 3, (-1), 0], [(-3229878), (-52336), 103, 0], [398469, (-35154), (-176)], [219694, 725], [88078]]], r2 := 499308303, V3 := [[[18445950695813684330]], [[(-21441780984395), 11466318975], [(-20345097322136)]], [[23751126, 186326408, (-159320)], [(-549823042294), 590401619], [(-53441384)]], [[4982, (-3393548), (-859), 2], [1222429, 9604524, (-12309)], [(-871655), 7636707], [(-4792)]], [[(-46), (-708), 76, 0, 0], [279, (-174674), (-67), 0], [15796, 124534, (-318)], [(-102), 704], [24]]], r3 := 2571182431, Vm := [[[18445003833020668361]], [[(-11565662921495), 0], [(-44547907783715)]], [[10684562072, 0, 0], [(-298683218638), 0], [1134100154]], [[(-115337838), 0, 0, 0], [299841087, 0, 0], [(-32629545), 0], [(-7578046)]], [[1638117, 0, 0, 0, 0], [(-3229451), 0, 0, 0], [394022, 0, 0], [219669, 0], [88041]]], rm := 49483393 }
noncomputable def w6 : Wit := { Z0 := { p := [[[163471511928255933]], [[(-2783710348830367), 163471511928255933], [388678474528361]], [[18054263159757, (-2783710348830367), 0], [(-6610596459203), 388678474528361], [(-4058759159129)]], [[(-141367207508), 18054263159757, 0, 0], [45692377960, (-6610596459203), 0], [69049848389, (-4058759159129)], [63679876016]], [[1332516588, (-141367207508), 0, 0, 0], [(-428738183), 45692377960, 0, 0], [(-470549162), 69049848389, 0], [(-1083458208), 63679876016], [(-1160384677)]]], r := 249552618434, ok := true }, Z1 := { p := [[[1307772095426047466]], [[(-22269682790642930), 0], [3109427796226890]], [[144434105278056, 0, 0], [(-52884771673624), 0], [(-32470073273031)]], [[(-1130937660061), 0, 0, 0], [365539023680, 0, 0], [552398787116, 0], [509439008130]], [[10660132707, 0, 0, 0, 0], [(-3429905461), 0, 0, 0], [(-3764393295), 0, 0], [(-8667665659), 0], [(-9283077414)]]], r := 85914837299, ok := true }, Z2 := { p := [[[24725450284231259847048]], [[(-149336282586472006120), 163471511928255933], [(-575287514124060173142)]], [[1089722264404297267, (-2783710348830367), 0], [3475789132313160260, 388678474528361], [14136850714804247832]], [[(-9407350762639406), 18054263159757, 0, 0], [(-24922542098892936), (-6610596459203), 0], [(-85423740701602092), (-4058759159129)], [(-352849382694216380)]], [[98170337567811, (-141367207508), 0, 0, 0], [209615250717840, 45692377960, 0, 0], [608492766897603, 69049848389, 0], [2132306885087866, 63679876016], [8871874045653348]]], r := 1014129676059244, ok := true }, Z3 := { p := [[[50612811331978908475291]], [[(-1251475327861142027571), 669245493609343131], [(-1187466067306491545832)]], [[32517974137660067835, (-23902316441910310), 0], [29615838261209936732, 1460784368014628], [29272278203376850452]], [[(-857135588980787560), 611823641649065, 0, 0], [(-772059890450476027), (-48811101496451), 0], [(-732462940356569709), (-15539300806185)], [(-732013095726868043)]], [[22746922711685536, (-16058741751968), 0, 0, 0], [20391009909866074, 1177715547517, 0, 0], [19119668710812302, 526577228229, 0], [18353118978513376, 245337444165], [18430142785368918]]], r := 26519202414532899, ok := true }, iE := { p := [[[24728965819932837834537]], [[(-149355719003385794947), 0], [(-575279155401261799481)]], [[1089866353038814031, 0, 0], [3475743093456042040, 0], [14136763429181452062]], [[(-9408609144259360), 0, 0, 0], [(-24922138027133701), 0, 0], [(-85423259534884031), 0], [(-352848013226992600)]], [[98183612140737, 0, 0, 0, 0], [209610972954257, 0, 0, 0], [608488693841085, 0, 0], [2132299333652571, 0], [8871849091007059]]], r := 1013986021277225, ok := true }, iHu := { p := [[[50619672936874925147178]], [[(-1251637635672687921021), 0], [(-1187451090253575527716)]], [[32522200745678427996, 0, 0], [29615518448897715238, 0], [29272118882853200229]], [[(-857247065622486203), 0, 0, 0], [(-772051866437375851), 0, 0], [(-732459463029872108), 0], [(-732010580344061374)]], [[22749881960553687, 0, 0, 0, 0], [20390803382858036, 0, 0, 0], [19119580903478608, 0, 0], [18353063665234752, 0], [18430096778257285]]], r := 26518758769277465, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[13760477061545902]], [[83109255774060, 0], [320115110333638]], [[(-104502481745), 0, 0], [1932719798076, 0], [(-419469971505)]], [[941443556, 0, 0, 0], [(-2679608432), 0, 0], [(-2542192615), 0], [3584989241]], [[(-12722211), 0, 0, 0, 0], [24139579, 0, 0, 0], [(-1477), 0, 0], [21727208, 0], [(-45961400)]]], r := 28291991, ok := true }, de := { p := [[[(-143009429304680086281)]], [[359643222314576817, 0], [341199980144598519]], [[(-4859939040062733), 0, 0], [198291023965, 0], [(-4374264658675793)]], [[87566469230809, 0, 0, 0], [115239, 0, 0], [109329, 0], [74773754883733]], [[(-1774995997922), 0, 0, 0, 0], [1, 0, 0, 0], [1478, 0, 0], [1, 0], [(-1437956824687)]]], r := 348585658166, ok := true }, dde := { p := [[[(-618852515252069250521120)]], [[16725384004505666607177, 0], [15867672004274606792587]], [[(-452037405736194033086), 0, 0], [(-428856000512120494267), 0], [(-406863384913116178024)]], [[12217227182059206199, 0, 0, 0], [11590702711184147536, 0, 0], [10996307700354208070, 0], [10432394484951620317]], [[(-330195329244830305), 0, 0, 0, 0], [(-313262235437407033), 0, 0, 0], [(-297197505414961591), 0, 0], [(-281956607701387881), 0], [(-267497294485915754)]]], r := 48630342793320003, ok := true }, nJu := { p := [[[(-286018858609360172562)]], [[719286444629153634, 0], [682399960289197038]], [[(-9719878080125466), 0, 0], [396582047930, 0], [(-8748529317351586)]], [[175132938461619, 0, 0, 0], [230478, 0, 0], [218658, 0], [149547509767467]], [[(-3549991995844), 0, 0, 0, 0], [2, 0, 0, 0], [2957, 0, 0], [2, 0], [(-2875913649374)]]], r := 697171316328, ok := true }, Jd1 := { p := [[[(-1237705030504138501042240)]], [[33450768009011333214355, 0], [31735344008549213585175]], [[(-904074811472388066171), 0, 0], [(-857712001024240988534), 0], [(-813726769826232356048)]], [[24434454364118412399, 0, 0, 0], [23181405422368295073, 0, 0], [21992615400708416141, 0], [20864788969903240635]], [[(-660390658489660610), 0, 0, 0, 0], [(-626524470874814066), 0, 0, 0], [(-594395010829923181), 0, 0], [(-563913215402775761), 0], [(-534994588971831507)]]], r := 97260685586639995, ok := true }, term0 := { p := [[[28784036433956670194963969919]], [[(-1555843681546454647712712806), 0], [(-1476001932514519109781338876)]], [[63074065790371472421652858, 0, 0], [79782601676029911244240199, 0], [56767991037943076644913745]], [[(-2272927090533954659804983), 0, 0, 0], [(-3234412411622767641796254), 0, 0], [(-3068507067181934283434892), 0], [(-1940763555848138551047686)]], [[76787829736405773223970, 0, 0, 0, 0], [116555088958404152634184, 0, 0, 0], [124398489359763951777142, 0, 0], [104905292284129762508150, 0], [62203528151353349081759]]], r := 21281843150597808254643, ok := true }, r0 := { p := [[[5493592760856399361984]], [[(-115079554680275203074), 10985202825187067241576], [(-127501903758490991549)]], [[1954385288951201113, (-230051093789966085580), 5488636816727072427430], [2635719439826438654, (-254967157410981805051)], [3130478107143115144]], [[(-33881338946827258), 3905720152191322302, (-114809586188334105305), (-3963001813211693627)], [(-43623961882302045), 5269452392383569951, (-127410289447435025105)], [(-64390977488786995), 6260130679873188616], [(-78094597709602282)]], [[650512480576027, (-67697940934033232), 1946762321121233841, 215819876353791193, (-988758520125098148)], [734838061153314, (-87192472126309133), 2630754185802972943, 73267353015131264], [1055205890401270, (-128737275417190346), 3128414498094237580], [1601486511802913, (-156169670822173285)], [1962848851760403]]], r := 442454809737814122, ok := true }, r1 := { p := [[[347642819025896004395755]], [[(-7151728683103483223006), 0], [(-8086925182048361291004)]], [[119123046889920531236, 0, 0], [164741824177933272502, 0], [198700625342797028942]], [[(-2043642392510172112), 0, 0, 0], [(-2682772102126905688), 0, 0], [(-4032203038675287629), 0], [(-4959014261694554828)]], [[39288089377517611, 0, 0, 0, 0], [44781487954561712, 0, 0, 0], [65081664696343137, 0, 0], [100394847036603600, 0], [124677791731515751]]], r := 105413501033183202, ok := true }, r2 := { p := [[[4447555691978837974288331849]], [[(-96877006617011421270365563), 104476613232999648507453], [(-224136159093775066419652455)]], [[2041754111685175897778067, (-1596296329682508649276), 448023530245805881], [4809888976865659881567272, (-2640977362682281391864)], [8529355259690536955566308]], [[(-46925879470984462070537), 27341830410359105441, (-309120511353415), (-645087097507538)], [(-100208817425861859187780), 39099708377776088527, (-115734905502510)], [(-181339749889177810851221), 67319817454899937929], [(-289406500460288382290342)]], [[1155883243882013597688, (-552853563824735606), (-589134871883673), 14869544422549, (-71106191598764)], [2288728638657376274055, (-650340265176957257), (-220172938052363), 54452398074702], [3750465809298000538164, (-984134877516964026), (-190388098221354)], [6111754534470390171920, (-1720054501144743822)], [9222090125812521482516]]], r := 21452813862629444847855, ok := true }, r3 := { p := [[[57552969445555153572757608324]], [[(-3110962004090930954879148121), 1369129719986828246093343], [(-2951616264805569707466344870)]], [[126119955008334128823171460, (-65780785809683386245971), 1695232104372260401], [159546591613663834131257323, (-35153995210415986495689)], [113526040379562216180539209]], [[(-4544860962643541511837513), 2555663503434498337751, (-39313580888355432), (-45316544967197125)], [(-6468101900581297930984132), 1688506431745287425939, (-28762288671219563)], [(-6136536814437972879942963), 901798944232189991203], [(-3881272165049426317804180)]], [[153542521320719714006050, (-90111329862572737735), (-29906194784117635), 4475655594699191, (-4610491784573238)], [233084651798524472605649, (-65634106022753271595), (-22653904918289007), (-41344526195226013)], [248778425026086986551889, (-43343359881228823514), (-6611704731691403)], [209798305285336232712017, (-23129220796064512016)], [124400495044332564226395]]], r := 2233014332984813783697255, ok := true }, eta := { p := [[[(-4449351193422244567981860713)]], [[96923439087210089305327095, 0], [224181647984859798536790475]], [[(-2042940578454278273254319), 0, 0], [(-4811057174835318536156411), 0], [(-8530515989117471695431642)]], [[46956920990003587402917, 0, 0, 0], [100238596478590472130580, 0, 0], [181369473659271944151637, 0], [289436174478327292053666]], [[(-1156708367892816475194), 0, 0, 0, 0], [(-2289507564081894187090), 0, 0, 0], [(-3751222890603010563661), 0, 0], [(-6112513626901026538614), 0], [(-9222849531979672704182)]]], r := 1865924797763167702471, ok := true } }
theorem sB_6 : stageB c6 w6 = true := by decide +kernel
theorem s0_6 : stageC0 w6 q6 = true := by decide +kernel
theorem s1_6 : stageC1 w6 q6 = true := by decide +kernel
theorem s2_6 : stageC2 w6 q6 = true := by decide +kernel
theorem s3_6 : stageC3 w6 q6 = true := by decide +kernel
theorem sE_6 : stageE w6 q6 = true := by decide +kernel
theorem sF_6 : stageF w6 = true := by decide +kernel
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 := 1372190511464448, bh := 35184372088832, tc := 2305843009213693952, th := 2305843009213693952, sc := 5620492334958379008, sh := 144115188075855872 }
noncomputable def q7 : Cert := { V0 := [[[157966841556764875]], [[(-2712717716350375), 157950129860214881], [375577089275909]], [[17226730878858, (-2711856777657466), (-25064417415627)], [(-6429752744233), 375457891894486], [(-3922027605411)]], [[(-131132674902), 17206479665541, 1291139516642, (-8349594156107)], [43159575986, (-6423618436964), (-178758895034)], [67192525273, (-3921066253068)], [61534921465]], [[1188693885, (-130818679755), (-30365892698), 429932385137, 3907512279], [(-391015962), 43014656244, 9198270844, (-59524348157)], [(-445501862), 67143019813, 1441817057], [(-1054473231), 61521086125], [(-1121301910)]]], r0 := 1033361300986, V1 := [[[1259548036647203920]], [[(-21486895885434325), 0], [2974871202258058]], [[132796080289864, 0, 0], [(-49917153698716), 0], [(-31135628967517)]], [[(-972179375181), 0, 0, 0], [309768662330, 0, 0], [525207815418, 0], [488815121518]], [[8542349751, 0, 0, 0, 0], [(-2578841661), 0, 0, 0], [(-3275835432), 0, 0], [(-8258127490), 0], [(-8910518784)]]], r1 := 324854571151, V2 := [[[18444980652872865542]], [[(-11523784878435), 12547431755], [(-45148774505115)]], [[10036307777, (-58240882), (-85612)], [(-297496810476), 645942267], [1009744280]], [[(-103248573), (-998836), 1356, 0], [281845576, (-2977121), (-6615)], [(-30785549), 8351579], [(-7156623)]], [[1394699, 1508, 2, (-1), 0], [(-2890888), (-51824), 104, 0], [375051, (-37894), (-171)], [209279, 731], [83086]]], r2 := 496239964, V3 := [[[18445907812346759183]], [[(-21441685921535), 11825392036], [(-21444738514812)]], [[23779957, 172743922, (-160739)], [(-549818149306), 608911662], [(-55121474)]], [[4635, (-3397646), (-562), 2], [1224045, 8905365, (-12419)], [(-808420), 7876741], [(-4991)]], [[(-41), (-659), 72, 0, 0], [260, (-174903), (-44), 0], [15821, 115496, (-321)], [(-97), 732], [24]]], r3 := 2362669110, Vm := [[[18444980743535745498]], [[(-11524258381264), 0], [(-45144099981200)]], [[10029797704, 0, 0], [(-297521196904), 0], [1070385097]], [[(-103241291), 0, 0, 0], [281508547, 0, 0], [(-31101095), 0], [(-7149233)]], [[1394635, 0, 0, 0, 0], [(-2890491), 0, 0, 0], [370639, 0, 0], [209250, 0], [83049]]], rm := 48726997 }
noncomputable def w7 : Wit := { Z0 := { p := [[[157975198186979705]], [[(-2713148252838026), 157975198186979705], [375636697262353]], [[17236859217945, (-2713148252838026), 0], [(-6432820695555), 375636697262353], [(-3922508334449)]], [[(-131289744611), 17236859217945, 0, 0], [43232068363, (-6432820695555), 0], [67217282544, (-3922508334449)], [61541839841]], [[1190702565, (-131289744611), 0, 0, 0], [(-392159489), 43232068363, 0, 0], [(-446085332), 67217282544, 0], [(-1054829571), 61541839841], [(-1121421490)]]], r := 241015239080, ok := true }, Z1 := { p := [[[1263801585495837643]], [[(-21705186022704202), 0], [3005093578098831]], [[137894873743560, 0, 0], [(-51462565564439), 0], [(-31380066675587)]], [[(-1050317956886), 0, 0, 0], [345856546904, 0, 0], [537738260358, 0], [492334718730]], [[9525620520, 0, 0, 0, 0], [(-3137275911), 0, 0, 0], [(-3568682650), 0, 0], [(-8438636563), 0], [(-8971371917)]]], r := 81977624752, ok := true }, Z2 := { p := [[[24431062881275672008330]], [[(-145087236622204026451), 157975198186979705], [(-568433982318116622872)]], [[1035538749521339927, (-2713148252838026), 0], [3378548321239463787, 375636697262353], [13968397467801459078]], [[(-8669050781846007), 17236859217945, 0, 0], [(-23713876918399144), (-6432820695555), 0], [(-83048987067969128), (-3922508334449)], [(-348644300955597038)]], [[86740057889535, (-131289744611), 0, 0, 0], [193596163060449, 43232068363, 0, 0], [579267022138048, 67217282544, 0], [2073256323799050, 61541839841], [8766133484440493]]], r := 980190373457944, ok := true }, Z3 := { p := [[[48233421028748354098068]], [[(-1131006715386520501537), 623766146687136901], [(-1131167733671577163785)]], [[27876216472793296220, (-21634967332451998), 0], [26756036387917449110, 1367644818499752], [27879992104488100934]], [[(-697035323297533039), 524840890752133, 0, 0], [(-661649466114328690), (-44436927010121), 0], [(-661645714048981326), (-14535065648540)], [(-697128382301283119)]], [[17548303076250533, (-13064734586912), 0, 0, 0], [16577437424124701, 1014857107562, 0, 0], [16383381855735591, 478847772224, 0], [16577318985466925, 229408805956], [17550629985223054]]], r := 22033011856662791, ok := true }, iE := { p := [[[24434540110638012381847]], [[(-145106111373516187553), 0], [(-568425714090139803194)]], [[1035675593427440548, 0, 0], [3378503848980267047, 0], [13968311128544973863]], [[(-8670209386838970), 0, 0, 0], [(-23713497294331381), 0, 0], [(-83048521709635582), 0], [(-348642946343639183)]], [[86751773525347, 0, 0, 0, 0], [193592282337951, 0, 0, 0], [579263187244254, 0, 0], [2073249017536909, 0], [8766108800567483]]], r := 980051000666369, ok := true }, iHu := { p := [[[48239974077592763907091]], [[(-1131153365717585059645), 0], [(-1131153365717585059645)]], [[27879839404641119083, 0, 0], [26755746355019203508, 0], [27879839404641119083]], [[(-697125972220007056), 0, 0, 0], [(-661642562501179083), 0, 0], [(-661642562501179083), 0], [(-697125972220007056)]], [[17550585912547630, 0, 0, 0, 0], [16577268866304423, 0, 0, 0], [16383306355861034, 0, 0], [16577268866304423, 0], [17550585912547630]]], r := 22032563330603004, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[13926284897532836]], [[82702151880523, 0], [323970019556719]], [[(-99143495352), 0, 0], [1922281006230, 0], [(-424554362644)]], [[847361098, 0, 0, 0], [(-2542198525), 0, 0], [(-2542198525), 0], [3628443656]], [[(-10863604), 0, 0, 0, 0], [21727208, 0, 0, 0], [(-1477), 0, 0], [21727208, 0], [(-46518508)]]], r := 27122565, ok := true }, de := { p := [[[(-142308909309160606150)]], [[341200376727107399, 0], [341200376727107399]], [[(-4374264658451225), 0, 0], [198291484919, 0], [(-4374264658451225)]], [[74773754883733, 0, 0, 0], [115239, 0, 0], [115239, 0], [74773754883733]], [[(-1437956824687), 0, 0, 0, 0], [1, 0, 0, 0], [1478, 0, 0], [1, 0], [(-1437956824687)]]], r := 302727756890, ok := true }, dde := { p := [[[(-587117171244313219059598)]], [[15053945234051782416854, 0], [15053945234051782411933]], [[(-385998595943213443099), 0, 0], [(-385998596141509429378), 0], [(-385998595943213444088)]], [[9897399895979763000, 0, 0, 0], [9897399895979504138, 0, 0], [9897399895979504167, 0], [9897399895979759271]], [[(-253779484512271528), 0, 0, 0, 0], [(-253779484512293212), 0, 0, 0], [(-253779484512277705), 0, 0], [(-253779484512293116), 0], [(-253779484512279482)]]], r := 40249235930887161, ok := true }, nJu := { p := [[[(-284617818618321212300)]], [[682400753454214799, 0], [682400753454214799]], [[(-8748529316902450), 0, 0], [396582969838, 0], [(-8748529316902450)]], [[149547509767467, 0, 0, 0], [230478, 0, 0], [230478, 0], [149547509767467]], [[(-2875913649374), 0, 0, 0, 0], [2, 0, 0, 0], [2957, 0, 0], [2, 0], [(-2875913649374)]]], r := 605455513774, ok := true }, Jd1 := { p := [[[(-1174234342488626438119196)]], [[30107890468103564833708, 0], [30107890468103564823866]], [[(-771997191886426886197), 0, 0], [(-771997192283018858756), 0], [(-771997191886426888176)]], [[19794799791959526000, 0, 0, 0], [19794799791959008277, 0, 0], [19794799791959008335, 0], [19794799791959518543]], [[(-507558969024543055), 0, 0, 0, 0], [(-507558969024586423), 0, 0, 0], [(-507558969024555410), 0, 0], [(-507558969024586231), 0], [(-507558969024558964)]]], r := 80498471861774315, ok := true }, term0 := { p := [[[25907615562461687465367906319]], [[(-1328550504622066701870702733), 0], [(-1328501096801811351996780831)]], [[51097517333726114369310365, 0, 0], [68127103378666894798146514, 0], [51094983599352743608330278]], [[(-1746913772129205986996476), 0, 0, 0], [(-2620258360771907751624931), 0, 0], [(-2620225876997890182708484), 0], [(-1746816320807152936539420)]], [[55990635695166281502022, 0, 0, 0, 0], [89581228640067342062642, 0, 0, 0], [100777537676843682234816, 0, 0], [89579562805502321468272, 0], [55987304026036967419525]]], r := 16722172514462457458738, ok := true }, r0 := { p := [[[5270990123983281938295]], [[(-107648829156279201644), 10540201879788298416131], [(-122399293648576092784)]], [[1765667512824954352, (-215201105231742238826), 5266544871526745933789], [2469622652824605341, (-244765697259240628906)], [3005781403560732815]], [[(-29186909085737818), 3528645220738950701, (-107407505555332840849), (-3554732637064177079)], [(-39523952483624843), 4937467433899545535, (-122317077738084454110)], [(-60371105168530265), 6010821858155798592], [(-74992637379139025)]], [[528587716171078, (-58318073239301170), 1758945587045843476, 192928888778908567, (-887013992083698503)], [635226049970009, (-78998892510868132), 2465178783516573927, 65752525192394254], [957089319040561, (-120702208765530799), 3003929221479727499], [1502079320100128, (-149967749159520645)], [1885039535856558]]], r := 400186021955346448, ok := true }, r1 := { p := [[[333800107389999425024861]], [[(-6698567226138867221098), 0], [(-7767827277461853310967)]], [[107740719564001509407, 0, 0], [154522560451045141053, 0], [190888257023502709082]], [[(-1760335332848518359), 0, 0, 0], [(-2432927129688461848), 0, 0], [(-3784162502258073883), 0], [(-4764467001657952985)]], [[31875353230769551, 0, 0, 0, 0], [38708484654553436, 0, 0, 0], [59082880597329115, 0, 0], [94250761481630887, 0], [119794208903506735]]], r := 95651974678494612, ok := true }, r2 := { p := [[[4261610881600676037631953303]], [[(-89238341820535280972504570), 101389163191024884156747], [(-214899762468907756578599081)]], [[1785743654094495985111326, (-1493177046345041052207), 448347474029470127], [4434827474067170231265625, (-2565277652974712781166)], [8181026939508283940328438]], [[(-38750155520288361971137), 24306497722588741118, (-73443515502064), (-609149813240235)], [(-87719192862458630474976), 36646197821014768653, (-522758521082100)], [(-167298761289333015967177), 65414665025541337564], [(-277664161779802078510114)]], [[901005140978854178350, (-462752770806507394), (-567696069653163), 12063998334415, (-67929919922583)], [1890966234085289580376, (-579076050341372670), (-204366906994071), 51487009733931], [3284813607115032268455, (-922812585547070201), (-116659211238136)], [5640953453404106686368, (-1672178099493333057)], [8849804147265491697583]]], r := 19474520311611178547602, ok := true }, r3 := { p := [[[51801473162617226368087413435]], [[(-2656477417924322733244393774), 1247115227550776021295760], [(-2656649116206488798596406902)]], [[102172100702303170578046181, (-56550340206355763587518), 1715501737234603832], [136238206084731424743918964, (-32022011049757573126188)], [102180910936762950688664086]], [[(-3493061421120289307597169), 2080076672890837115273, (-27778738200713903), (-37207855738742832)], [(-5239928308416124080038218), 1451586763383993628806, (-32481057799066813)], [(-5240041402995612251184933), 821487525332372212057], [(-3493400408441934581212993)]], [[111957027992869052411523, (-69494479611146014019), (-24648750062171074), 3487175950529135, (-3764009984114017)], [179142794211911143325421, (-53403770938886979239), (-14689080542731393), (-33956754569814589)], [201539959600101344623878, (-37237120605906710338), (-11431945635434354)], [179148575498039336316821, (-21084914546769326441)], [111968629152915525285022]]], r := 1740635321238114967774123, ok := true }, eta := { p := [[[(-4263318028159044180859666301)]], [[89280376195279700652745857, 0], [214943028163742556631944255]], [[(-1786762029250642676493146), 0, 0], [(-4435885282563817719519208), 0], [(-8182131097873119434706253)]], [[38775395929168067946571, 0, 0, 0], [87744753768251123706590, 0, 0], [167325678773952307585798, 0], [277692391384358958892665]], [[(-901640877683466559042), 0, 0, 0, 0], [(-1891600096202032177762), 0, 0, 0], [(-3285463361714620756234), 0, 0], [(-5641640866847658245443), 0], [(-8850527089422082600972)]]], r := 1723690377387386047905, 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 1266637395197952 1407374883553280 0 4611686018427387904 4611686018427387904 5764607523034234880 :=
  (RegionPosI.split_s 5188146770730811392 (RegionPosI.split_s 4899916394579099648 (RegionPosI.split_b 1337006139375616 (RegionPosI.of_check c0 q0 ok_0 1266637395197952 1337006139375616 0 4611686018427387904 4611686018427387904 4899916394579099648 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 1337006139375616 1407374883553280 0 4611686018427387904 4611686018427387904 4899916394579099648 (by decide +kernel))) (RegionPosI.split_b 1337006139375616 (RegionPosI.of_check c2 q2 ok_2 1266637395197952 1337006139375616 0 4611686018427387904 4899916394579099648 5188146770730811392 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 1337006139375616 1407374883553280 0 4611686018427387904 4899916394579099648 5188146770730811392 (by decide +kernel)))) (RegionPosI.split_b 1337006139375616 (RegionPosI.split_s 5476377146882523136 (RegionPosI.of_check c4 q4 ok_4 1266637395197952 1337006139375616 0 4611686018427387904 5188146770730811392 5476377146882523136 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 1266637395197952 1337006139375616 0 4611686018427387904 5476377146882523136 5764607523034234880 (by decide +kernel))) (RegionPosI.split_s 5476377146882523136 (RegionPosI.of_check c6 q6 ok_6 1337006139375616 1407374883553280 0 4611686018427387904 5188146770730811392 5476377146882523136 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 1337006139375616 1407374883553280 0 4611686018427387904 5476377146882523136 5764607523034234880 (by decide +kernel)))))

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

View graph