Prove2Me

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

Definition
CK_CKLaneC_RSC2_S01_0262

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

general-courtade-kumartransplant

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

Definition code
import Definitions.Def_CK_CKLaneC_RSC2_S01_0262_part00

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

namespace CKLaneC.RSC2.S01_0262
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def q4 : Cert := { V0 := [[[454128445770565837]], [[(-23756871965663734), 64818780763923741], [1201683724524931]], [[214229954270525, (-3384939984052523), (-12139935484233)], [(-61980767472087), 171218975848697], [(-13987994594816)]], [[(-2154511472344), 30058687703607, 1903624609201, (-575112986815)], [522969075159, (-8784101847059), (-96290231888)], [723959994577, (-1994235938198)], [244573072039]], [[23331222885, (-290485896481), (-116540335778), 89870069642, 318371624], [(-5495102399), 70431886244, 15019690315, (-4545859413)], [(-6214534306), 102788695777, 866591497], [(-12672070433), 34874068029], [(-4966294965)]]], r0 := 1574983334464, V1 := [[[518934511813360180]], [[(-27139818540498502), 0], [1372801868605173]], [[244166650181358, 0, 0], [(-70749145794295), 0], [(-15981322953065)]], [[(-2441145328905), 0, 0, 0], [592447007842, 0, 0], [826606688941, 0], [279432581701]], [[26237465731, 0, 0, 0, 0], [(-6116213729), 0, 0, 0], [(-7054892533), 0, 0], [(-14469908788), 0], [(-5674234307)]]], r1 := 421688172989, V2 := [[[18444728693409804405]], [[(-19721061339475), 6659585639], [(-57568001178274)]], [[14078859052, (-223768999), (-21092)], [(-564834036548), 382291531], [243449588]], [[(-148270092), (-2903277), 1624, 0], [441836477, (-12836980), (-1817)], [(-23519769), 5516183], [(-1850272)]], [[1991954, 2365, (-22), 0, 0], [(-4620141), (-167140), 140, 0], [677152, (-184959), (-52)], [176671, 633], [23911]]], r2 := 1351115352, V3 := [[[18445166264119800185]], [[(-38482710658659), 10403958680], [(-45080573918597)]], [[11098496, (-196317595), (-65810)], [(-1099500371684), 597185449], [(-8615056)]], [[1657, (-11098513), 4094, 0], [637388, (-11256445), (-5668)], [161983, 8615218], [(-966)]], [[(-12), (-1655), 17, (-1), 0], [104, (-637390), 352, 0], [9206, (-161994), (-163)], [13, 967], [5]]], r3 := 5199239160, Vm := [[[18444728700668829925]], [[(-19721336955930), 0], [(-57567582730729)]], [[14077075879, 0, 0], [(-564849998269), 0], [249542636]], [[(-148268418), 0, 0, 0], [441736655, 0, 0], [(-23754500), 0], [(-1848931)]], [[1991974, 0, 0, 0, 0], [(-4620033), 0, 0, 0], [675791, 0, 0], [176593, 0], [23904]]], rm := 124737071 }
noncomputable def w4 : Wit := { Z0 := { p := [[[454327089573086471]], [[(-23788058183831063), 64903869939012353], [1203261203700445]], [[216144091588526, (-3398294026261581), 0], [(-62227324951743), 171894457671492], [(-14002179007703)]], [[(-2215366120652), 30877727369789, 0, 0], [538002067020, (-8889617850249), 0], [726182933619, (-2000311286815)], [244800561612]], [[24567902297, (-316480874379), 0, 0, 0], [(-5968708480), 76857438145, 0, 0], [(-6350613483), 103740419088, 0], [(-12707743430), 34971508801], [(-4970676717)]]], r := 380148553996, ok := true }, Z1 := { p := [[[519230959512098824]], [[(-27186352210092643), 0], [1375155661371938]], [[247021818958315, 0, 0], [(-71116942801992), 0], [(-16002490294518)]], [[(-2531846995031), 0, 0, 0], [614859505166, 0, 0], [829923352707, 0], [279772070414]], [[28077602625, 0, 0, 0, 0], [(-6821381120), 0, 0, 0], [(-7257843980), 0, 0], [(-14523135348), 0], [(-5680773391)]]], r := 105519679169, ok := true }, Z2 := { p := [[[21640421741431012795482]], [[(-192200126197005787360), 64903869939012353], [(-561053834827136531339)]], [[1939841403899553681, (-3398294026261581), 0], [5019324970354270302, 171894457671492], [15362976152908760619]], [[(-21190365752882397), 30877727369789, 0, 0], [(-50325274548730704), (-8889617850249), 0], [(-137817033557669935), (-2000311286815)], [(-427279737453978226)]], [[248989731668966, (-316480874379), 0, 0, 0], [542871480618612, 76857438145, 0, 0], [1378478464636330, 103740419088, 0], [3839294778230576, 34971508801], [11971192677105807]]], r := 2133451010740169, ok := true }, Z3 := { p := [[[27030780266520278850717]], [[(-599723917604129059804), 162137821150434446], [(-702546622510865758378)]], [[14031802471633292260, (-10646478319313412), 0], [15739825546719175682, 418871426727031], [19255404348158268854]], [[(-333333890585459142), 240551567782694, 0, 0], [(-369619936654872889), (-26580429707822), 0], [(-432983021699876690), (-4901625291098)], [(-535839037593242845)]], [[7975568579629942, (-5658398916759), 0, 0, 0], [8799918248022553, 551548623524, 0, 0], [10182421226199767, 313433836677, 0], [12075631267636676, 85854597377], [15018698254317226]]], r := 14172709635728438, ok := true }, iE := { p := [[[21642857047507420085076]], [[(-192201999874339846826), 0], [(-561047385048137814042)]], [[1939884262299650976, 0, 0], [5019324157310689995, 0], [15362901097750477096]], [[(-21190979687791227), 0, 0, 0], [(-50325131609574715), 0, 0], [(-137817013094870712), 0], [(-427278425262147965)]], [[248998408640870, 0, 0, 0, 0], [542869092998384, 0, 0, 0], [1378476886628224, 0, 0], [3839294356889977, 0], [11971166033043657]]], r := 2133303087391663, ok := true }, iHu := { p := [[[27033254630660444176394]], [[(-599729464778123000695), 0], [(-702540230168657880638)]], [[14031992083722970135, 0, 0], [15739825316778633150, 0], [19255329545094043847]], [[(-333338787322660257), 0, 0, 0], [(-369619619236683333), 0, 0], [(-432982982533119692), 0], [(-535837727377430696)]], [[7975690123560964, 0, 0, 0, 0], [8799909099505379, 0, 0, 0], [10182417146670062, 0, 0], [12075630367277233, 0], [15018671621014021]]], r := 14172073759775209, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[15722617682776237]], [[139626600834444, 0], [407577128919268]], [[(-169272785053), 0, 0], [3592749498860, 0], [(-594881629740)]], [[1376142647, 0, 0, 0], [(-4836572129), 0, 0], [(-5665698780), 0], [5665214170]], [[(-16782227), 0, 0, 0, 0], [39318362, 0, 0, 0], [(-5910), 0, 0], [53954421, 0], [(-80931630)]]], r := 51983067, ok := true }, de := { p := [[[(-133859750945441287610)]], [[324562980315796883, 0], [380202348369933491]], [[(-3957915845777861), 0, 0], [396598914636, 0], [(-5431229825920478)]], [[64356355333620, 0, 0, 0], [413703, 0, 0], [484624, 0], [103451996873433]], [[(-1177250402444), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-2216828504430)]]], r := 378528397787, ok := true }, dde := { p := [[[(-311157898649249857383973)]], [[7588892463364328479187, 0], [8889845457083927646815]], [[(-185094938469411776791), 0, 0], [(-216825499746498280876), 0], [(-253995584952719365983)]], [[4514510694375574938, 0, 0, 0], [5288426813410536382, 0, 0], [6195014267138052613, 0], [7257016712934283858]], [[(-110110016935970128), 0, 0, 0, 0], [(-128986019839289041), 0, 0, 0], [(-151097908954600395), 0, 0], [(-177000407632535982), 0], [(-207343334655255132)]]], r := 25617859057088596, ok := true }, nJu := { p := [[[(-267719501890882575219)]], [[649125960631593767, 0], [760404696739866983]], [[(-7915831691555722), 0, 0], [793197829272, 0], [(-10862459651840956)]], [[128712710667241, 0, 0, 0], [827406, 0, 0], [969248, 0], [206903993746867]], [[(-2354500804887), 0, 0, 0, 0], [2, 0, 0, 0], [11823, 0, 0], [2, 0], [(-4433657008859)]]], r := 757056795566, ok := true }, Jd1 := { p := [[[(-622315797298499714767945)]], [[15177784926728656958375, 0], [17779690914167855293630]], [[(-370189876938823553582), 0, 0], [(-433650999492996561751), 0], [(-507991169905438731966)]], [[9029021388751149877, 0, 0, 0], [10576853626821072764, 0, 0], [12390028534276105227, 0], [14514033425868567716]], [[(-220220033871940256), 0, 0, 0, 0], [(-257972039678578081), 0, 0, 0], [(-302195817909200789), 0, 0], [(-354000815265071963), 0], [(-414686669310510263)]]], r := 51235718114177182, ok := true }, term0 := { p := [[[7276875663230009884891096309]], [[(-354946774624634466289314497), 0], [(-415780916299781651441664707)]], [[12985579965814183582593141, 0, 0], [20281345440571560713197090, 0], [17818602893303311322568644]], [[(-422290768930418712655606), 0, 0, 0], [(-741992510307418823039418), 0, 0], [(-869181556093945923213730), 0], [(-678792886719479518419542)]], [[12874635982438202033788, 0, 0, 0, 0], [24129708747554221091210, 0, 0, 0], [31799098576084813666994, 0, 0], [33111317131434300850478, 0], [24242366675150755263789]]], r := 5595882323696726891990, ok := true }, r0 := { p := [[[139024788767158625802565]], [[(-3853058096338071159262), 39665478849573075308425], [(-3612543745627081680069)]], [[79361367073407528848, (-1093493241601163150454), 2817304952938675380378], [100483244099345178932, (-1030998315543750425753)], [99007035543497264052]], [[(-1471023293605323110), 22277688824233447792, (-76003825232968365758), (-2270557520072329113)], [(-2055047365680660300), 28556286374886309067, (-73312537010384895593)], [(-2757467879194218341), 28258642911218070882], [(-2755059434091046020)]], [[26491084565520553, (-407569751782014011), 1478449033246226597, 298728855321552511, (-79828285520638520)], [37628209610614117, (-578888155337097919), 1996050829597571686, 47062043049337984], [56242093285139184, (-783994177231118456), 2010174341218253197], [76791147235839930, (-786392795456053359)], [77217614478559088]]], r := 566784364769958968, ok := true }, r1 := { p := [[[181505222293989634056458]], [[(-5022246089606812439497), 0], [(-4716805876551460236575)]], [[103101026623251400079, 0, 0], [131029149760847111407, 0], [129274627820462137434]], [[(-1903588532576286720), 0, 0, 0], [(-2672586993768196646), 0, 0], [(-3596200794512809111), 0], [(-3597371895083254968)]], [[34157999333359804, 0, 0, 0, 0], [48776382105348467, 0, 0, 0], [73168090158724107, 0, 0], [100156412685576862, 0], [100826721964972348]]], r := 75319262846479398, ok := true }, r2 := { p := [[[2683990627970262036662948353]], [[(-66665740382650825708176294), 69754848161533957914878], [(-152043472876868375227511740)]], [[1377671452930922923920195, (-1239156731562922183289), 451663911853112320], [3741820854188859428549392, (-1988218745815698760141)], [6482035527605766832134084]], [[(-28034002891550674687907), 21341963520282824440, (-220002411330876), (-5206327912588)], [(-76580959971654057972654), 34744995808620779789, (-203631935440720)], [(-158617627030479043312835), 56747478083328132384], [(-246021509268998937656667)]], [[586932350369212673153, (-380682447082621301), (-15917917277153), (-37649895319970), (-967605997497)], [1544908410916889486138, (-586966094855180710), (-205687947747634), (-3610148912692)], [3226709234457985856885, (-985191112367738262), (-249383627087395)], [5995731829913297412846, (-1620633780011898586)], [8761583482647557628948]]], r := 24369486341913299066282, ok := true }, r3 := { p := [[[14551762925983189491864227541]], [[(-709815467546846366386502054), 394678030478673637344222], [(-831505002603661765330068895)]], [[25968533967846052757239321, (-15519616764970617365263), 1793215969679433144], [40560459379743745176825520, (-11296646670055495301570)], [35635581860270759833143046]], [[(-844499894460047163370710), 522199560735967607584, 1355086982325239, (-3535019851452178)], [(-1483909976668193674820284), 444009643583619457285, (-1627076853274061)], [(-1738299349673038441624908), 322973144658079061233], [(-1357539374154165034381496)]], [[25746850939132686223996, (-16243965992007060048), (-1113209718583727), 299520121360375, (-355274644034577)], [48257083697716481980275, (-14937266853389056238), (-2789203100733611), 347280808705585], [63596052009574380680111, (-12695518988883264654), (-2857461399922679)], [66220810720975316037826, (-9232413989806160662)], [48483404546810099987124]]], r := 577968364419935744189719, ok := true }, eta := { p := [[[(-2684480970634338956902641081)]], [[66681167247115335442786934, 0], [152057350554991402145915445]], [[(-1378077654075168706641573), 0, 0], [(-3742257149373438401188903), 0], [(-6482430547484691868777536)]], [[28044160636756337019745, 0, 0, 0], [76592434216693615897404, 0, 0], [158630040997924778109187, 0], [246032769784142511524507]], [[(-587182277143547857292), 0, 0, 0, 0], [(-1545195288815415419835), 0, 0, 0], [(-3227035673505732034739), 0, 0], [(-5996085918676773920266), 0], [(-8761904716656704458724)]]], r := 2413187152029330930709, 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 := 1231453023109120, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 12393906174523604992, sh := 288230376151711744 }
noncomputable def q5 : Cert := { V0 := [[[407454750366268274]], [[(-22925080827239140), 58166858363529200], [1079771121086266]], [[201841849987001, (-3268098158657327), (-8770526676414)], [(-59952813253352), 153927396774999], [(-12564425946996)]], [[(-1978226258137), 28384828735930, 1479391501541, (-415911345852)], [491496872540, (-8509978032549), (-69679327729)], [699856290987, (-1791991643911)], [219657500488]], [[20802811637, (-267876327305), (-96120331570), 69960013818, 185268324], [(-5006088714), 66680113448, 11696411975, (-3295116085)], [(-5843005942), 99486452698, 626463085], [(-12247848290), 31332716576], [(-4460058200)]]], r0 := 1460465177087, V1 := [[[465612422482277743]], [[(-26191629687892676), 0], [1233625545937848]], [[230126046770391, 0, 0], [(-68450545041169), 0], [(-14355761457761)]], [[(-2242818970393), 0, 0, 0], [557387990027, 0, 0], [799232292100, 0], [250979694497]], [[23413782850, 0, 0, 0, 0], [(-5581404571), 0, 0, 0], [(-6638585646), 0, 0], [(-13987857660), 0], [(-5096102907)]]], r1 := 383827550279, V2 := [[[18444689306447328955]], [[(-19666463744820), 6200453027], [(-58695937903389)]], [[13234724840, (-235354573), (-17932)], [(-563120220158), 355950119], [199068293]], [[(-133476346), (-2889714), 1533, 0], [415532207, (-13503889), (-1545)], [(-20886060), 5136575], [(-1516810)]], [[1715462, 2160, (-24), 0, 0], [(-4159427), (-166327), 132, 0], [640342, (-194641), (-45)], [156980, 595], [19597]]], r2 := 1338215770, V3 := [[[18445089298742889930]], [[(-38482666245146), 9966916383], [(-47279572111585)]], [[11108172, (-240731140), (-57578)], [(-1099497820897), 572122176], [(-8254249)]], [[1569, (-11108171), 4125, 0], [637999, (-13807234), (-4959)], [198829, 8254391], [(-934)]], [[(-11), (-1567), (-2), (-1), 0], [99, (-638000), 355, 0], [9217, (-198840), (-143)], [18, 935], [5]]], r3 := 4881057110, Vm := [[[18444689313148002570]], [[(-19666746473277), 0], [(-58695551777697)]], [[13232952152, 0, 0], [(-563136579844), 0], [204686452]], [[(-133474532), 0, 0, 0], [415433055, 0, 0], [(-21126211), 0], [(-1515621)]], [[1715477, 0, 0, 0, 0], [(-4159312), 0, 0, 0], [638992, 0, 0], [156905, 0], [19591]]], rm := 123539851 }
noncomputable def w5 : Wit := { Z0 := { p := [[[407598210574810812]], [[(-22949302809578768), 58228315796401544], [1080911976258071]], [[203418923305020, (-3278471829939824), 0], [(-60144628838620), 154415996608295], [(-12574675663405)]], [[(-2029983360382), 29059846186431, 0, 0], [503905074447, (-8592089834089), 0], [701583962706, (-1796382237630)], [219821854081]], [[21846550787, (-289997622912), 0, 0, 0], [(-5409410087), 71986439206, 0, 0], [(-5955202774), 100226280386, 0], [(-12275567181), 31403122011], [(-4463223512)]]], r := 353880905628, ok := true }, Z1 := { p := [[[465826526371212357]], [[(-26227774639518591), 0], [1235327972866367]], [[232478769491452, 0, 0], [(-68736718672708), 0], [(-14371057901034)]], [[(-2319980983294), 0, 0, 0], [575891513654, 0, 0], [801810243092, 0], [251224976093]], [[24967486613, 0, 0, 0, 0], [(-6182182957), 0, 0, 0], [(-6805946027), 0, 0], [(-14029219636), 0], [(-5100826870)]]], r := 96020793039, ok := true }, Z2 := { p := [[[21263615217368273803330]], [[(-184687321482600820426), 58228315796401544], [(-551212240997905730764)]], [[1818432713024792450, (-3278471829939824), 0], [4824343543989460149, 154415996608295], [15092740262546238609]], [[(-19317982822631687), 29059846186431, 0, 0], [(-47212670103704835), (-8592089834089), 0], [(-132475429843578013), (-1796382237630)], [(-419751323303486831)]], [[219885286110473, (-289997622912), 0, 0, 0], [495624834880992, 71986439206, 0, 0], [1293603386577500, 100226280386, 0], [3690688827477106, 31403122011], [11760019689418378]]], r := 2030385973145313, ok := true }, Z3 := { p := [[[25884914729050412996640]], [[(-547355987075168969373), 141763861173231464], [(-672478271042164754738)]], [[12208920469175930858, (-9748104705725923), 0], [14360580238383602538, 367821177981380], [18428315718769867119]], [[(-276513566891507518), 209594558010257, 0, 0], [(-321503227189837778), (-24515489312396), 0], [(-394989374342266391), (-4300119861148)], [(-512772965995007643)]], [[6307891236015678, (-4698025842755), 0, 0, 0], [7297748786940781, 482995553716, 0, 0], [8855798719903116, 288624137553, 0], [11015121987399998, 75294766088], [14371206527258338]]], r := 12126819772071744, ok := true }, iE := { p := [[[21266046942747009239266]], [[(-184689030825722105129), 0], [(-551205792291761660500)]], [[1818472086318822783, 0, 0], [4824343275195928375, 0], [15092665242202314762]], [[(-19318532141582078), 0, 0, 0], [(-47212540642523215), 0, 0], [(-132475415394610785), 0], [(-419750011849296154)]], [[219892798415676, 0, 0, 0, 0], [495622722711922, 0, 0, 0], [1293601954724964, 0, 0], [3690688509517213, 0], [11759993061887635]]], r := 2030250157433437, ok := true }, iHu := { p := [[[25887378719970804876857]], [[(-547360830897501610377), 0], [(-672471877959785554552)]], [[12209083395766455685, 0, 0], [14360581175384842803, 0], [18428240978591328130]], [[(-276517599793222227), 0, 0, 0], [(-321502959477782535), 0, 0], [(-394989350209283539), 0], [(-512771657300263719)]], [[6307986884486944, 0, 0, 0, 0], [7297741299702415, 0, 0, 0], [8855795261952230, 0, 0], [11015121359266506, 0], [14371179929942449]]], r := 12126291093130666, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[16001204541542454]], [[138965505285388, 0], [414743588720967]], [[(-161399968981), 0, 0], [3573860227230, 0], [(-606213050942)]], [[1251106430, 0, 0, 0], [(-4611634527), 0, 0], [(-5665722421), 0], [5773123011]], [[(-14547748), 0, 0, 0, 0], [35745898, 0, 0, 0], [(-5910), 0, 0], [53954421, 0], [(-82473185)]]], r := 51078695, ok := true }, de := { p := [[[(-133225959926975293219)]], [[309467673370456165, 0], [380203141569417575]], [[(-3598299911052621), 0, 0], [396600569452, 0], [(-5431229824927589)]], [[55787595632441, 0, 0, 0], [413706, 0, 0], [508267, 0], [103451996873434]], [[(-973039458705), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-2216828504430)]]], r := 353473782171, ok := true }, dde := { p := [[[(-296686057208776634242672)]], [[6899366267486926691188, 0], [8476364271483938520339]], [[(-160450378636478336177), 0, 0], [(-197124751292863202611), 0], [(-242181836815386478862)]], [[3731404154336385347, 0, 0, 0], [4584296532469576821, 0, 0], [5632135739891191022, 0], [6919481051867575349]], [[(-86776840798511542), 0, 0, 0, 0], [(-106611547266741279), 0, 0, 0], [(-130979900927711827), 0, 0], [(-160918163996909156), 0], [(-197699458624778217)]]], r := 22217983346769359, ok := true }, nJu := { p := [[[(-266451919853950586438)]], [[618935346740912331, 0], [760406283138835150]], [[(-7196599822105241), 0, 0], [793201138904, 0], [(-10862459649855177)]], [[111575191264882, 0, 0, 0], [827412, 0, 0], [1016534, 0], [206903993746868]], [[(-1946078917410), 0, 0, 0, 0], [2, 0, 0, 0], [11823, 0, 0], [2, 0], [(-4433657008859)]]], r := 706947564337, ok := true }, Jd1 := { p := [[[(-593372114417553268485343)]], [[13798732534973853382376, 0], [16952728542967877040679]], [[(-320900757272956672354), 0, 0], [(-394249502585726405221), 0], [(-484363673630772957723)]], [[7462808308672770695, 0, 0, 0], [9168593064939153643, 0, 0], [11264271479782382044, 0], [13838962103735150698]], [[(-173553681597023083), 0, 0, 0, 0], [(-213223094533482558), 0, 0, 0], [(-261959801855423654), 0, 0], [(-321836327993818312), 0], [(-395398917249556433)]]], r := 44435966693538710, ok := true }, term0 := { p := [[[6615740693692548652038101116]], [[(-307688168280439821292703488), 0], [(-378004276474794090690394334)]], [[10733067520264730279146776, 0, 0], [17581002880396045641085336, 0], [16199639776396302709902525]], [[(-332804563797853527827595), 0, 0, 0], [(-613283921708455184695153), 0, 0], [(-753454721099585412571146), 0], [(-617118781937023590280253)]], [[9674486190562426852201, 0, 0, 0, 0], [19016449100342293965313, 0, 0, 0], [26283107754551615521022, 0, 0], [28702716405369081308757, 0], [22039734660567201253999]]], r := 4600957506425289662395, ok := true }, r0 := { p := [[[131624758826415839457028]], [[(-3552454141590266715048), 37564454537988259774340], [(-3419506726265420984263)]], [[71134464051331426185, (-1009051321859325268477), 2671013610753683380353], [92694160834103950467, (-976120254874089030191)], [93709148183247670121]], [[(-1277042229116908217), 19996372481590702340, (-70383056728558547481), (-1733032564004552646)], [(-1844383279093668383), 26360921839396938147, (-69471205405817551398)], [(-2544244748665469933), 26751886697571586233], [(-2607512279584327905)]], [[22163421403480076, (-354433904646387224), 1335086051846236497, 240624177994408916, (-61117868676551123)], [32736092722852616, (-520143364389955632), 1847803975400647812, 35885791655906475], [50501885762549728, (-723830722598613483), 1904524294802679536], [70862075564812136, (-744419210133530962)], [73079798480873322]]], r := 500905667596035262, ok := true }, r1 := { p := [[[171858432892482484207096]], [[(-4631639514332488225808), 0], [(-4465061032123096919618)]], [[92452275794111829210, 0, 0], [120897711277127247135, 0], [122364625275608753973]], [[(-1653410183934684530), 0, 0, 0], [(-2399451526007120194), 0, 0], [(-3318764154707006566), 0], [(-3404912851293233747)]], [[28591174149013592, 0, 0, 0, 0], [42453104923146665, 0, 0, 0], [65721507217418010, 0, 0], [92440274897173573, 0], [95429122447103758]]], r := 65735961655192070, ok := true }, r2 := { p := [[[2555954561560329489134886455]], [[(-61473648295954577690374902), 67358970925631506245733], [(-144854288537677105837029605)]], [[1222598635469262648219828, (-1158133752739131664604), 451824010489853106], [3453060501950828501321067, (-1920996638011987092538)], [6177209761790710062145809]], [[(-23806049458906819331569), 19221356064989610993, 3874840797304, (-4868761870839)], [(-68030559108207761401737), 32515060953499684758, 2305778014286], [(-146446954572607094978701), 54841113620597424393], [(-234497149796591941324498)]], [[474944773275520229866, (-328452132383698031), (-28931042796596), (-34730378274091), (-910274574011)], [1313353401689276219105, (-529707206950519320), (-231296065679797), (-3382505536297)], [2868282992809535388361, (-922505422933606666), (-224452672894032)], [5537581619863519365977, (-1566224849474022365)], [8352403319257767204898]]], r := 22305885818070287054321, ok := true }, r3 := { p := [[[13229639263011321730207202195]], [[(-615307851205190674218058782), 365604962157056642069787], [(-755955903392208742862632403)]], [[21463945985741535836549118, (-13611331275134849622795), 1795085957376656714], [35160048503426820614870592, (-10464862325741404547756)], [32397775078132265886427565]], [[(-665544350534649877679312), 435291387216738728235, (-232900624139425), (-2967577979323036)], [(-1226505284439387446938960), 389425363693558882287, 2032436687750], [(-1506853515606779820890816), 299194858382353998111], [(-1234194577954274784803303)]], [[19347141512089504490410, (-12885898391140935089), (-1126879183919447), 238425310680872, (-299807263756804)], [38031045342345492400079, (-12454020915808620291), (-1745572401354928), 288402785361280], [52564427222420303069483, (-11132915454139774580), (-2110950475909276)], [57403833517865245125041, (-8552390133660742589)], [44078240726885524831635]]], r := 468263926584574037126463, ok := true }, eta := { p := [[[(-2556415597844022620886491078)]], [[61487564723416547241786484, 0], [144867337338070377972118659]], [[(-1222949426225312297665311), 0, 0], [(-3453454126998740613269107), 0], [(-6177581196579085934810000)]], [[23814432014617739575223, 0, 0, 0], [68040469475129869606992, 0, 0], [146458155112023285633626, 0], [234507738089631044905552]], [[(-475141568742994357246), 0, 0, 0, 0], [(-1313590299899474300842), 0, 0, 0], [(-2868564982394160262351), 0, 0], [(-5537901093090659388276), 0], [(-8352705483650057717692)]]], r := 2228061353357907732095, 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 1125899906842624 1266637395197952 13835058055282163712 18446744073709551616 11529215046068469760 12682136550675316736 :=
  (RegionPosI.split_b 1196268651020288 (RegionPosI.split_s 12105675798371893248 (RegionPosI.split_b 1161084278931456 (RegionPosI.of_check c0 q0 ok_0 1125899906842624 1161084278931456 13835058055282163712 18446744073709551616 11529215046068469760 12105675798371893248 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 1161084278931456 1196268651020288 13835058055282163712 18446744073709551616 11529215046068469760 12105675798371893248 (by decide +kernel))) (RegionPosI.split_b 1161084278931456 (RegionPosI.of_check c2 q2 ok_2 1125899906842624 1161084278931456 13835058055282163712 18446744073709551616 12105675798371893248 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 1161084278931456 1196268651020288 13835058055282163712 18446744073709551616 12105675798371893248 12682136550675316736 (by decide +kernel)))) (RegionPosI.split_s 12105675798371893248 (RegionPosI.of_check c4 q4 ok_4 1196268651020288 1266637395197952 13835058055282163712 18446744073709551616 11529215046068469760 12105675798371893248 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 1196268651020288 1266637395197952 13835058055282163712 18446744073709551616 12105675798371893248 12682136550675316736 (by decide +kernel))))

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

View graph