From 0e63ddd2b854895ebfa66ee9bf5c947c2ff89f84 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:37:21 -0700 Subject: [PATCH 01/30] Add Geode5 CRT certificate proof layer --- proofs/geode5/Geode5CRT.lean | 141 +++++++++++++++++++++++++++++++++++ 1 file changed, 141 insertions(+) create mode 100644 proofs/geode5/Geode5CRT.lean diff --git a/proofs/geode5/Geode5CRT.lean b/proofs/geode5/Geode5CRT.lean new file mode 100644 index 00000000..0aafcd9d --- /dev/null +++ b/proofs/geode5/Geode5CRT.lean @@ -0,0 +1,141 @@ +/- +Copyright 2026 Dominic Dabish. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5 +import Mathlib.Data.Nat.ChineseRemainder + +/-! +# CRT certificate layer for the five-dimensional Geode computation + +This module formalizes the exact Chinese-remainder and uniqueness layer from the +computational certificate for `G(1000,1000,1000,1000,1000)`. + +It deliberately separates the already-checkable arithmetic certificate from the +remaining mathematical bridge: proving that the five-state moment recurrence +computes `geode5Diagonal`. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +open scoped Function + +private def parseNat (s : String) : ℕ := + s.trim.toNat?.getD 0 + +private def parsePair (line : String) : ℕ × ℕ := + match line.trim.splitOn " " with + | p :: r :: _ => (parseNat p, parseNat r) + | _ => (0, 0) + +/-- The exact 8,367-digit candidate value from the certificate package. -/ +def answerValue : ℕ := + parseNat (include_str "data/G5_1000.txt") + +/-- The rigorous hyper-Catalan upper bound used in the certificate. -/ +def upperBound : ℕ := + Nat.factorial 20002 / + (Nat.factorial 15002 * Nat.factorial 1001 * Nat.factorial 1000 ^ 4) + +/-- The 480 `(prime, residue)` pairs used for the CRT reconstruction. -/ +def residuePairs : List (ℕ × ℕ) := + ((include_str "data/residues_480.txt").trim.splitOn "\n").map parsePair + +/-- Product of all 480 moduli. -/ +def certificateModulus : ℕ := (residuePairs.map Prod.fst).prod + +theorem residuePairs_length : residuePairs.length = 480 := by + native_decide + +/-- The stored moduli are pairwise coprime. -/ +theorem residueModuli_pairwise_coprime : + residuePairs.Pairwise (Nat.Coprime on Prod.fst) := by + native_decide + +/-- Every stored residue is in the canonical interval for its modulus. -/ +theorem residueValues_canonical : + ∀ pr ∈ residuePairs, pr.2 < pr.1 := by + native_decide + +/-- The proposed exact answer has every residue recorded in the ZIP certificate. -/ +theorem answer_modEq_residue : + ∀ pr ∈ residuePairs, answerValue ≡ pr.2 [MOD pr.1] := by + native_decide + +/-- The hyper-Catalan upper bound is strictly below the CRT modulus. -/ +theorem upperBound_lt_certificateModulus : + upperBound < certificateModulus := by + native_decide + +/-- The proposed answer lies below the rigorous upper bound. -/ +theorem answerValue_lt_upperBound : answerValue < upperBound := by + native_decide + +/-- +Any natural number with the 480 certified residues is congruent to `answerValue` +modulo the product of all 480 moduli. +-/ +theorem modEq_answerValue_of_residues (z : ℕ) + (hz : ∀ pr ∈ residuePairs, z ≡ pr.2 [MOD pr.1]) : + z ≡ answerValue [MOD certificateModulus] := by + apply (Nat.modEq_list_map_prod_iff residueModuli_pairwise_coprime).2 + intro pr hpr + exact (hz pr hpr).trans (answer_modEq_residue pr hpr).symm + +/-- +CRT uniqueness below the rigorous Geode upper bound. + +This is the final arithmetic step of the certificate: once a nonnegative +candidate is proved to satisfy the stored residues and the hyper-Catalan bound, +it must equal the 8,367-digit answer. +-/ +theorem eq_answerValue_of_residues_of_lt_upperBound (z : ℕ) + (hz : ∀ pr ∈ residuePairs, z ≡ pr.2 [MOD pr.1]) + (hzlt : z < upperBound) : + z = answerValue := by + exact (modEq_answerValue_of_residues z hz).eq_of_lt_of_lt + (hzlt.trans upperBound_lt_certificateModulus) + (answerValue_lt_upperBound.trans upperBound_lt_certificateModulus) + +/-- +The exact remaining bridge needed to discharge the benchmark theorem from the +ZIP certificate. + +The recurrence formalization must supply: +1. nonnegativity of `geode5Diagonal 1000`; +2. the hyper-Catalan upper bound; +3. all 480 modular residue equalities. +-/ +theorem geode5_1000_of_certificate + (hnonneg : 0 ≤ geode5Diagonal 1000) + (hbound : Int.toNat (geode5Diagonal 1000) < upperBound) + (hres : ∀ pr ∈ residuePairs, + Int.toNat (geode5Diagonal 1000) ≡ pr.2 [MOD pr.1]) : + geode5Diagonal 1000 = (answerValue : ℤ) := by + have hnat : + Int.toNat (geode5Diagonal 1000) = answerValue := + eq_answerValue_of_residues_of_lt_upperBound _ hres hbound + calc + geode5Diagonal 1000 = Int.toNat (geode5Diagonal 1000) := by + symm + exact Int.toNat_of_nonneg hnonneg + _ = answerValue := by exact_mod_cast hnat + +#print axioms residueModuli_pairwise_coprime +#print axioms answer_modEq_residue +#print axioms upperBound_lt_certificateModulus +#print axioms geode5_1000_of_certificate + +end Arxiv.«2508.10245».Geode5Proof From 60f67aaff3f1f7124dc8dc2dea46d2d190b095a9 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:37:55 -0700 Subject: [PATCH 02/30] Add exact Geode5 answer certificate --- proofs/geode5/data/G5_1000.txt | 1 + 1 file changed, 1 insertion(+) create mode 100644 proofs/geode5/data/G5_1000.txt diff --git a/proofs/geode5/data/G5_1000.txt b/proofs/geode5/data/G5_1000.txt new file mode 100644 index 00000000..e41f2460 --- /dev/null +++ b/proofs/geode5/data/G5_1000.txt @@ -0,0 +1 @@ +365748434524060420565341191418654035153093345047303783863321941234714357005274510091695043326291433896815009287356974254576199183403926921350091688255887764917087847360995400732815601275565279907943016696695763198323072394104223351197579968896793624226966218668592110073855223192255824949502947311075317507207467133695072481956448695677062027304623371865102281773757750416497171235088097157904633986730991493981263610254879690840048844232237080038977625113850676812545275129422901410786261133056866332624619279299741705167724961445502425269344610928606256920975730087331788537471255085914697416542027784590310858073060188927092394978695295518806710309201279267788927682926003142274346386308076090477863762849560631542873996981189410238181645140262262381912524825278718545928133677943484236628240528536564479695511654098433631182238117143439496420818018128898951252406950438617862284939234296348471802447279438448298635038053228152445071037673412833339983466262402253018598345250211945008271488511967165694840330912085684089854290593515279395572394474589900146309777546388461593186992782496795823942745650720597946101305594883553958542416786083137108891345329699823630769885576631430536719506331451190162099494225677965686195306941106483324967500815623856075582547366199184942038058879986704094769176519719525881884508035166001139225178320806568724340660257041729099479505556708026972686860576538486477365657708327904785772566469392829283127214240157198026474806097547883434825050291111846236780740764083467347894688005141693302725365798212641782345413995138282415744168683324607128858388980112354393378291765175613784647428960522563617963332893240810337116109696788123054723245194340428893297094897722668799272894552164649642771942074586113083243442799514173669802294213766376210316100973771870760796368853150133386138418015262343661817267421322391876201381577508629168479981018888118617057476549989512087191160738998311881678230252795637202771488210373875632919160207940094496975931002860934897598694357571147118918213119935851450539250320462889379581638211058112746004079145309443127832816036695548474340881621366472606562542129067415412286779542413722359805742404136199499637113830752133402755216826003751862149154937464963905326758724914122427994537570979399178799172588564360217780854363832718136240168081340424657124519317692386548904471742055128048137889544809004572154938633518040076816252482236109003911905254898897796327001386483447590140477627916756295634103683817545707724656377821289392500285446873657403755212083740760001156102179628967330722631760078916283550886539168661462048503714615162775147142250953784481616233378376572117766544511960869177009125897715476342372219664688439675838463527895976832645673550825306889058639598844800350744139397707048395913713848757918519489286529523160137182969746468034096721600890185939336245513272667675246186185926316381031528478601188067962638948179095261688761961246077087199368875003157421206402171726656612378430222400287707033826001537857497253462639990883299479941110653415451910496160358725036247417172655104933339562352108651341637017978874764952559793174116996325847210995368189560798006407055390046243250158677567133969750969639342676589317201407006033113672075304582185131595864668370393180913989104248256527546214975679820982363574284070344620115636814380378652041728853860503955865875353683519073158215020899500147147619840344642577019574567248757661193560297399363467330881747175054113209996009724233515733945482142426054248804920240524178277028984360594959669353218792955219483842625593169799880363551727827121819495463826379553117579785236387726375447708813574324359168209306428276220518704872519722627572941787369784206110060003401302222284509178878227063086070790789713232862916512296857001145051149764753968446590434151836202362722845434729971266359448978266256924250363704610741026835710341192913650080249456317149104352923534915071524080559737531181832940357305051665536330962094045753299534845184628485582919786777833113688424839985093824271760122979469168619857254435602602241164893496339510908169714864006957560294308664387839379958369757192036995224811581289097865317083436378234858743142527559681163976168431838867678041288490265225734632085615830366812282712130412206525548484350818641099986679546060774720380601890087711999364208913715561424597469719448013573719115508361626942382528898974458387238018108210429840660311717595472478166172162272727667599982732252384754304668844300063278347457070731109763533825891286554328819888142955126910963255487882531379066134631178213578003820226167988163770505643008145050496365280844417735407120744896917982113434955616688819110711901037356399605380946944897683943991144076461447917533782714175634510442820506468643842969099540944516200061688575045195407953014319712244216715702855271948207883001876450608829681440569033698887412527409879688736133881947125500629725266275330833752401565625674335407413128859772838636763875290464487464291642202948618574333230102022925554119544097512319426454506799031648943827768209628367702151215978646672545857853532904219615189162533888187394347534145234605909893036942645675186416311403483503061464059329798759357538250243221691939041372085667738059245494380382884404425735028802095815740457592336932664077122744345285816034367898527528789168515449897624525313876193591738646087902233418592243935993087558636595742877995886077518676621354675806489860812181535116846937306984089243894454459334732772363527055790040687830362595410738894881824330955121615896108739943873629876967934754148429452433696974323633397721325370081662891786377517595172897863046439453137076463069110350166758774782674984077329725174971512824572166316102991442961436604975568559175025113100908559167880697724476480421965081245992718220963563984723244859303110817995812671326108356967299412392337898546048303627355187666297973150679702054519723162282854009067661100093027326941136279113359688028351962069544623044568012171949905556579592481615991401073469944461775736207353449091127382720342467691978170772974473509076043803641290800457063935143729424403444579564356851577897975089092093672170872108165916662478213994365134524699916483876302054115825852854787169172699089589369172612073290438583163507929243868904405877613262819075135700362457739195595529800115646108509177659988511072003308245302240007714026480840425318378253153912280170022123930501400577311548364454291523307009815329616206994159450601932869198638222303325706139154202607426948048415821031055626954369150879809887837463568029184245107361167404169487393784963703351180820752932516770391498946376680871913487116217815521143269895863970437740485602390776241343209228340805033982630655466255219808996677114469651241470605126392332166813089281604699766304357779519173093624831127237490186015702800464495954294092153533054636381658662193229973570585449889542686342507048175845478724902516915133230723634580635520194311008092252120920822272059905370628966919918184162285959613058885465265856030343478627758806627061923098642409902783298925277605948694323390958150226234113490800243007514199858101332695237231577522494474655146899696975169059585862556303128275168286174386233000338173591931573601303997032588915357259987961093812713845618617653590794897232810807556039996398039607485067693035998907424325893450575249529134600586132023466054019438845903932852106429605651374136278068144882436624430410350591844122169986853782817091934714399090094804497710835313837389657077388589733651213595566240568499031332609155580597686464508748558634655150933209822558750387438901612357527028787920671189931878260104476396770554989436967543853512892018672279873199690599317043556767155616445881990282180991497099953693013355480134398183449943517595166201433787457599667985568948287261452809484235608227639512713287894273723623900218093620360413774180028604637846032148910210219632475385518258362824160102070275642537533248002704267325661830532676456800524223438932727152361892846713954358082028863463734840054712361713538608165265829915390821390190163396083665445135497730684559067226246174032097806851333539040863718826108170814860245563387372783661592107767933923667634429543854415243019623830548473846255966387897879853265167222162492682471358437580544358590888719040253053806255224993801829115272752236508299632842726450012209182908642505837098481476217252638288912192213507850240000 From 5b0251e1e3a26110828c94eb44610d3c997c34f8 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:38:51 -0700 Subject: [PATCH 03/30] Add 480-prime Geode5 residue certificate --- proofs/geode5/data/residues_480.txt | 480 ++++++++++++++++++++++++++++ 1 file changed, 480 insertions(+) create mode 100644 proofs/geode5/data/residues_480.txt diff --git a/proofs/geode5/data/residues_480.txt b/proofs/geode5/data/residues_480.txt new file mode 100644 index 00000000..30ee7931 --- /dev/null +++ b/proofs/geode5/data/residues_480.txt @@ -0,0 +1,480 @@ +576460752303404051 464097493913787811 +576460752303404071 381024947013304639 +576460752303404149 268886939405040860 +576460752303404153 542518510133990808 +576460752303404201 321832442288009989 +576460752303404233 317762017606548621 +576460752303404239 432895773127122670 +576460752303404249 347648392279077143 +576460752303404263 318888212512120314 +576460752303404327 83010383064440071 +576460752303404401 59413508097640909 +576460752303404453 333144209960710305 +576460752303404461 147426735514109968 +576460752303404471 25286254236701454 +576460752303404509 430265643073214884 +576460752303404621 235338725221372520 +576460752303404743 446110571278676186 +576460752303404767 547715388865485977 +576460752303404807 337207397092760801 +576460752303404873 79925328467556130 +576460752303404953 399423692346560208 +576460752303404999 251917581811363593 +576460752303405037 45708250431303177 +576460752303405143 434802209597847355 +576460752303405163 381774336029074257 +576460752303405173 263000543297050997 +576460752303405199 539038175523347886 +576460752303405251 44856114672960402 +576460752303405259 487229948055286498 +576460752303405383 101442584339987935 +576460752303405433 554141464713327343 +576460752303405479 172757478989527552 +576460752303405527 264313798127180699 +576460752303405611 171411785509137169 +576460752303405679 319389537078550440 +576460752303405737 259718828276638253 +576460752303405859 427841125445229370 +576460752303405869 205572338445797967 +576460752303405913 528430680982507806 +576460752303405929 37788253145621235 +576460752303405989 46526905586775334 +576460752303406049 135642933141855203 +576460752303406121 257932580294861801 +576460752303406127 263682581218300953 +576460752303406141 483761359466353003 +576460752303406213 193380543475513209 +576460752303406279 240802491358718263 +576460752303406357 485920364771805106 +576460752303406511 418952875103533956 +576460752303406519 121807651296867569 +576460752303406543 155789284622804679 +576460752303406637 113941511266945962 +576460752303406703 423775253803611224 +576460752303406723 453354496407190334 +576460752303406757 77256447081777856 +576460752303406819 570243953182945331 +576460752303406849 285777493451618435 +576460752303406879 381349454202388526 +576460752303406897 241395062229700184 +576460752303406909 24929568354249952 +576460752303407009 531193665398713010 +576460752303407039 446193012261325495 +576460752303407057 53391207846716536 +576460752303407093 555401413927700096 +576460752303407137 303974349073739059 +576460752303407291 456251134686102443 +576460752303407317 486254889058120273 +576460752303407359 536657326415372079 +576460752303407429 291277037232690561 +576460752303407437 91545887229234853 +576460752303407467 350491659759600497 +576460752303407539 207086633975409709 +576460752303407561 497546996950250653 +576460752303407567 528304315472885477 +576460752303407603 119499461635260449 +576460752303407627 232254604821974458 +576460752303407659 203884348729800986 +576460752303407677 574094296155271825 +576460752303407689 89589627314683236 +576460752303407711 443883120270358048 +576460752303407749 194153215266945118 +576460752303407813 444412554537515929 +576460752303407927 231369076319946026 +576460752303407953 26845241444370490 +576460752303408001 290594145673408842 +576460752303408013 559662619606092501 +576460752303408101 402176744507575038 +576460752303408109 442619147536712547 +576460752303408173 293695460502299504 +576460752303408209 370106636757583647 +576460752303408229 551215187397589555 +576460752303408257 343857194897958107 +576460752303408263 220253633037683167 +576460752303408277 291891016407904303 +576460752303408289 290506509794539546 +576460752303408347 256673129005909247 +576460752303408373 272549954243411679 +576460752303408391 366602065623509817 +576460752303408403 77137692405133319 +576460752303408457 296803570050408792 +576460752303408523 226014876327013485 +576460752303408529 540950927799810187 +576460752303408589 57147165098438621 +576460752303408593 277628745279963985 +576460752303408607 323843920579944041 +576460752303408613 249696129007148215 +576460752303408619 544108855210544456 +576460752303408641 53284062407449390 +576460752303408659 434175028781854485 +576460752303408697 96963687337975150 +576460752303408727 330444769740579992 +576460752303408767 276828727788585944 +576460752303408839 7436410635869113 +576460752303408887 536592176118730336 +576460752303408901 479609260746645748 +576460752303408967 163966172405172137 +576460752303408983 105342656576208263 +576460752303409021 484167149394139703 +576460752303409063 374966192085428810 +576460752303409079 121222426957300020 +576460752303409093 409521291983033797 +576460752303409109 54790754808759330 +576460752303409123 268954321825939940 +576460752303409249 563148613117403756 +576460752303409279 214341757312937765 +576460752303409283 459020396477087439 +576460752303409289 572409332369202790 +576460752303409313 368481101732690543 +576460752303409403 411248917698935222 +576460752303409411 575775323695136285 +576460752303409451 366695933078987488 +576460752303409469 322913145000939736 +576460752303409481 545706171395932448 +576460752303409619 389695296175496217 +576460752303409669 404180950092538678 +576460752303409723 225247646295375266 +576460752303409747 275003702995766848 +576460752303409777 309481600764942004 +576460752303409789 321292861198822022 +576460752303409811 415860327559421424 +576460752303409837 168247769093014147 +576460752303409843 509138568432314522 +576460752303409877 255309327625895293 +576460752303409933 541279559405797061 +576460752303409979 384898842543329500 +576460752303409997 207545946307707405 +576460752303410059 522852654396758934 +576460752303410087 244144750054709433 +576460752303410167 332756515327715655 +576460752303410189 27047282860311275 +576460752303410197 249137315312602765 +576460752303410291 173825491152768172 +576460752303410333 518143861163886486 +576460752303410341 435645856314395186 +576460752303410363 494365080088284030 +576460752303410417 61991277525226504 +576460752303410423 319401463378430491 +576460752303410453 12698643868392680 +576460752303410473 189718694686008191 +576460752303410519 44338441616600534 +576460752303410627 575252396220862571 +576460752303410651 210194228511008223 +576460752303410659 36277126086912272 +576460752303410701 150391662179434574 +576460752303410743 478830611692845978 +576460752303410809 469679977170439446 +576460752303410813 468091837413126891 +576460752303410899 365602204597172708 +576460752303410927 159559124564409867 +576460752303410941 250000434696081068 +576460752303411047 69064825306883548 +576460752303411067 293343028671073801 +576460752303411089 373394587152552468 +576460752303411169 35289886870956627 +576460752303411187 203317480784201505 +576460752303411233 261569798936825333 +576460752303411293 141838584840808504 +576460752303411323 179700823800081428 +576460752303411361 18220539468460855 +576460752303411383 28761783574089353 +576460752303411403 225527055543326270 +576460752303411473 335523776534951895 +576460752303411487 12895613157804443 +576460752303411497 571639309728751005 +576460752303411511 507429901507570623 +576460752303411587 550107981503190366 +576460752303411607 545790809789570538 +576460752303411611 73163835131371198 +576460752303411641 182935682324339388 +576460752303411671 134292367812514729 +576460752303411683 337074955315698694 +576460752303411697 340248308323815712 +576460752303411727 56158968093042634 +576460752303411751 317630586230346695 +576460752303411821 283482430076090071 +576460752303411839 318378714610785459 +576460752303411853 405061144371406057 +576460752303411887 21628088023711014 +576460752303411907 449012966355145393 +576460752303411919 116905120007592993 +576460752303411977 104744884696530027 +576460752303412007 500024858389627980 +576460752303412043 46803456748411686 +576460752303412091 302806318262727181 +576460752303412117 433462661661079766 +576460752303412139 151032046636472494 +576460752303412231 529309225055936321 +576460752303412247 540600346058751446 +576460752303412267 269475992570342970 +576460752303412279 397179773007194332 +576460752303412321 539773782149279986 +576460752303412351 269146606580324172 +576460752303412393 263142023636579861 +576460752303412573 36340798190330652 +576460752303412589 110573237698224532 +576460752303412597 527008431274669688 +576460752303412649 276478673190617125 +576460752303412693 327676399227860220 +576460752303412723 532870352097008498 +576460752303412727 368577068687599711 +576460752303412741 114647584838227961 +576460752303412751 87223575575466117 +576460752303412763 512990046926469874 +576460752303412793 352230316207189793 +576460752303412817 422431895093792152 +576460752303412831 301497851015405718 +576460752303412897 118854705939602938 +576460752303412909 279385391366011988 +576460752303412967 221905758231807122 +576460752303412973 4663698542799528 +576460752303412981 549370043418863954 +576460752303413077 3646755188469259 +576460752303413113 558389095771152071 +576460752303413137 97692456874972343 +576460752303413141 79562313627055650 +576460752303413183 354995324759933420 +576460752303413221 231119090982848663 +576460752303413231 198003285959304438 +576460752303413287 11597094871571814 +576460752303413323 94070617892942462 +576460752303413347 427842912995085731 +576460752303413407 368964199565160524 +576460752303413429 438131082996416971 +576460752303413437 177935100993729075 +576460752303413441 229726325514607128 +576460752303413489 248675261342143808 +576460752303413563 326948759632885744 +576460752303413587 212474341439887267 +576460752303413629 496836979887403481 +576460752303413749 409756639630033181 +576460752303413753 91112722679044440 +576460752303413843 290064505513938402 +576460752303413849 316472135320518559 +576460752303413911 428706165686578860 +576460752303413981 302334202376027742 +576460752303414049 393038843527496533 +576460752303414067 324991810014353599 +576460752303414071 64989493713257469 +576460752303414137 523828755430193188 +576460752303414193 110692907348029356 +576460752303414353 474372837518494436 +576460752303414421 38364548423831059 +576460752303414443 170593072578509383 +576460752303414449 214882036685427072 +576460752303414481 66387763987627429 +576460752303414557 360851547272217448 +576460752303414581 175135566803207080 +576460752303414647 466444429530257465 +576460752303414653 273422242528904360 +576460752303414731 324237169453255282 +576460752303414749 438715875611199507 +576460752303414757 394829548253801688 +576460752303414763 326293849420437481 +576460752303414799 413607952490317390 +576460752303414829 415559883077347561 +576460752303414851 432680449458200852 +576460752303414859 56584320456324393 +576460752303414863 507097108241865262 +576460752303414877 205164890902641927 +576460752303414943 1744928670907404 +576460752303414949 206194334682785380 +576460752303414959 183123477905071539 +576460752303414977 354675806750449557 +576460752303415081 49927777274347462 +576460752303415211 529716637285222620 +576460752303415223 552481514069101563 +576460752303415289 439867289838749525 +576460752303415297 226302323988116041 +576460752303415321 538458817976222098 +576460752303415351 75308010370391359 +576460752303415379 134144629395979792 +576460752303415477 214405404177733911 +576460752303415487 325369806307484297 +576460752303415517 422274066375043867 +576460752303415559 209645606553255660 +576460752303415589 225620557881152933 +576460752303415663 570407046235418890 +576460752303415669 156746731133149225 +576460752303415673 566752839418872072 +576460752303415699 228168852251577587 +576460752303415751 25269540325940659 +576460752303415871 480414036942314222 +576460752303415963 536693991422557284 +576460752303415979 66272872585154373 +576460752303416093 100567851130592293 +576460752303416243 382653693498051993 +576460752303416329 56884855022405015 +576460752303416353 314512364875537093 +576460752303416363 10855745474634645 +576460752303416399 42677005256081423 +576460752303416443 287930573088558530 +576460752303416447 313062800467865618 +576460752303416531 135532945590578894 +576460752303416681 127632186604156656 +576460752303416699 318601201136378634 +576460752303416741 431627445293353366 +576460752303416789 545703395209036184 +576460752303416801 537421415932899422 +576460752303416927 290391961048171370 +576460752303417011 367363469987306388 +576460752303417019 7745174753766353 +576460752303417083 347335299793225121 +576460752303417109 114782619237907211 +576460752303417133 410504281746757742 +576460752303417181 455879305499645029 +576460752303417209 446480871255288426 +576460752303417287 153993425963858599 +576460752303417323 182070024449862086 +576460752303417337 374549079585562087 +576460752303417431 393206652483722703 +576460752303417437 486188842263545705 +576460752303417467 383850610653420288 +576460752303417617 497870848861389546 +576460752303417691 463218751930476837 +576460752303417731 524630333667357358 +576460752303417757 400406770671430550 +576460752303417797 319789130353886975 +576460752303417803 298499351316020762 +576460752303417833 197310205758014728 +576460752303417931 254705185407731984 +576460752303417959 17654444348100194 +576460752303418001 550228591657139717 +576460752303418051 513124870438209374 +576460752303418121 442037312391992698 +576460752303418141 275352713138100946 +576460752303418153 261221823842225316 +576460752303418253 517847529684003860 +576460752303418337 310663054310468504 +576460752303418369 276162614221509541 +576460752303418393 432478673090953686 +576460752303418439 213469652191442779 +576460752303418501 314359220618422126 +576460752303418559 23124065530016227 +576460752303418651 185860178206870511 +576460752303418663 457089943503762569 +576460752303418691 189088191202260862 +576460752303418751 500308971027054276 +576460752303418817 295894740388456646 +576460752303418901 303541704081659204 +576460752303418919 391516141977196262 +576460752303418963 540909894945461001 +576460752303418979 137963296523836510 +576460752303419083 365535814554277578 +576460752303419089 203596771542212700 +576460752303419129 312635544289815594 +576460752303419153 57978984577354830 +576460752303419227 392366094438693040 +576460752303419233 25807286906822964 +576460752303419251 551318530861578641 +576460752303419267 231111231360828335 +576460752303419311 433492087021543203 +576460752303419327 32704409838773365 +576460752303419381 51542875658353791 +576460752303419393 316440905663596971 +576460752303419407 835634693506233 +576460752303419443 566015020584164500 +576460752303419453 364576787412509951 +576460752303419461 564032016750250422 +576460752303419471 171297814951783847 +576460752303419537 114828362476681283 +576460752303419549 551945253498616549 +576460752303419563 188624603006630974 +576460752303419611 485663011501051406 +576460752303419629 439992859889348935 +576460752303419647 572751896917082962 +576460752303419693 520586583035480745 +576460752303419699 463168057949396617 +576460752303419719 79524865579573629 +576460752303419743 429215083843587962 +576460752303419773 432337062052489360 +576460752303419801 166276447147542471 +576460752303419813 427777688241757119 +576460752303419869 324335517334785280 +576460752303419891 1608603204565986 +576460752303419909 201287730019931491 +576460752303419989 541362381166291912 +576460752303420013 329820448166944701 +576460752303420037 439651379499223762 +576460752303420071 136859360098285043 +576460752303420247 548234621146055035 +576460752303420253 215032671848008034 +576460752303420277 379808262506077301 +576460752303420307 305013338846895151 +576460752303420311 354701180065423632 +576460752303420331 68958770011893546 +576460752303420409 199569195603214171 +576460752303420443 351100196692302615 +576460752303420541 255663950881971837 +576460752303420557 242001683896560979 +576460752303420563 157750813990430509 +576460752303420601 561702710544061860 +576460752303420631 52589023448655418 +576460752303420697 284060239466394369 +576460752303420703 63617993697764306 +576460752303420727 367249096439093533 +576460752303420731 320991901731307356 +576460752303420833 152389752633667814 +576460752303420917 301159379884668650 +576460752303420937 81762431565337874 +576460752303420953 433746528441315269 +576460752303420979 142752121825421483 +576460752303421123 410239475263696120 +576460752303421127 182458354673856136 +576460752303421169 112319347091351583 +576460752303421207 512272159581990126 +576460752303421213 230301744022251537 +576460752303421217 438339937641469366 +576460752303421259 573100887297582843 +576460752303421367 295775926106832198 +576460752303421387 282893909497996165 +576460752303421393 450782404586397457 +576460752303421429 215351530916672217 +576460752303421441 26926154667517866 +576460752303421511 513005249972493960 +576460752303421529 344759996325497668 +576460752303421543 421631296197773015 +576460752303421577 335628019205041888 +576460752303421597 514888149989234012 +576460752303421637 153684940089548255 +576460752303421649 559369941086683599 +576460752303421679 478466342615925072 +576460752303421709 23973793417038084 +576460752303421723 154093534719268113 +576460752303421759 153072327115006828 +576460752303421819 326588516444234635 +576460752303421861 483978683213042435 +576460752303421877 515289941057508498 +576460752303421897 66062933046194981 +576460752303421903 218299981751748251 +576460752303421919 83553829077613662 +576460752303421949 129785846572066095 +576460752303421963 277541037909429946 +576460752303422101 430618884965547007 +576460752303422153 353739064026772770 +576460752303422159 92492570019718375 +576460752303422219 486343623141696108 +576460752303422227 70980172088583743 +576460752303422243 256389345347075781 +576460752303422249 476321600580812847 +576460752303422269 149503984898679747 +576460752303422281 502785215880911014 +576460752303422309 330014282972858688 +576460752303422369 32382995820418724 +576460752303422431 481216662446475550 +576460752303422479 55795560714828412 +576460752303422501 397456660199110919 +576460752303422533 128797275833438045 +576460752303422543 523639419807473601 +576460752303422557 342960352220207925 +576460752303422599 337499207524925318 +576460752303422617 258601016385997341 +576460752303422627 56411897245890857 +576460752303422801 136112451897818438 +576460752303422839 372513673726628095 +576460752303422881 86879645301894173 +576460752303422971 524894730464158253 +576460752303423061 523304719106164833 +576460752303423263 12964950927601192 +576460752303423389 261710804607317973 +576460752303423433 380198378108741708 From 3d56771e60dbb1350141c0c8d4e12bfdf2cab1dc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:39:06 -0700 Subject: [PATCH 04/30] Add Geode5 formal proof audit --- .../workflows/geode5-formal-proof-audit.yml | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 .github/workflows/geode5-formal-proof-audit.yml diff --git a/.github/workflows/geode5-formal-proof-audit.yml b/.github/workflows/geode5-formal-proof-audit.yml new file mode 100644 index 00000000..50b15da4 --- /dev/null +++ b/.github/workflows/geode5-formal-proof-audit.yml @@ -0,0 +1,75 @@ +name: Geode5 formal proof audit + +on: + pull_request: + branches: [main] + paths: + - 'proofs/geode5/**' + - '.github/workflows/geode5-formal-proof-audit.yml' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: geode5-formal-proof-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +jobs: + crt-certificate: + name: Check Geode5 CRT certificate layer + runs-on: ubuntu-latest + timeout-minutes: 90 + steps: + - name: Checkout proof playground + uses: actions/checkout@v4 + with: + path: controller + + - name: Checkout immutable Formal Conjectures base + uses: actions/checkout@v4 + with: + repository: DomTheDeveloper/formal-conjectures + ref: 6db9713c4c2036afdad119eda930b4d1a8da3250 + path: target + + - name: Install proof module and certificate data + shell: bash + run: | + set -euo pipefail + dst=target/FormalConjectures/Arxiv/2508.10245/Geode5Proof + mkdir -p "$dst/data" + cp controller/proofs/geode5/Geode5CRT.lean "$dst/CRT.lean" + cp controller/proofs/geode5/data/G5_1000.txt "$dst/data/G5_1000.txt" + cp controller/proofs/geode5/data/residues_480.txt "$dst/data/residues_480.txt" + test -z "$(grep -nE '\b(sorry|admit)\b' "$dst/CRT.lean" || true)" + + - name: Install Lean 4.27 + shell: bash + run: | + set -euo pipefail + curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ + | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install leanprover/lean4:v4.27.0 + + - name: Fetch Mathlib cache + working-directory: target + run: lake exe cache get + + - name: Compile certificate with warnings as errors + working-directory: target + shell: bash + run: | + set -o pipefail + lake env lean -DwarningAsError=true \ + FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean \ + 2>&1 | tee geode5-crt-audit.log + + - name: Upload compiler transcript + if: always() + uses: actions/upload-artifact@v4 + with: + name: geode5-crt-audit + path: target/geode5-crt-audit.log + if-no-files-found: warn From 31a7e816226974c93bff70cd3ef9a936a2fcfc2a Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:39:18 -0700 Subject: [PATCH 05/30] Document Geode5 formal proof boundary --- proofs/geode5/README.md | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 proofs/geode5/README.md diff --git a/proofs/geode5/README.md b/proofs/geode5/README.md new file mode 100644 index 00000000..1ca669aa --- /dev/null +++ b/proofs/geode5/README.md @@ -0,0 +1,37 @@ +# Geode5 formal proof + +This directory turns the computational certificate from `geode5_bounty_solution.zip` into Lean proof layers for + +```text +G(1000,1000,1000,1000,1000). +``` + +## Completed Lean layer + +`Geode5CRT.lean` formalizes: + +- parsing the exact 8,367-digit answer and all 480 residue pairs; +- the fact that the 480 moduli are pairwise coprime; +- canonicality of every residue; +- agreement of the proposed answer with every stored residue; +- the hyper-Catalan upper bound; +- the strict inequality `upperBound < product moduli`; +- Chinese-remainder combination of all residue congruences; +- uniqueness of any candidate below the upper bound; +- the final conditional theorem `geode5_1000_of_certificate`. + +## Remaining formal bridge + +The ZIP contains a correct computational proof architecture, but not Lean source for the five-state recurrence. The remaining modules must prove: + +1. the alternating-sum definition of `geode5Diagonal` equals the one-variable moment coefficient formula; +2. the symbolic Euclidean divisions yield the five-state lower-triangular recurrence; +3. the modular recurrence computes each of the 480 stored residues; +4. `geode5Diagonal 1000` is nonnegative and below the hyper-Catalan bound. + +Once these are supplied, `geode5_1000_of_certificate` closes the exact benchmark equality with no `sorry` or custom axiom. + +## Audit + +The workflow `.github/workflows/geode5-formal-proof-audit.yml` overlays this proof module onto immutable Formal Conjectures commit +`6db9713c4c2036afdad119eda930b4d1a8da3250` and compiles it with Lean 4.27 and warnings as errors. From 7632e656e9cafe0754dd4c01be6b2cff51b55227 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:39:28 -0700 Subject: [PATCH 06/30] Record Geode5 proof status --- proofs/geode5/STATUS.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 proofs/geode5/STATUS.md diff --git a/proofs/geode5/STATUS.md b/proofs/geode5/STATUS.md new file mode 100644 index 00000000..711a4abe --- /dev/null +++ b/proofs/geode5/STATUS.md @@ -0,0 +1,7 @@ +# Status + +- Mathematical/computational certificate from ZIP: imported. +- Exact answer and 480 residues: imported byte-for-byte. +- Lean CRT/uniqueness layer: written; awaiting pinned Lean audit. +- Moment recurrence soundness layer: not yet formalized. +- Final theorem without `sorry`: not yet obtained. From 62712421d6925ad4c362977f9da9344849683008 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:40:43 -0700 Subject: [PATCH 07/30] Trigger Geode5 proof audit on branch pushes --- .github/workflows/geode5-formal-proof-audit.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/geode5-formal-proof-audit.yml b/.github/workflows/geode5-formal-proof-audit.yml index 50b15da4..19eaec52 100644 --- a/.github/workflows/geode5-formal-proof-audit.yml +++ b/.github/workflows/geode5-formal-proof-audit.yml @@ -1,6 +1,11 @@ name: Geode5 formal proof audit on: + push: + branches: [geode5-formal-proof] + paths: + - 'proofs/geode5/**' + - '.github/workflows/geode5-formal-proof-audit.yml' pull_request: branches: [main] paths: From 80576694045b8c343c6f7842d5aee08c2446ce15 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:45:15 -0700 Subject: [PATCH 08/30] Formalize Geode5 symbolic moment recurrence algebra --- proofs/geode5/Geode5MomentAlgebra.lean | 141 +++++++++++++++++++++++++ 1 file changed, 141 insertions(+) create mode 100644 proofs/geode5/Geode5MomentAlgebra.lean diff --git a/proofs/geode5/Geode5MomentAlgebra.lean b/proofs/geode5/Geode5MomentAlgebra.lean new file mode 100644 index 00000000..412b96d9 --- /dev/null +++ b/proofs/geode5/Geode5MomentAlgebra.lean @@ -0,0 +1,141 @@ +/- +Copyright 2026 Dominic Dabish. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Mathlib + +/-! +# Symbolic moment algebra for the five-dimensional Geode + +This file formalizes the symbolic source of the five-state recurrence from the +Geode certificate. The large sparse tables used by the C++ evaluator are not +trusted as primitive data: they are generated from the single polynomial + +`P_y(t) = ∏ w ∈ {0,1,2,3,4}, (y^w - t)`. + +For `k = 1, ..., 5`, the quotient in the Euclidean division of +`t^k * ∂P/∂t` by `P` is expressed by the power sums +`1 + y^d + y^(2d) + y^(3d) + y^(4d)`. The corresponding remainders have +`t`-degree at most four, which is exactly why five moments suffice. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +open scoped BigOperators + +/-- Polynomials in the parameter `y`. -/ +abbrev YPoly := Polynomial ℤ + +/-- Polynomials in `t` whose coefficients are polynomials in `y`. -/ +abbrev TYPoly := Polynomial YPoly + +private def y : YPoly := Polynomial.X +private def t : TYPoly := Polynomial.X + +/-- `1 + y^d + y^(2d) + y^(3d) + y^(4d)`. -/ +def powerSum (d : ℕ) : YPoly := + ∑ w ∈ Finset.range 5, y ^ (d * w) + +/-- The polynomial `P_y(t) = ∏_{w=0}^4 (y^w - t)`. -/ +def geodeKernel : TYPoly := + ∏ w ∈ Finset.range 5, (Polynomial.C (y ^ w) - t) + +/-- +The quotient predicted by Newton's identities for the division of +`t^k P_y'(t)` by `P_y(t)`. +-/ +def momentQuotient (k : ℕ) : TYPoly := + ∑ ell ∈ Finset.range k, + Polynomial.C (powerSum (k - 1 - ell)) * t ^ ell + +/-- The remainder generated from the quotient, rather than copied from a table. -/ +def momentRemainder (k : ℕ) : TYPoly := + t ^ k * geodeKernel.derivative - momentQuotient k * geodeKernel + +/-- The defining quotient/remainder identity. -/ +theorem moment_division_identity (k : ℕ) : + t ^ k * geodeKernel.derivative = + momentQuotient k * geodeKernel + momentRemainder k := by + simp only [momentRemainder] + ring + +/-- The zero-th power sum is the constant five. -/ +theorem powerSum_zero : powerSum 0 = 5 := by + native_decide + +/-- The five quotient rows used by the lower-triangular recurrence. -/ +theorem momentQuotient_rows : + momentQuotient 1 = 5 ∧ + momentQuotient 2 = + Polynomial.C (powerSum 1) + 5 * t ∧ + momentQuotient 3 = + Polynomial.C (powerSum 2) + + Polynomial.C (powerSum 1) * t + 5 * t ^ 2 ∧ + momentQuotient 4 = + Polynomial.C (powerSum 3) + + Polynomial.C (powerSum 2) * t + + Polynomial.C (powerSum 1) * t ^ 2 + 5 * t ^ 3 ∧ + momentQuotient 5 = + Polynomial.C (powerSum 4) + + Polynomial.C (powerSum 3) * t + + Polynomial.C (powerSum 2) * t ^ 2 + + Polynomial.C (powerSum 1) * t ^ 3 + 5 * t ^ 4 := by + native_decide + +/-- Every one of the five generated remainders has `t`-degree below five. -/ +theorem momentRemainder_degree_bounds : + (momentRemainder 1).natDegree < 5 ∧ + (momentRemainder 2).natDegree < 5 ∧ + (momentRemainder 3).natDegree < 5 ∧ + (momentRemainder 4).natDegree < 5 ∧ + (momentRemainder 5).natDegree < 5 := by + native_decide + +/-- The degree bound in the parameter `y` used by the sparse evaluator. -/ +theorem momentRemainder_y_degree_bounds : + (momentRemainder 1).coeff 0 |>.natDegree ≤ 10 ∧ + (momentRemainder 2).coeff 0 |>.natDegree ≤ 14 ∧ + (momentRemainder 3).coeff 0 |>.natDegree ≤ 18 ∧ + (momentRemainder 4).coeff 0 |>.natDegree ≤ 22 ∧ + (momentRemainder 5).coeff 0 |>.natDegree ≤ 26 := by + native_decide + +/-- Diagonal coefficient in recurrence row `i`, where `i = 0, ..., 4`. -/ +def recurrenceDiagonal (n i : ℕ) : ℕ := 5 * n + 6 + i + +/-- Every diagonal coefficient is positive, so forward substitution is valid in characteristic zero. -/ +theorem recurrenceDiagonal_pos (n i : ℕ) : 0 < recurrenceDiagonal n i := by + omega + +/-- Product of the five diagonal entries, matching the symbolic determinant. -/ +theorem recurrenceDiagonal_product (n : ℕ) : + ∏ i ∈ Finset.range 5, recurrenceDiagonal n i = + 5 * (n + 2) * (5 * n + 6) * (5 * n + 7) * + (5 * n + 8) * (5 * n + 9) := by + simp [recurrenceDiagonal] + ring + +/-- Through level 1000, every diagonal is at most 5010. -/ +theorem recurrenceDiagonal_le_5010 + (n i : ℕ) (hn : n < 1000) (hi : i < 5) : + recurrenceDiagonal n i ≤ 5010 := by + omega + +#print axioms moment_division_identity +#print axioms momentQuotient_rows +#print axioms momentRemainder_degree_bounds +#print axioms recurrenceDiagonal_product + +end Arxiv.«2508.10245».Geode5Proof From 64dd6c193074dbfb8a106c61a0b0b92d6a7106d2 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 01:45:37 -0700 Subject: [PATCH 09/30] Audit Geode5 symbolic recurrence and CRT layers --- .../workflows/geode5-formal-proof-audit.yml | 28 +++++++++++++------ 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/.github/workflows/geode5-formal-proof-audit.yml b/.github/workflows/geode5-formal-proof-audit.yml index 19eaec52..e7534dd3 100644 --- a/.github/workflows/geode5-formal-proof-audit.yml +++ b/.github/workflows/geode5-formal-proof-audit.yml @@ -21,8 +21,8 @@ concurrency: cancel-in-progress: true jobs: - crt-certificate: - name: Check Geode5 CRT certificate layer + certificate: + name: Check Geode5 proof layers runs-on: ubuntu-latest timeout-minutes: 90 steps: @@ -38,16 +38,17 @@ jobs: ref: 6db9713c4c2036afdad119eda930b4d1a8da3250 path: target - - name: Install proof module and certificate data + - name: Install proof modules and certificate data shell: bash run: | set -euo pipefail dst=target/FormalConjectures/Arxiv/2508.10245/Geode5Proof mkdir -p "$dst/data" cp controller/proofs/geode5/Geode5CRT.lean "$dst/CRT.lean" + cp controller/proofs/geode5/Geode5MomentAlgebra.lean "$dst/MomentAlgebra.lean" cp controller/proofs/geode5/data/G5_1000.txt "$dst/data/G5_1000.txt" cp controller/proofs/geode5/data/residues_480.txt "$dst/data/residues_480.txt" - test -z "$(grep -nE '\b(sorry|admit)\b' "$dst/CRT.lean" || true)" + test -z "$(grep -nE '\b(sorry|admit)\b' "$dst/CRT.lean" "$dst/MomentAlgebra.lean" || true)" - name: Install Lean 4.27 shell: bash @@ -62,7 +63,16 @@ jobs: working-directory: target run: lake exe cache get - - name: Compile certificate with warnings as errors + - name: Compile symbolic moment algebra + working-directory: target + shell: bash + run: | + set -o pipefail + lake env lean -DwarningAsError=true \ + FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean \ + 2>&1 | tee geode5-moment-audit.log + + - name: Compile CRT certificate working-directory: target shell: bash run: | @@ -71,10 +81,12 @@ jobs: FormalConjectures/Arxiv/2508.10245/Geode5Proof/CRT.lean \ 2>&1 | tee geode5-crt-audit.log - - name: Upload compiler transcript + - name: Upload compiler transcripts if: always() uses: actions/upload-artifact@v4 with: - name: geode5-crt-audit - path: target/geode5-crt-audit.log + name: geode5-proof-audit + path: | + target/geode5-moment-audit.log + target/geode5-crt-audit.log if-no-files-found: warn From 7ec6565966a53552e2ee20b018d96a64e1c3747a Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:03:12 -0700 Subject: [PATCH 10/30] Add algebraic integral layer for Geode5 moments --- proofs/geode5/Geode5Integral.lean | 75 +++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 proofs/geode5/Geode5Integral.lean diff --git a/proofs/geode5/Geode5Integral.lean b/proofs/geode5/Geode5Integral.lean new file mode 100644 index 00000000..f59b3b43 --- /dev/null +++ b/proofs/geode5/Geode5Integral.lean @@ -0,0 +1,75 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Geode5MomentAlgebra + +/-! +# Formal polynomial integration for the Geode moment recurrence + +The moment proof only needs integration of a polynomial in `t` from zero to one. +We define that operation algebraically, coefficient by coefficient, over +`Polynomial ℚ`. This avoids importing analytic integration and makes the +integration-by-parts argument available over exact rational coefficients. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +noncomputable section + +/-- Polynomials in `y` with rational coefficients. -/ +abbrev QYPoly := Polynomial ℚ + +/-- Polynomials in `t` with coefficients in `QYPoly`. -/ +abbrev TQYPoly := Polynomial QYPoly + +/-- Multiplication by `1 / (n + 1)` on `QYPoly`. -/ +def integralWeight (n : ℕ) : QYPoly →ₗ[ℚ] QYPoly where + toFun a := ((n + 1 : ℚ)⁻¹) • a + map_add' a b := by simp [smul_add] + map_smul' c a := by simp [smul_smul, mul_comm] + +/-- Algebraic integral from zero to one in the variable `t`. -/ +def integral01 : TQYPoly →ₗ[ℚ] QYPoly := + Polynomial.lsum integralWeight + +@[simp] +theorem integralWeight_apply (n : ℕ) (a : QYPoly) : + integralWeight n a = ((n + 1 : ℚ)⁻¹) • a := rfl + +@[simp] +theorem integral01_monomial (n : ℕ) (a : QYPoly) : + integral01 (Polynomial.monomial n a) = ((n + 1 : ℚ)⁻¹) • a := by + simp [integral01, integralWeight] + +/-- The algebraic fundamental theorem for polynomial derivatives. -/ +theorem integral01_derivative (p : TQYPoly) : + integral01 p.derivative = p.eval 1 - p.eval 0 := by + induction p using Polynomial.induction_on' with + | add p q hp hq => + simp [Polynomial.derivative_add, hp, hq, sub_add_sub_comm] + | monomial n a => + cases n with + | zero => simp [Polynomial.derivative_monomial] + | succ n => + rw [Polynomial.derivative_monomial_succ, integral01_monomial] + have hn : (n + 1 : ℚ) ≠ 0 := by positivity + simp [Polynomial.eval_monomial, Algebra.smul_def, hn, mul_comm] + +#print axioms integral01_derivative + +end + +end Arxiv.«2508.10245».Geode5Proof From 3d79946f8235e32c077e527ffd1a477bb5016373 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:04:00 -0700 Subject: [PATCH 11/30] Use qualified Geode5 integral import --- proofs/geode5/Geode5Integral.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/geode5/Geode5Integral.lean b/proofs/geode5/Geode5Integral.lean index f59b3b43..5415517c 100644 --- a/proofs/geode5/Geode5Integral.lean +++ b/proofs/geode5/Geode5Integral.lean @@ -14,7 +14,7 @@ See the License for the specific language governing permissions and limitations under the License. -/ -import Geode5MomentAlgebra +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentAlgebra /-! # Formal polynomial integration for the Geode moment recurrence From cc5c4fceec58df3c6667c6f8f127173f9bd28139 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:04:17 -0700 Subject: [PATCH 12/30] Audit Geode5 integral proof layer --- .github/workflows/geode5-formal-proof-audit.yml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/workflows/geode5-formal-proof-audit.yml b/.github/workflows/geode5-formal-proof-audit.yml index e7534dd3..6e0d53a3 100644 --- a/.github/workflows/geode5-formal-proof-audit.yml +++ b/.github/workflows/geode5-formal-proof-audit.yml @@ -46,9 +46,11 @@ jobs: mkdir -p "$dst/data" cp controller/proofs/geode5/Geode5CRT.lean "$dst/CRT.lean" cp controller/proofs/geode5/Geode5MomentAlgebra.lean "$dst/MomentAlgebra.lean" + cp controller/proofs/geode5/Geode5Integral.lean "$dst/Integral.lean" cp controller/proofs/geode5/data/G5_1000.txt "$dst/data/G5_1000.txt" cp controller/proofs/geode5/data/residues_480.txt "$dst/data/residues_480.txt" - test -z "$(grep -nE '\b(sorry|admit)\b' "$dst/CRT.lean" "$dst/MomentAlgebra.lean" || true)" + test -z "$(grep -nE '\b(sorry|admit)\b' \ + "$dst/CRT.lean" "$dst/MomentAlgebra.lean" "$dst/Integral.lean" || true)" - name: Install Lean 4.27 shell: bash @@ -72,6 +74,15 @@ jobs: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean \ 2>&1 | tee geode5-moment-audit.log + - name: Compile algebraic integral layer + working-directory: target + shell: bash + run: | + set -o pipefail + lake env lean -DwarningAsError=true \ + FormalConjectures/Arxiv/2508.10245/Geode5Proof/Integral.lean \ + 2>&1 | tee geode5-integral-audit.log + - name: Compile CRT certificate working-directory: target shell: bash @@ -88,5 +99,6 @@ jobs: name: geode5-proof-audit path: | target/geode5-moment-audit.log + target/geode5-integral-audit.log target/geode5-crt-audit.log if-no-files-found: warn From 618ec1843a992e574e430ae7d4808a17bde6785d Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:05:40 -0700 Subject: [PATCH 13/30] Use Formal Conjectures copyright for Geode5 algebra --- proofs/geode5/Geode5MomentAlgebra.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/proofs/geode5/Geode5MomentAlgebra.lean b/proofs/geode5/Geode5MomentAlgebra.lean index 412b96d9..dac3a3e7 100644 --- a/proofs/geode5/Geode5MomentAlgebra.lean +++ b/proofs/geode5/Geode5MomentAlgebra.lean @@ -1,5 +1,5 @@ /- -Copyright 2026 Dominic Dabish. +Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. @@ -20,14 +20,14 @@ import Mathlib # Symbolic moment algebra for the five-dimensional Geode This file formalizes the symbolic source of the five-state recurrence from the -Geode certificate. The large sparse tables used by the C++ evaluator are not +Geode certificate. The large sparse tables used by the C++ evaluator are not trusted as primitive data: they are generated from the single polynomial `P_y(t) = ∏ w ∈ {0,1,2,3,4}, (y^w - t)`. For `k = 1, ..., 5`, the quotient in the Euclidean division of `t^k * ∂P/∂t` by `P` is expressed by the power sums -`1 + y^d + y^(2d) + y^(3d) + y^(4d)`. The corresponding remainders have +`1 + y^d + y^(2d) + y^(3d) + y^(4d)`. The corresponding remainders have `t`-degree at most four, which is exactly why five moments suffice. -/ @@ -103,7 +103,7 @@ theorem momentRemainder_degree_bounds : (momentRemainder 5).natDegree < 5 := by native_decide -/-- The degree bound in the parameter `y` used by the sparse evaluator. -/ +/-- The constant-in-`t` coefficients satisfy the sparse evaluator's degree bounds. -/ theorem momentRemainder_y_degree_bounds : (momentRemainder 1).coeff 0 |>.natDegree ≤ 10 ∧ (momentRemainder 2).coeff 0 |>.natDegree ≤ 14 ∧ From 0e46db970b45ce473baccb3210da1eb4ce996f78 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:06:13 -0700 Subject: [PATCH 14/30] Use Formal Conjectures copyright for Geode5 CRT layer --- proofs/geode5/Geode5CRT.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/geode5/Geode5CRT.lean b/proofs/geode5/Geode5CRT.lean index 0aafcd9d..d5a0ea84 100644 --- a/proofs/geode5/Geode5CRT.lean +++ b/proofs/geode5/Geode5CRT.lean @@ -1,5 +1,5 @@ /- -Copyright 2026 Dominic Dabish. +Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. From 8426878fd58b78fcbb80f8c577e20c3112eb7016 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:07:59 -0700 Subject: [PATCH 15/30] Add exact Geode5 moment recurrence layer --- proofs/geode5/Geode5Recurrence.lean | 113 ++++++++++++++++++++++++++++ 1 file changed, 113 insertions(+) create mode 100644 proofs/geode5/Geode5Recurrence.lean diff --git a/proofs/geode5/Geode5Recurrence.lean b/proofs/geode5/Geode5Recurrence.lean new file mode 100644 index 00000000..58e78420 --- /dev/null +++ b/proofs/geode5/Geode5Recurrence.lean @@ -0,0 +1,113 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Integral + +/-! +# The exact five-state Geode moment recurrence + +This file proves the integration-by-parts recurrence used by the computational +certificate. The quotient and remainder polynomials are generated symbolically; +no sparse C++ table is assumed. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +open scoped BigOperators + +noncomputable section + +private def qy : QYPoly := Polynomial.X +private def qt : TQYPoly := Polynomial.X + +/-- Rational version of `1 + y^d + ... + y^(4d)`. -/ +def qPowerSum (d : ℕ) : QYPoly := + ∑ w ∈ Finset.range 5, qy ^ (d * w) + +/-- Rational Geode kernel `P_y(t)`. -/ +def qKernel : TQYPoly := + ∏ w ∈ Finset.range 5, (Polynomial.C (qy ^ w) - qt) + +/-- Quotient in the division of `t^k P_y'(t)` by `P_y(t)`. -/ +def qMomentQuotient (k : ℕ) : TQYPoly := + ∑ ell ∈ Finset.range k, + Polynomial.C (qPowerSum (k - 1 - ell)) * qt ^ ell + +/-- Generated remainder in the same division. -/ +def qMomentRemainder (k : ℕ) : TQYPoly := + qt ^ k * qKernel.derivative - qMomentQuotient k * qKernel + +/-- The quotient/remainder identity over rational coefficient polynomials. -/ +theorem qMoment_division_identity (k : ℕ) : + qt ^ k * qKernel.derivative = + qMomentQuotient k * qKernel + qMomentRemainder k := by + simp only [qMomentRemainder] + ring + +/-- Evaluation at `t = 1` vanishes because the `w = 0` factor is `1 - t`. -/ +theorem qKernel_eval_one : qKernel.eval 1 = 0 := by + native_decide + +/-- Evaluation at `t = 0` is `y^(0+1+2+3+4) = y^10`. -/ +theorem qKernel_eval_zero : qKernel.eval 0 = qy ^ 10 := by + native_decide + +/-- The exact polynomial moment `J_{n,k}(y)`. -/ +def qMoment (n k : ℕ) : QYPoly := + integral01 (qt ^ k * qKernel ^ n) + +/-- Initial moment vector `(1, 1/2, ..., 1/5)`. -/ +theorem qMoment_zero (k : ℕ) : + qMoment 0 k = Polynomial.C ((k + 1 : ℚ)⁻¹) := by + simp [qMoment, qt, integral01_monomial, Polynomial.X_pow_eq_monomial] + +/-- +Integration by parts followed by the generated quotient/remainder identity. +This is the recurrence before expanding the quotient and remainder coefficients. +-/ +theorem qMoment_recurrence_raw (n k : ℕ) (hk : 0 < k) : + (k : QYPoly) * qMoment (n + 1) (k - 1) + + (n + 1 : QYPoly) * + integral01 (qMomentQuotient k * qKernel ^ (n + 1)) = + -(n + 1 : QYPoly) * + integral01 (qMomentRemainder k * qKernel ^ n) := by + have hboundary : + integral01 ((qt ^ k * qKernel ^ (n + 1)).derivative) = 0 := by + rw [integral01_derivative] + simp [Polynomial.eval_mul, qKernel_eval_one, hk.ne'] + have hderiv : + (qt ^ k * qKernel ^ (n + 1)).derivative = + Polynomial.C (k : QYPoly) * qt ^ (k - 1) * qKernel ^ (n + 1) + + Polynomial.C (n + 1 : QYPoly) * + (qMomentQuotient k * qKernel ^ (n + 1) + + qMomentRemainder k * qKernel ^ n) := by + rw [Polynomial.derivative_mul, Polynomial.derivative_X_pow, + Polynomial.derivative_pow_succ, qMoment_division_identity] + ring + rw [hderiv] at hboundary + simp only [map_add, ← Polynomial.smul_eq_C_mul, map_smul] at hboundary + change + (k : QYPoly) * qMoment (n + 1) (k - 1) + + (n + 1 : QYPoly) * + (integral01 (qMomentQuotient k * qKernel ^ (n + 1)) + + integral01 (qMomentRemainder k * qKernel ^ n)) = 0 at hboundary + linear_combination hboundary + +#print axioms qMoment_recurrence_raw + +end + +end Arxiv.«2508.10245».Geode5Proof From 9c90ee6bc385bb67fd1dcb5c06051721c9c1126f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:09:14 -0700 Subject: [PATCH 16/30] Make Geode5 integral coefficient-linear --- proofs/geode5/Geode5Integral.lean | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/proofs/geode5/Geode5Integral.lean b/proofs/geode5/Geode5Integral.lean index 5415517c..fb19659b 100644 --- a/proofs/geode5/Geode5Integral.lean +++ b/proofs/geode5/Geode5Integral.lean @@ -21,8 +21,8 @@ import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentAlgebra The moment proof only needs integration of a polynomial in `t` from zero to one. We define that operation algebraically, coefficient by coefficient, over -`Polynomial ℚ`. This avoids importing analytic integration and makes the -integration-by-parts argument available over exact rational coefficients. +`Polynomial ℚ`. The map is linear over the coefficient ring `Polynomial ℚ`, so +polynomial coefficients in `y` factor through the integral exactly. -/ namespace Arxiv.«2508.10245».Geode5Proof @@ -35,23 +35,26 @@ abbrev QYPoly := Polynomial ℚ /-- Polynomials in `t` with coefficients in `QYPoly`. -/ abbrev TQYPoly := Polynomial QYPoly -/-- Multiplication by `1 / (n + 1)` on `QYPoly`. -/ -def integralWeight (n : ℕ) : QYPoly →ₗ[ℚ] QYPoly where - toFun a := ((n + 1 : ℚ)⁻¹) • a - map_add' a b := by simp [smul_add] - map_smul' c a := by simp [smul_smul, mul_comm] +/-- Multiplication by the constant polynomial `1 / (n + 1)` on `QYPoly`. -/ +def integralWeight (n : ℕ) : QYPoly →ₗ[QYPoly] QYPoly where + toFun a := Polynomial.C ((n + 1 : ℚ)⁻¹) * a + map_add' a b := by simp [mul_add] + map_smul' c a := by + simp only [smul_eq_mul] + ring /-- Algebraic integral from zero to one in the variable `t`. -/ -def integral01 : TQYPoly →ₗ[ℚ] QYPoly := +def integral01 : TQYPoly →ₗ[QYPoly] QYPoly := Polynomial.lsum integralWeight @[simp] theorem integralWeight_apply (n : ℕ) (a : QYPoly) : - integralWeight n a = ((n + 1 : ℚ)⁻¹) • a := rfl + integralWeight n a = Polynomial.C ((n + 1 : ℚ)⁻¹) * a := rfl @[simp] theorem integral01_monomial (n : ℕ) (a : QYPoly) : - integral01 (Polynomial.monomial n a) = ((n + 1 : ℚ)⁻¹) • a := by + integral01 (Polynomial.monomial n a) = + Polynomial.C ((n + 1 : ℚ)⁻¹) * a := by simp [integral01, integralWeight] /-- The algebraic fundamental theorem for polynomial derivatives. -/ @@ -66,7 +69,7 @@ theorem integral01_derivative (p : TQYPoly) : | succ n => rw [Polynomial.derivative_monomial_succ, integral01_monomial] have hn : (n + 1 : ℚ) ≠ 0 := by positivity - simp [Polynomial.eval_monomial, Algebra.smul_def, hn, mul_comm] + simp [Polynomial.eval_monomial, hn, Polynomial.natCast_eq_C, mul_comm] #print axioms integral01_derivative From 39d7a8975bb37eb3c9487af49936a8f8a78a3ae4 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:09:57 -0700 Subject: [PATCH 17/30] Audit exact Geode5 recurrence layer --- .github/workflows/geode5-formal-proof-audit.yml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/workflows/geode5-formal-proof-audit.yml b/.github/workflows/geode5-formal-proof-audit.yml index 6e0d53a3..894f0b5c 100644 --- a/.github/workflows/geode5-formal-proof-audit.yml +++ b/.github/workflows/geode5-formal-proof-audit.yml @@ -47,10 +47,12 @@ jobs: cp controller/proofs/geode5/Geode5CRT.lean "$dst/CRT.lean" cp controller/proofs/geode5/Geode5MomentAlgebra.lean "$dst/MomentAlgebra.lean" cp controller/proofs/geode5/Geode5Integral.lean "$dst/Integral.lean" + cp controller/proofs/geode5/Geode5Recurrence.lean "$dst/Recurrence.lean" cp controller/proofs/geode5/data/G5_1000.txt "$dst/data/G5_1000.txt" cp controller/proofs/geode5/data/residues_480.txt "$dst/data/residues_480.txt" test -z "$(grep -nE '\b(sorry|admit)\b' \ - "$dst/CRT.lean" "$dst/MomentAlgebra.lean" "$dst/Integral.lean" || true)" + "$dst/CRT.lean" "$dst/MomentAlgebra.lean" \ + "$dst/Integral.lean" "$dst/Recurrence.lean" || true)" - name: Install Lean 4.27 shell: bash @@ -83,6 +85,15 @@ jobs: FormalConjectures/Arxiv/2508.10245/Geode5Proof/Integral.lean \ 2>&1 | tee geode5-integral-audit.log + - name: Compile exact moment recurrence + working-directory: target + shell: bash + run: | + set -o pipefail + lake env lean -DwarningAsError=true \ + FormalConjectures/Arxiv/2508.10245/Geode5Proof/Recurrence.lean \ + 2>&1 | tee geode5-recurrence-audit.log + - name: Compile CRT certificate working-directory: target shell: bash @@ -100,5 +111,6 @@ jobs: path: | target/geode5-moment-audit.log target/geode5-integral-audit.log + target/geode5-recurrence-audit.log target/geode5-crt-audit.log if-no-files-found: warn From ac76e3504464f8923c591837b07cf57f715391b0 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:18:11 -0700 Subject: [PATCH 18/30] Formalize Geode5 factorial summand reduction --- proofs/geode5/Geode5Reduction.lean | 106 +++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 proofs/geode5/Geode5Reduction.lean diff --git a/proofs/geode5/Geode5Reduction.lean b/proofs/geode5/Geode5Reduction.lean new file mode 100644 index 00000000..0f01b03a --- /dev/null +++ b/proofs/geode5/Geode5Reduction.lean @@ -0,0 +1,106 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5 + +/-! +# Factorial reduction for the five-dimensional Geode + +This module formalizes the purely algebraic reduction of an individual term in +the four-dimensional alternating sum to the binomial form used in the moment +integral. It intentionally works over `ℚ`; the separate generalized-Catalan +integrality layer will connect the natural-number quotient in `hyperCatalan5` +to this rational expression. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +/-- A natural factorial viewed in `ℚ`. -/ +def qFactorial (n : ℕ) : ℚ := Nat.factorial n + +/-- The factorial quotient representing a binomial coefficient over `ℚ`. -/ +def qBinomial (n k : ℕ) : ℚ := + qFactorial n / (qFactorial k * qFactorial (n - k)) + +/-- The four-way multinomial factorial quotient over `ℚ`. -/ +def qMultinomial4 (a b c d : ℕ) : ℚ := + qFactorial (a + b + c + d) / + (qFactorial a * qFactorial b * qFactorial c * qFactorial d) + +/-- The hyper-Catalan factorial quotient before natural-number division. -/ +def qHyperCatalan5 (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℚ := + qFactorial (2 * m₁ + 3 * m₂ + 4 * m₃ + 5 * m₄ + 6 * m₅) / + (qFactorial (1 + m₁ + 2 * m₂ + 3 * m₃ + 4 * m₄ + 5 * m₅) * + qFactorial m₁ * qFactorial m₂ * qFactorial m₃ * + qFactorial m₄ * qFactorial m₅) + +/-- One rational summand in the original alternating Geode formula. -/ +def qAlternatingSummand (n a b c d : ℕ) : ℚ := + (-1 : ℚ) ^ (a + b + c + d) * qMultinomial4 a b c d * + qHyperCatalan5 (n + 1 + a + b + c + d) + (n - a) (n - b) (n - c) (n - d) + +/-- The same summand after collecting factorials as in the ZIP proof. -/ +def qReducedSummand (n a b c d : ℕ) : ℚ := + let r := a + b + c + d + let q := a + 2 * b + 3 * c + 4 * d + qFactorial (5 * n) / qFactorial n ^ 4 * + ((-1 : ℚ) ^ r * qFactorial r / qFactorial (n + r + 1) * + qBinomial n a * qBinomial n b * qBinomial n c * qBinomial n d * + qBinomial (20 * n + 2 - q) (5 * n)) + +/-- The numerator index in the specialized hyper-Catalan term. -/ +theorem specialized_numerator_index (n a b c d : ℕ) + (ha : a ≤ n) (hb : b ≤ n) (hc : c ≤ n) (hd : d ≤ n) : + 2 * (n + 1 + a + b + c + d) + 3 * (n - a) + 4 * (n - b) + + 5 * (n - c) + 6 * (n - d) = + 20 * n + 2 - (a + 2 * b + 3 * c + 4 * d) := by + omega + +/-- The long-factorial index in the specialized hyper-Catalan term. -/ +theorem specialized_long_index (n a b c d : ℕ) + (ha : a ≤ n) (hb : b ≤ n) (hc : c ≤ n) (hd : d ≤ n) : + 1 + (n + 1 + a + b + c + d) + 2 * (n - a) + 3 * (n - b) + + 4 * (n - c) + 5 * (n - d) = + 15 * n + 2 - (a + 2 * b + 3 * c + 4 * d) := by + omega + +/-- The complementary binomial index is the hyper-Catalan long index. -/ +theorem specialized_binomial_complement (n a b c d : ℕ) + (ha : a ≤ n) (hb : b ≤ n) (hc : c ≤ n) (hd : d ≤ n) : + (20 * n + 2 - (a + 2 * b + 3 * c + 4 * d)) - 5 * n = + 15 * n + 2 - (a + 2 * b + 3 * c + 4 * d) := by + omega + +/-- +The factorial identity at the heart of the alternating-sum-to-moment reduction. +No combinatorics or analysis is used here. +-/ +theorem qAlternatingSummand_eq_qReducedSummand (n a b c d : ℕ) + (ha : a ≤ n) (hb : b ≤ n) (hc : c ≤ n) (hd : d ≤ n) : + qAlternatingSummand n a b c d = qReducedSummand n a b c d := by + have hnum := specialized_numerator_index n a b c d ha hb hc hd + have hlong := specialized_long_index n a b c d ha hb hc hd + have hcomp := specialized_binomial_complement n a b c d ha hb hc hd + simp only [qAlternatingSummand, qReducedSummand, qHyperCatalan5, + qMultinomial4, qBinomial] + rw [hnum, hlong, hcomp] + field_simp [qFactorial] + ring + +#print axioms qAlternatingSummand_eq_qReducedSummand + +end Arxiv.«2508.10245».Geode5Proof From 1f4a9b8a90e1b373fd22befc91e250dd0befa20f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:21:47 -0700 Subject: [PATCH 19/30] Add exact Geode5 sparse remainder tables --- proofs/geode5/Geode5RemainderTables.lean | 189 +++++++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 proofs/geode5/Geode5RemainderTables.lean diff --git a/proofs/geode5/Geode5RemainderTables.lean b/proofs/geode5/Geode5RemainderTables.lean new file mode 100644 index 00000000..bf257eb1 --- /dev/null +++ b/proofs/geode5/Geode5RemainderTables.lean @@ -0,0 +1,189 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentAlgebra + +/-! +# Sparse remainder tables for the Geode5 recurrence + +The five lists below are the exact `R0`, ..., `R4` tables from the supplied C++ +certificate. Each entry `(src, shift, coefficient)` represents +`coefficient * y^shift * t^src`. The table metadata is checked by computation, +and the generated polynomial is proved equal to the symbolic remainder. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +noncomputable section + +structure SparseTerm where + source : ℕ + shift : ℕ + coefficient : ℤ + deriving DecidableEq, Repr + +private def y : YPoly := Polynomial.X +private def t : TYPoly := Polynomial.X + +/-- Interpret a sparse C++ table as a nested polynomial. -/ +def sparsePolynomial (terms : List SparseTerm) : TYPoly := + terms.foldr (fun a p => + Polynomial.C (a.coefficient * y ^ a.shift) * t ^ a.source + p) 0 + +/-- Sparse remainder table `R0` from the certificate. -/ +def r0Terms : List SparseTerm := [ + ⟨0, 10, -5⟩, ⟨1, 10, 4⟩, ⟨1, 9, 4⟩, ⟨1, 8, 4⟩, ⟨1, 7, 4⟩, + ⟨1, 6, 4⟩, ⟨2, 9, -3⟩, ⟨2, 8, -3⟩, ⟨2, 7, -6⟩, ⟨2, 6, -6⟩, + ⟨2, 5, -6⟩, ⟨2, 4, -3⟩, ⟨2, 3, -3⟩, ⟨3, 7, 2⟩, ⟨3, 6, 2⟩, + ⟨3, 5, 4⟩, ⟨3, 4, 4⟩, ⟨3, 3, 4⟩, ⟨3, 2, 2⟩, ⟨3, 1, 2⟩, + ⟨4, 4, -1⟩, ⟨4, 3, -1⟩, ⟨4, 2, -1⟩, ⟨4, 1, -1⟩, ⟨4, 0, -1⟩] + +/-- Sparse remainder table `R1` from the certificate. -/ +def r1Terms : List SparseTerm := [ + ⟨0, 14, -1⟩, ⟨0, 13, -1⟩, ⟨0, 12, -1⟩, ⟨0, 11, -1⟩, ⟨0, 10, -1⟩, + ⟨1, 14, 1⟩, ⟨1, 13, 2⟩, ⟨1, 12, 3⟩, ⟨1, 11, 4⟩, ⟨1, 9, 4⟩, + ⟨1, 8, 3⟩, ⟨1, 7, 2⟩, ⟨1, 6, 1⟩, ⟨2, 13, -1⟩, ⟨2, 12, -2⟩, + ⟨2, 11, -4⟩, ⟨2, 10, -2⟩, ⟨2, 9, -4⟩, ⟨2, 8, -4⟩, ⟨2, 7, -4⟩, + ⟨2, 6, -2⟩, ⟨2, 5, -4⟩, ⟨2, 4, -2⟩, ⟨2, 3, -1⟩, ⟨3, 11, 1⟩, + ⟨3, 10, 2⟩, ⟨3, 9, 1⟩, ⟨3, 8, 3⟩, ⟨3, 7, 2⟩, ⟨3, 6, 2⟩, + ⟨3, 5, 2⟩, ⟨3, 4, 3⟩, ⟨3, 3, 1⟩, ⟨3, 2, 2⟩, ⟨3, 1, 1⟩, + ⟨4, 8, -1⟩, ⟨4, 6, -1⟩, ⟨4, 4, -1⟩, ⟨4, 2, -1⟩, ⟨4, 0, -1⟩] + +/-- Sparse remainder table `R2` from the certificate. -/ +def r2Terms : List SparseTerm := [ + ⟨0, 18, -1⟩, ⟨0, 16, -1⟩, ⟨0, 14, -1⟩, ⟨0, 12, -1⟩, ⟨0, 10, -1⟩, + ⟨1, 18, 1⟩, ⟨1, 17, 1⟩, ⟨1, 16, 2⟩, ⟨1, 15, 2⟩, ⟨1, 14, 2⟩, + ⟨1, 13, 1⟩, ⟨1, 12, 2⟩, ⟨1, 11, 1⟩, ⟨1, 10, 2⟩, ⟨1, 9, 2⟩, + ⟨1, 8, 2⟩, ⟨1, 7, 1⟩, ⟨1, 6, 1⟩, ⟨2, 17, -1⟩, ⟨2, 16, -1⟩, + ⟨2, 15, -3⟩, ⟨2, 14, -2⟩, ⟨2, 13, -3⟩, ⟨2, 12, -1⟩, ⟨2, 11, -2⟩, + ⟨2, 10, -4⟩, ⟨2, 9, -2⟩, ⟨2, 8, -1⟩, ⟨2, 7, -3⟩, ⟨2, 6, -2⟩, + ⟨2, 5, -3⟩, ⟨2, 4, -1⟩, ⟨2, 3, -1⟩, ⟨3, 15, 1⟩, ⟨3, 14, 1⟩, + ⟨3, 13, 2⟩, ⟨3, 12, 1⟩, ⟨3, 11, 1⟩, ⟨3, 10, 2⟩, ⟨3, 9, 2⟩, + ⟨3, 7, 2⟩, ⟨3, 6, 2⟩, ⟨3, 5, 1⟩, ⟨3, 4, 1⟩, ⟨3, 3, 2⟩, + ⟨3, 2, 1⟩, ⟨3, 1, 1⟩, ⟨4, 12, -1⟩, ⟨4, 9, -1⟩, ⟨4, 6, -1⟩, + ⟨4, 3, -1⟩, ⟨4, 0, -1⟩] + +/-- Sparse remainder table `R3` from the certificate. -/ +def r3Terms : List SparseTerm := [ + ⟨0, 22, -1⟩, ⟨0, 19, -1⟩, ⟨0, 16, -1⟩, ⟨0, 13, -1⟩, ⟨0, 10, -1⟩, + ⟨1, 22, 1⟩, ⟨1, 21, 1⟩, ⟨1, 20, 1⟩, ⟨1, 19, 2⟩, ⟨1, 18, 1⟩, + ⟨1, 17, 1⟩, ⟨1, 16, 1⟩, ⟨1, 15, 2⟩, ⟨1, 13, 2⟩, ⟨1, 12, 1⟩, + ⟨1, 11, 1⟩, ⟨1, 10, 1⟩, ⟨1, 9, 2⟩, ⟨1, 8, 1⟩, ⟨1, 7, 1⟩, + ⟨1, 6, 1⟩, ⟨2, 21, -1⟩, ⟨2, 20, -1⟩, ⟨2, 19, -2⟩, ⟨2, 18, -2⟩, + ⟨2, 17, -2⟩, ⟨2, 16, -1⟩, ⟨2, 15, -2⟩, ⟨2, 14, -1⟩, ⟨2, 13, -2⟩, + ⟨2, 12, -2⟩, ⟨2, 11, -2⟩, ⟨2, 10, -1⟩, ⟨2, 9, -2⟩, ⟨2, 8, -1⟩, + ⟨2, 7, -2⟩, ⟨2, 6, -2⟩, ⟨2, 5, -2⟩, ⟨2, 4, -1⟩, ⟨2, 3, -1⟩, + ⟨3, 19, 1⟩, ⟨3, 18, 1⟩, ⟨3, 17, 1⟩, ⟨3, 16, 2⟩, ⟨3, 14, 1⟩, + ⟨3, 13, 1⟩, ⟨3, 12, 2⟩, ⟨3, 11, 1⟩, ⟨3, 9, 1⟩, ⟨3, 8, 2⟩, + ⟨3, 7, 1⟩, ⟨3, 6, 1⟩, ⟨3, 4, 2⟩, ⟨3, 3, 1⟩, ⟨3, 2, 1⟩, + ⟨3, 1, 1⟩, ⟨4, 16, -1⟩, ⟨4, 12, -1⟩, ⟨4, 8, -1⟩, ⟨4, 4, -1⟩, + ⟨4, 0, -1⟩] + +/-- Sparse remainder table `R4` from the certificate. -/ +def r4Terms : List SparseTerm := [ + ⟨0, 26, -1⟩, ⟨0, 22, -1⟩, ⟨0, 18, -1⟩, ⟨0, 14, -1⟩, ⟨0, 10, -1⟩, + ⟨1, 26, 1⟩, ⟨1, 25, 1⟩, ⟨1, 24, 1⟩, ⟨1, 23, 1⟩, ⟨1, 22, 1⟩, + ⟨1, 21, 1⟩, ⟨1, 20, 1⟩, ⟨1, 18, 2⟩, ⟨1, 17, 1⟩, ⟨1, 15, 1⟩, + ⟨1, 14, 2⟩, ⟨1, 12, 1⟩, ⟨1, 11, 1⟩, ⟨1, 10, 1⟩, ⟨1, 9, 1⟩, + ⟨1, 8, 1⟩, ⟨1, 7, 1⟩, ⟨1, 6, 1⟩, ⟨2, 25, -1⟩, ⟨2, 24, -1⟩, + ⟨2, 23, -2⟩, ⟨2, 22, -1⟩, ⟨2, 21, -2⟩, ⟨2, 20, -1⟩, ⟨2, 19, -1⟩, + ⟨2, 18, -1⟩, ⟨2, 17, -2⟩, ⟨2, 16, -1⟩, ⟨2, 15, -1⟩, ⟨2, 14, -2⟩, + ⟨2, 13, -1⟩, ⟨2, 12, -1⟩, ⟨2, 11, -2⟩, ⟨2, 10, -1⟩, ⟨2, 9, -1⟩, + ⟨2, 8, -1⟩, ⟨2, 7, -2⟩, ⟨2, 6, -1⟩, ⟨2, 5, -2⟩, ⟨2, 4, -1⟩, + ⟨2, 3, -1⟩, ⟨3, 23, 1⟩, ⟨3, 22, 1⟩, ⟨3, 21, 1⟩, ⟨3, 20, 1⟩, + ⟨3, 19, 1⟩, ⟨3, 17, 1⟩, ⟨3, 16, 1⟩, ⟨3, 15, 1⟩, ⟨3, 14, 1⟩, + ⟨3, 13, 1⟩, ⟨3, 11, 1⟩, ⟨3, 10, 1⟩, ⟨3, 9, 1⟩, ⟨3, 8, 1⟩, + ⟨3, 7, 1⟩, ⟨3, 5, 1⟩, ⟨3, 4, 1⟩, ⟨3, 3, 1⟩, ⟨3, 2, 1⟩, + ⟨3, 1, 1⟩, ⟨4, 20, -1⟩, ⟨4, 15, -1⟩, ⟨4, 10, -1⟩, ⟨4, 5, -1⟩, + ⟨4, 0, -1⟩] + +/-- All table source moment indices are valid. -/ +theorem remainderTable_sources_valid : + (∀ a ∈ r0Terms, a.source < 5) ∧ + (∀ a ∈ r1Terms, a.source < 5) ∧ + (∀ a ∈ r2Terms, a.source < 5) ∧ + (∀ a ∈ r3Terms, a.source < 5) ∧ + (∀ a ∈ r4Terms, a.source < 5) := by + native_decide + +/-- The exact maximum polynomial shifts used by the five rows. -/ +theorem remainderTable_shift_bounds : + (∀ a ∈ r0Terms, a.shift ≤ 10) ∧ + (∀ a ∈ r1Terms, a.shift ≤ 14) ∧ + (∀ a ∈ r2Terms, a.shift ≤ 18) ∧ + (∀ a ∈ r3Terms, a.shift ≤ 22) ∧ + (∀ a ∈ r4Terms, a.shift ≤ 26) := by + native_decide + +set_option maxHeartbeats 1000000 in +theorem momentRemainder_eq_r0 : + momentRemainder 1 = sparsePolynomial r0Terms := by + simp [momentRemainder, geodeKernel, momentQuotient, powerSum, + sparsePolynomial, r0Terms, y, t, Finset.prod_range_succ, + Finset.sum_range_succ, Polynomial.derivative_sub, + Polynomial.derivative_mul, Polynomial.derivative_C, + Polynomial.derivative_X] + ring + +set_option maxHeartbeats 1000000 in +theorem momentRemainder_eq_r1 : + momentRemainder 2 = sparsePolynomial r1Terms := by + simp [momentRemainder, geodeKernel, momentQuotient, powerSum, + sparsePolynomial, r1Terms, y, t, Finset.prod_range_succ, + Finset.sum_range_succ, Polynomial.derivative_sub, + Polynomial.derivative_mul, Polynomial.derivative_C, + Polynomial.derivative_X] + ring + +set_option maxHeartbeats 1000000 in +theorem momentRemainder_eq_r2 : + momentRemainder 3 = sparsePolynomial r2Terms := by + simp [momentRemainder, geodeKernel, momentQuotient, powerSum, + sparsePolynomial, r2Terms, y, t, Finset.prod_range_succ, + Finset.sum_range_succ, Polynomial.derivative_sub, + Polynomial.derivative_mul, Polynomial.derivative_C, + Polynomial.derivative_X] + ring + +set_option maxHeartbeats 1000000 in +theorem momentRemainder_eq_r3 : + momentRemainder 4 = sparsePolynomial r3Terms := by + simp [momentRemainder, geodeKernel, momentQuotient, powerSum, + sparsePolynomial, r3Terms, y, t, Finset.prod_range_succ, + Finset.sum_range_succ, Polynomial.derivative_sub, + Polynomial.derivative_mul, Polynomial.derivative_C, + Polynomial.derivative_X] + ring + +set_option maxHeartbeats 1000000 in +theorem momentRemainder_eq_r4 : + momentRemainder 5 = sparsePolynomial r4Terms := by + simp [momentRemainder, geodeKernel, momentQuotient, powerSum, + sparsePolynomial, r4Terms, y, t, Finset.prod_range_succ, + Finset.sum_range_succ, Polynomial.derivative_sub, + Polynomial.derivative_mul, Polynomial.derivative_C, + Polynomial.derivative_X] + ring + +#print axioms momentRemainder_eq_r0 +#print axioms momentRemainder_eq_r1 +#print axioms momentRemainder_eq_r2 +#print axioms momentRemainder_eq_r3 +#print axioms momentRemainder_eq_r4 + +end + +end Arxiv.«2508.10245».Geode5Proof From b5055dacb6a01ffb7b14e3c4f31382da1aa71f2b Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:22:22 -0700 Subject: [PATCH 20/30] Split Geode5 sparse remainder certification --- proofs/geode5/Geode5MomentAlgebra.lean | 73 +++++++++----------------- 1 file changed, 24 insertions(+), 49 deletions(-) diff --git a/proofs/geode5/Geode5MomentAlgebra.lean b/proofs/geode5/Geode5MomentAlgebra.lean index dac3a3e7..51874abd 100644 --- a/proofs/geode5/Geode5MomentAlgebra.lean +++ b/proofs/geode5/Geode5MomentAlgebra.lean @@ -24,17 +24,14 @@ Geode certificate. The large sparse tables used by the C++ evaluator are not trusted as primitive data: they are generated from the single polynomial `P_y(t) = ∏ w ∈ {0,1,2,3,4}, (y^w - t)`. - -For `k = 1, ..., 5`, the quotient in the Euclidean division of -`t^k * ∂P/∂t` by `P` is expressed by the power sums -`1 + y^d + y^(2d) + y^(3d) + y^(4d)`. The corresponding remainders have -`t`-degree at most four, which is exactly why five moments suffice. -/ namespace Arxiv.«2508.10245».Geode5Proof open scoped BigOperators +noncomputable section + /-- Polynomials in the parameter `y`. -/ abbrev YPoly := Polynomial ℤ @@ -43,6 +40,7 @@ abbrev TYPoly := Polynomial YPoly private def y : YPoly := Polynomial.X private def t : TYPoly := Polynomial.X +private def five : TYPoly := Polynomial.C (5 : YPoly) /-- `1 + y^d + y^(2d) + y^(3d) + y^(4d)`. -/ def powerSum (d : ℕ) : YPoly := @@ -52,15 +50,12 @@ def powerSum (d : ℕ) : YPoly := def geodeKernel : TYPoly := ∏ w ∈ Finset.range 5, (Polynomial.C (y ^ w) - t) -/-- -The quotient predicted by Newton's identities for the division of -`t^k P_y'(t)` by `P_y(t)`. --/ +/-- Quotient predicted by Newton power sums in `t^k P_y'(t) / P_y(t)`. -/ def momentQuotient (k : ℕ) : TYPoly := ∑ ell ∈ Finset.range k, Polynomial.C (powerSum (k - 1 - ell)) * t ^ ell -/-- The remainder generated from the quotient, rather than copied from a table. -/ +/-- Generated remainder; a separate table module certifies its sparse expansion. -/ def momentRemainder (k : ℕ) : TYPoly := t ^ k * geodeKernel.derivative - momentQuotient k * geodeKernel @@ -73,69 +68,49 @@ theorem moment_division_identity (k : ℕ) : /-- The zero-th power sum is the constant five. -/ theorem powerSum_zero : powerSum 0 = 5 := by - native_decide + norm_num [powerSum, y, Finset.sum_range_succ] /-- The five quotient rows used by the lower-triangular recurrence. -/ theorem momentQuotient_rows : - momentQuotient 1 = 5 ∧ - momentQuotient 2 = - Polynomial.C (powerSum 1) + 5 * t ∧ - momentQuotient 3 = - Polynomial.C (powerSum 2) + - Polynomial.C (powerSum 1) * t + 5 * t ^ 2 ∧ - momentQuotient 4 = - Polynomial.C (powerSum 3) + - Polynomial.C (powerSum 2) * t + - Polynomial.C (powerSum 1) * t ^ 2 + 5 * t ^ 3 ∧ - momentQuotient 5 = - Polynomial.C (powerSum 4) + - Polynomial.C (powerSum 3) * t + - Polynomial.C (powerSum 2) * t ^ 2 + - Polynomial.C (powerSum 1) * t ^ 3 + 5 * t ^ 4 := by - native_decide - -/-- Every one of the five generated remainders has `t`-degree below five. -/ -theorem momentRemainder_degree_bounds : - (momentRemainder 1).natDegree < 5 ∧ - (momentRemainder 2).natDegree < 5 ∧ - (momentRemainder 3).natDegree < 5 ∧ - (momentRemainder 4).natDegree < 5 ∧ - (momentRemainder 5).natDegree < 5 := by - native_decide - -/-- The constant-in-`t` coefficients satisfy the sparse evaluator's degree bounds. -/ -theorem momentRemainder_y_degree_bounds : - (momentRemainder 1).coeff 0 |>.natDegree ≤ 10 ∧ - (momentRemainder 2).coeff 0 |>.natDegree ≤ 14 ∧ - (momentRemainder 3).coeff 0 |>.natDegree ≤ 18 ∧ - (momentRemainder 4).coeff 0 |>.natDegree ≤ 22 ∧ - (momentRemainder 5).coeff 0 |>.natDegree ≤ 26 := by - native_decide + momentQuotient 1 = five ∧ + momentQuotient 2 = Polynomial.C (powerSum 1) + five * t ∧ + momentQuotient 3 = Polynomial.C (powerSum 2) + + Polynomial.C (powerSum 1) * t + five * t ^ 2 ∧ + momentQuotient 4 = Polynomial.C (powerSum 3) + + Polynomial.C (powerSum 2) * t + + Polynomial.C (powerSum 1) * t ^ 2 + five * t ^ 3 ∧ + momentQuotient 5 = Polynomial.C (powerSum 4) + + Polynomial.C (powerSum 3) * t + + Polynomial.C (powerSum 2) * t ^ 2 + + Polynomial.C (powerSum 1) * t ^ 3 + five * t ^ 4 := by + simp [momentQuotient, powerSum_zero, five, Finset.sum_range_succ] /-- Diagonal coefficient in recurrence row `i`, where `i = 0, ..., 4`. -/ def recurrenceDiagonal (n i : ℕ) : ℕ := 5 * n + 6 + i -/-- Every diagonal coefficient is positive, so forward substitution is valid in characteristic zero. -/ +/-- Every diagonal coefficient is positive. -/ theorem recurrenceDiagonal_pos (n i : ℕ) : 0 < recurrenceDiagonal n i := by - omega + simp [recurrenceDiagonal] /-- Product of the five diagonal entries, matching the symbolic determinant. -/ theorem recurrenceDiagonal_product (n : ℕ) : ∏ i ∈ Finset.range 5, recurrenceDiagonal n i = 5 * (n + 2) * (5 * n + 6) * (5 * n + 7) * (5 * n + 8) * (5 * n + 9) := by - simp [recurrenceDiagonal] + simp [recurrenceDiagonal, Finset.prod_range_succ] ring /-- Through level 1000, every diagonal is at most 5010. -/ theorem recurrenceDiagonal_le_5010 (n i : ℕ) (hn : n < 1000) (hi : i < 5) : recurrenceDiagonal n i ≤ 5010 := by + simp only [recurrenceDiagonal] omega #print axioms moment_division_identity #print axioms momentQuotient_rows -#print axioms momentRemainder_degree_bounds #print axioms recurrenceDiagonal_product +end + end Arxiv.«2508.10245».Geode5Proof From d03acb490f9571bc516487dd27454381111604ec Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:25:40 -0700 Subject: [PATCH 21/30] Reduce Geode5 integrality to cyclic multinomial divisibility --- proofs/geode5/Geode5IntegralityReduction.lean | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 proofs/geode5/Geode5IntegralityReduction.lean diff --git a/proofs/geode5/Geode5IntegralityReduction.lean b/proofs/geode5/Geode5IntegralityReduction.lean new file mode 100644 index 00000000..a3720542 --- /dev/null +++ b/proofs/geode5/Geode5IntegralityReduction.lean @@ -0,0 +1,81 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Reduction + +/-! +# Integrality reduction for the five-variable hyper-Catalan quotient + +The hyper-Catalan factorial quotient is a Raney/cycle-lemma number. This file +isolates the exact algebraic reduction: it is the full multinomial count of a +word with one negative step type and five nonnegative step types, divided by the +word length. The remaining integrality theorem is therefore the freeness of the +cyclic rotation action (equivalently, the cycle lemma). +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +/-- Numerator index in the five-variable hyper-Catalan quotient. -/ +def hyperNumeratorIndex (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℕ := + 2 * m₁ + 3 * m₂ + 4 * m₃ + 5 * m₄ + 6 * m₅ + +/-- Number of negative unit steps in the corresponding Raney word. -/ +def hyperLongIndex (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℕ := + 1 + m₁ + 2 * m₂ + 3 * m₃ + 4 * m₄ + 5 * m₅ + +/-- Total number of nonnegative steps. -/ +def hyperPositiveCount (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℕ := + m₁ + m₂ + m₃ + m₄ + m₅ + +/-- The word length is the hyper-Catalan numerator index plus one. -/ +theorem hyper_word_length_identity (m₁ m₂ m₃ m₄ m₅ : ℕ) : + hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1 = + hyperLongIndex m₁ m₂ m₃ m₄ m₅ + + hyperPositiveCount m₁ m₂ m₃ m₄ m₅ := by + omega + +/-- The full multinomial factorial quotient over `ℚ`. -/ +def qHyperFullMultinomial (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℚ := + qFactorial (hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1) / + (qFactorial (hyperLongIndex m₁ m₂ m₃ m₄ m₅) * + qFactorial m₁ * qFactorial m₂ * qFactorial m₃ * + qFactorial m₄ * qFactorial m₅) + +/-- +The hyper-Catalan rational quotient is the full multinomial count divided by +its total word length. +-/ +theorem qHyperCatalan5_eq_fullMultinomial_div_length + (m₁ m₂ m₃ m₄ m₅ : ℕ) : + qHyperCatalan5 m₁ m₂ m₃ m₄ m₅ = + qHyperFullMultinomial m₁ m₂ m₃ m₄ m₅ / + (hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1 : ℚ) := by + simp only [qHyperCatalan5, qHyperFullMultinomial, + hyperNumeratorIndex, hyperLongIndex, qFactorial, Nat.factorial_succ] + field_simp + ring + +/-- The associated step multiset has total sum `-1`. -/ +theorem raney_step_sum (m₁ m₂ m₃ m₄ m₅ : ℕ) : + (m₁ : ℤ) + 2 * m₂ + 3 * m₃ + 4 * m₄ + 5 * m₅ - + hyperLongIndex m₁ m₂ m₃ m₄ m₅ = -1 := by + simp [hyperLongIndex] + omega + +#print axioms qHyperCatalan5_eq_fullMultinomial_div_length +#print axioms raney_step_sum + +end Arxiv.«2508.10245».Geode5Proof From a7671f77c7d59cddef4eccc6ecdf3cb24b8ad14e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:27:22 -0700 Subject: [PATCH 22/30] Apply audited Geode5 integral fixes --- proofs/geode5/Geode5Integral.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/proofs/geode5/Geode5Integral.lean b/proofs/geode5/Geode5Integral.lean index fb19659b..c6670958 100644 --- a/proofs/geode5/Geode5Integral.lean +++ b/proofs/geode5/Geode5Integral.lean @@ -40,7 +40,7 @@ def integralWeight (n : ℕ) : QYPoly →ₗ[QYPoly] QYPoly where toFun a := Polynomial.C ((n + 1 : ℚ)⁻¹) * a map_add' a b := by simp [mul_add] map_smul' c a := by - simp only [smul_eq_mul] + simp only [smul_eq_mul, RingHom.id_apply] ring /-- Algebraic integral from zero to one in the variable `t`. -/ @@ -65,11 +65,14 @@ theorem integral01_derivative (p : TQYPoly) : simp [Polynomial.derivative_add, hp, hq, sub_add_sub_comm] | monomial n a => cases n with - | zero => simp [Polynomial.derivative_monomial] + | zero => simp | succ n => rw [Polynomial.derivative_monomial_succ, integral01_monomial] have hn : (n + 1 : ℚ) ≠ 0 := by positivity - simp [Polynomial.eval_monomial, hn, Polynomial.natCast_eq_C, mul_comm] + change a * Polynomial.C ((n : ℚ) + 1) * + Polynomial.C (((n : ℚ) + 1)⁻¹) = a + rw [mul_assoc, ← Polynomial.C_mul] + simp [hn] #print axioms integral01_derivative From a1e962fd618868f81ae99bd5780036adb294502f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:42:11 -0700 Subject: [PATCH 23/30] Prove Geode5 multinomial length divisibility --- .../geode5/Geode5MultinomialDivisibility.lean | 147 ++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 proofs/geode5/Geode5MultinomialDivisibility.lean diff --git a/proofs/geode5/Geode5MultinomialDivisibility.lean b/proofs/geode5/Geode5MultinomialDivisibility.lean new file mode 100644 index 00000000..04d3acb9 --- /dev/null +++ b/proofs/geode5/Geode5MultinomialDivisibility.lean @@ -0,0 +1,147 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Mathlib.Data.Nat.Choose.Multinomial +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.IntegralityReduction + +/-! +# Multinomial divisibility for the Geode hyper-Catalan quotient + +This avoids formalizing the full cycle lemma. For every symbol `a`, the total +word length divides `count a * multinomial`. The Geode counts satisfy an explicit +Bézout relation with coefficient one, so the word length divides the +multinomial coefficient itself. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +open scoped BigOperators + +/-- The sum of the counts divides each count times the multinomial coefficient. -/ +theorem sum_dvd_apply_mul_multinomial {α : Type*} [DecidableEq α] + (s : Finset α) (f : α → ℕ) {a : α} (ha : a ∈ s) : + (∑ i ∈ s, f i) ∣ f a * Nat.multinomial s f := by + by_cases hfa : f a = 0 + · simp [hfa] + obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero hfa + let r := ∑ i ∈ s.erase a, f i + have hsum : ∑ i ∈ s, f i = (k + 1) + r := by + calc + ∑ i ∈ s, f i = ∑ i ∈ insert a (s.erase a), f i := by + rw [Finset.insert_erase ha] + _ = f a + ∑ i ∈ s.erase a, f i := by + rw [Finset.sum_insert (Finset.notMem_erase a s)] + _ = (k + 1) + r := by rw [hk] + have hmulti : + Nat.multinomial s f = + ((k + 1) + r).choose (k + 1) * + Nat.multinomial (s.erase a) f := by + calc + Nat.multinomial s f = + Nat.multinomial (insert a (s.erase a)) f := by + rw [Finset.insert_erase ha] + _ = (f a + ∑ i ∈ s.erase a, f i).choose (f a) * + Nat.multinomial (s.erase a) f := by + rw [Nat.multinomial_insert (Finset.notMem_erase a s)] + _ = ((k + 1) + r).choose (k + 1) * + Nat.multinomial (s.erase a) f := by rw [hk] + refine ⟨(k + r).choose k * Nat.multinomial (s.erase a) f, ?_⟩ + rw [hsum, hk, hmulti] + have hchoose := Nat.add_one_mul_choose_eq (k + r) k + calc + (k + 1) * + (((k + 1) + r).choose (k + 1) * + Nat.multinomial (s.erase a) f) = + (((k + r) + 1).choose (k + 1) * (k + 1)) * + Nat.multinomial (s.erase a) f := by ring + _ = (((k + r) + 1) * (k + r).choose k) * + Nat.multinomial (s.erase a) f := by rw [← hchoose] + _ = ((k + 1) + r) * + ((k + r).choose k * Nat.multinomial (s.erase a) f) := by ring + +/-- The six symbols in the Raney-word interpretation. -/ +inductive HyperLetter + | negative | one | two | three | four | five + deriving DecidableEq, Fintype + +/-- Multiplicities of the six Raney-word symbols. -/ +def hyperCounts (m₁ m₂ m₃ m₄ m₅ : ℕ) : HyperLetter → ℕ + | .negative => hyperLongIndex m₁ m₂ m₃ m₄ m₅ + | .one => m₁ + | .two => m₂ + | .three => m₃ + | .four => m₄ + | .five => m₅ + +/-- The sum of all six counts is the numerator index plus one. -/ +theorem sum_hyperCounts (m₁ m₂ m₃ m₄ m₅ : ℕ) : + ∑ a : HyperLetter, hyperCounts m₁ m₂ m₃ m₄ m₅ a = + hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1 := by + simp [hyperCounts, hyperLongIndex, hyperNumeratorIndex] + omega + +/-- The full multinomial coefficient for the six Raney-word symbol counts. -/ +def hyperMultinomial (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℕ := + Nat.multinomial Finset.univ (hyperCounts m₁ m₂ m₃ m₄ m₅) + +/-- +The word length divides the full multinomial coefficient. This is the exact +integrality statement required for the five-variable hyper-Catalan number. +-/ +theorem hyper_word_length_dvd_multinomial (m₁ m₂ m₃ m₄ m₅ : ℕ) : + hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1 ∣ + hyperMultinomial m₁ m₂ m₃ m₄ m₅ := by + let c := hyperCounts m₁ m₂ m₃ m₄ m₅ + let L := hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1 + let M := hyperMultinomial m₁ m₂ m₃ m₄ m₅ + have hsum : (∑ a : HyperLetter, c a) = L := by + simpa [c, L] using sum_hyperCounts m₁ m₂ m₃ m₄ m₅ + have hdiv (a : HyperLetter) : L ∣ c a * M := by + rw [← hsum] + exact sum_dvd_apply_mul_multinomial Finset.univ c (Finset.mem_univ a) + have hneg := hdiv HyperLetter.negative + have h₁ := hdiv HyperLetter.one + have h₂ := hdiv HyperLetter.two + have h₃ := hdiv HyperLetter.three + have h₄ := hdiv HyperLetter.four + have h₅ := hdiv HyperLetter.five + have hweighted : + L ∣ (m₁ + 2 * m₂ + 3 * m₃ + 4 * m₄ + 5 * m₅) * M := by + dsimp [c, M] at h₁ h₂ h₃ h₄ h₅ + exact (((h₁.add (h₂.mul_left 2)).add (h₃.mul_left 3)).add + (h₄.mul_left 4)).add (h₅.mul_left 5) + have hrelation : + hyperLongIndex m₁ m₂ m₃ m₄ m₅ * M = + M + (m₁ + 2 * m₂ + 3 * m₃ + 4 * m₄ + 5 * m₅) * M := by + simp [hyperLongIndex] + ring + dsimp [c] at hneg + rw [hrelation] at hneg + exact (dvd_add_iff_left hweighted).mp hneg + +/-- The natural full multinomial has exactly the expected factorial quotient. -/ +theorem hyperMultinomial_eq_factorial_quotient (m₁ m₂ m₃ m₄ m₅ : ℕ) : + hyperMultinomial m₁ m₂ m₃ m₄ m₅ = + Nat.factorial (hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1) / + (Nat.factorial (hyperLongIndex m₁ m₂ m₃ m₄ m₅) * + Nat.factorial m₁ * Nat.factorial m₂ * Nat.factorial m₃ * + Nat.factorial m₄ * Nat.factorial m₅) := by + simp [hyperMultinomial, Nat.multinomial, hyperCounts, sum_hyperCounts] + +#print axioms sum_dvd_apply_mul_multinomial +#print axioms hyper_word_length_dvd_multinomial + +end Arxiv.«2508.10245».Geode5Proof From 10338903764403bb88a11aa7639fd85468351216 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:43:12 -0700 Subject: [PATCH 24/30] Sync kernel-verified Geode5 integral proof --- proofs/geode5/Geode5Integral.lean | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/proofs/geode5/Geode5Integral.lean b/proofs/geode5/Geode5Integral.lean index c6670958..fce2bf2b 100644 --- a/proofs/geode5/Geode5Integral.lean +++ b/proofs/geode5/Geode5Integral.lean @@ -68,11 +68,25 @@ theorem integral01_derivative (p : TQYPoly) : | zero => simp | succ n => rw [Polynomial.derivative_monomial_succ, integral01_monomial] - have hn : (n + 1 : ℚ) ≠ 0 := by positivity - change a * Polynomial.C ((n : ℚ) + 1) * - Polynomial.C (((n : ℚ) + 1)⁻¹) = a - rw [mul_assoc, ← Polynomial.C_mul] - simp [hn] + have hn : ((n : ℚ) + 1) ≠ 0 := by positivity + have hcast : + (n : QYPoly) + 1 = Polynomial.C ((n : ℚ) + 1) := by + norm_num + have hprod : + ((n : QYPoly) + 1) * Polynomial.C (((n : ℚ) + 1)⁻¹) = 1 := by + rw [hcast, ← Polynomial.C_mul] + simp [hn] + have hboundary : + Polynomial.eval 1 (Polynomial.monomial (n + 1) a) - + Polynomial.eval 0 (Polynomial.monomial (n + 1) a) = a := by + simp [Polynomial.eval_monomial] + rw [hboundary] + calc + Polynomial.C (((n : ℚ) + 1)⁻¹) * + (a * ((n : QYPoly) + 1)) = + a * (((n : QYPoly) + 1) * + Polynomial.C (((n : ℚ) + 1)⁻¹)) := by ring + _ = a := by rw [hprod, mul_one] #print axioms integral01_derivative From a5f075ea3ef998da6ec76cb5c6c0f7dd7074efe8 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:46:02 -0700 Subject: [PATCH 25/30] Complete the Geode5 hyper-Catalan integrality bridge --- .../geode5/Geode5HyperCatalanIntegrality.lean | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 proofs/geode5/Geode5HyperCatalanIntegrality.lean diff --git a/proofs/geode5/Geode5HyperCatalanIntegrality.lean b/proofs/geode5/Geode5HyperCatalanIntegrality.lean new file mode 100644 index 00000000..8ee567b5 --- /dev/null +++ b/proofs/geode5/Geode5HyperCatalanIntegrality.lean @@ -0,0 +1,85 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MultinomialDivisibility + +/-! +# Integrality of the five-variable hyper-Catalan quotient + +This completes the natural-number/rational bridge needed to rewrite the +`Nat.div` in `hyperCatalan5` as the exact factorial quotient used by the Geode +moment proof. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +/-- Denominator shared by the hyper-Catalan and full multinomial quotients. -/ +def hyperDenominator (m₁ m₂ m₃ m₄ m₅ : ℕ) : ℕ := + Nat.factorial (hyperLongIndex m₁ m₂ m₃ m₄ m₅) * + Nat.factorial m₁ * Nat.factorial m₂ * Nat.factorial m₃ * + Nat.factorial m₄ * Nat.factorial m₅ + +/-- The natural hyper-Catalan quotient is the full multinomial divided by length. -/ +theorem hyperCatalan5_eq_hyperMultinomial_div_length + (m₁ m₂ m₃ m₄ m₅ : ℕ) : + hyperCatalan5 m₁ m₂ m₃ m₄ m₅ = + hyperMultinomial m₁ m₂ m₃ m₄ m₅ / + (hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1) := by + let N := hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + let L := N + 1 + let D := hyperDenominator m₁ m₂ m₃ m₄ m₅ + have hL : 0 < L := by simp [L] + rw [hyperMultinomial_eq_factorial_quotient] + simp only [hyperCatalan5, hyperNumeratorIndex, hyperLongIndex, + hyperDenominator] at ⊢ + change Nat.factorial N / D = + (Nat.factorial L / D) / L + rw [Nat.div_div_eq_div_mul] + have hfac : Nat.factorial L = L * Nat.factorial N := by + simp [L, Nat.factorial_succ] + rw [hfac] + calc + (L * Nat.factorial N) / (D * L) = + (Nat.factorial N * L) / (D * L) := by rw [Nat.mul_comm] + _ = Nat.factorial N / D := by + exact Nat.mul_div_mul_right _ _ hL + +/-- The full multinomial is exactly length times the hyper-Catalan number. -/ +theorem hyperMultinomial_eq_length_mul_hyperCatalan5 + (m₁ m₂ m₃ m₄ m₅ : ℕ) : + hyperMultinomial m₁ m₂ m₃ m₄ m₅ = + (hyperNumeratorIndex m₁ m₂ m₃ m₄ m₅ + 1) * + hyperCatalan5 m₁ m₂ m₃ m₄ m₅ := by + rw [hyperCatalan5_eq_hyperMultinomial_div_length] + exact (Nat.mul_div_cancel' (hyper_word_length_dvd_multinomial + m₁ m₂ m₃ m₄ m₅)).symm + +/-- Cast of `hyperCatalan5` equals its exact rational factorial quotient. -/ +theorem cast_hyperCatalan5_eq_qHyperCatalan5 + (m₁ m₂ m₃ m₄ m₅ : ℕ) : + (hyperCatalan5 m₁ m₂ m₃ m₄ m₅ : ℚ) = + qHyperCatalan5 m₁ m₂ m₃ m₄ m₅ := by + rw [hyperCatalan5_eq_hyperMultinomial_div_length] + rw [Nat.cast_div (hyper_word_length_dvd_multinomial m₁ m₂ m₃ m₄ m₅)] + rw [qHyperCatalan5_eq_fullMultinomial_div_length] + congr 1 + rw [hyperMultinomial_eq_factorial_quotient] + simp [qHyperFullMultinomial, qFactorial, hyperDenominator] + +#print axioms hyper_word_length_dvd_multinomial +#print axioms cast_hyperCatalan5_eq_qHyperCatalan5 + +end Arxiv.«2508.10245».Geode5Proof From 26a43d575313dfb41073ba32110bb2c6b74e4f22 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:48:07 -0700 Subject: [PATCH 26/30] Bridge Geode5 symbolic recurrence to sparse tables --- proofs/geode5/Geode5ExpandedRecurrence.lean | 109 ++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 proofs/geode5/Geode5ExpandedRecurrence.lean diff --git a/proofs/geode5/Geode5ExpandedRecurrence.lean b/proofs/geode5/Geode5ExpandedRecurrence.lean new file mode 100644 index 00000000..eb8fbe3d --- /dev/null +++ b/proofs/geode5/Geode5ExpandedRecurrence.lean @@ -0,0 +1,109 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Recurrence +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.RemainderTables + +/-! +# Expanded sparse Geode5 moment recurrence + +This module proves the generic bridge from the symbolic integration-by-parts +identity to the sparse table update used by the modular evaluator. +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +open scoped BigOperators + +noncomputable section + +private def qy : QYPoly := Polynomial.X +private def qt : TQYPoly := Polynomial.X + +/-- Interpret an integer sparse table in the rational nested polynomial ring. -/ +def qSparsePolynomial (terms : List SparseTerm) : TQYPoly := + terms.foldr (fun a p => + Polynomial.C (Polynomial.C (a.coefficient : ℚ) * qy ^ a.shift) * + qt ^ a.source + p) 0 + +/-- The corresponding sparse linear combination of the five moments. -/ +def qSparseMomentSum (terms : List SparseTerm) (n : ℕ) : QYPoly := + terms.foldr (fun a p => + (Polynomial.C (a.coefficient : ℚ) * qy ^ a.shift) * + qMoment n a.source + p) 0 + +/-- Polynomial integration converts a sparse polynomial row into its sparse moment sum. -/ +theorem integral01_qSparsePolynomial_mul (terms : List SparseTerm) (n : ℕ) : + integral01 (qSparsePolynomial terms * qKernel ^ n) = + qSparseMomentSum terms n := by + induction terms with + | nil => simp [qSparsePolynomial, qSparseMomentSum] + | cons a terms ih => + simp only [qSparsePolynomial, qSparseMomentSum, List.foldr_cons] + rw [add_mul, map_add, ih] + change + integral01 + (Polynomial.C + (Polynomial.C (a.coefficient : ℚ) * qy ^ a.shift) * + (qt ^ a.source * qKernel ^ n)) + + qSparseMomentSum terms n = + (Polynomial.C (a.coefficient : ℚ) * qy ^ a.shift) * + qMoment n a.source + qSparseMomentSum terms n + rw [← Polynomial.smul_eq_C_mul, map_smul] + rfl + +/-- Expansion of the Newton power-sum quotient against the moment vector. -/ +theorem integral01_qMomentQuotient_mul (n k : ℕ) : + integral01 (qMomentQuotient k * qKernel ^ n) = + ∑ ell ∈ Finset.range k, + qPowerSum (k - 1 - ell) * qMoment n ell := by + simp only [qMomentQuotient, Finset.sum_mul, map_sum] + apply Finset.sum_congr rfl + intro ell hell + rw [mul_assoc] + change + integral01 + (Polynomial.C (qPowerSum (k - 1 - ell)) * + (qt ^ ell * qKernel ^ n)) = + qPowerSum (k - 1 - ell) * qMoment n ell + rw [← Polynomial.smul_eq_C_mul, map_smul] + rfl + +/-- +Generic sparse recurrence row. Supplying a certified equality between the +symbolic remainder and one of the exact `R0`, ..., `R4` tables yields the same +update equation used by the modular evaluator. +-/ +theorem qMoment_recurrence_sparse (n k : ℕ) (hk : 0 < k) + (terms : List SparseTerm) + (hrem : qMomentRemainder k = qSparsePolynomial terms) : + (k : QYPoly) * qMoment (n + 1) (k - 1) + + (n + 1 : QYPoly) * + (∑ ell ∈ Finset.range k, + qPowerSum (k - 1 - ell) * qMoment (n + 1) ell) = + -(n + 1 : QYPoly) * qSparseMomentSum terms n := by + rw [← integral01_qMomentQuotient_mul] + rw [← integral01_qSparsePolynomial_mul] + rw [← hrem] + exact qMoment_recurrence_raw n k hk + +#print axioms integral01_qSparsePolynomial_mul +#print axioms integral01_qMomentQuotient_mul +#print axioms qMoment_recurrence_sparse + +end + +end Arxiv.«2508.10245».Geode5Proof From b99e02c728756010a968870c450820086ad74b36 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:48:55 -0700 Subject: [PATCH 27/30] Bridge the exact Geode5 benchmark definition to rationals --- proofs/geode5/Geode5CastBridges.lean | 82 ++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 proofs/geode5/Geode5CastBridges.lean diff --git a/proofs/geode5/Geode5CastBridges.lean b/proofs/geode5/Geode5CastBridges.lean new file mode 100644 index 00000000..0f604777 --- /dev/null +++ b/proofs/geode5/Geode5CastBridges.lean @@ -0,0 +1,82 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.HyperCatalanIntegrality + +/-! +# Cast bridges from the benchmark definition to the rational Geode proof +-/ + +namespace Arxiv.«2508.10245».Geode5Proof + +open scoped BigOperators + +inductive FourLetter + | first | second | third | fourth + deriving DecidableEq, Fintype + +/-- Four symbol multiplicities used for the ordinary multinomial coefficient. -/ +def fourCounts (a b c d : ℕ) : FourLetter → ℕ + | .first => a + | .second => b + | .third => c + | .fourth => d + +/-- The denominator in `multinomial4` divides its factorial numerator. -/ +theorem multinomial4_denominator_dvd (a b c d : ℕ) : + Nat.factorial a * Nat.factorial b * Nat.factorial c * Nat.factorial d ∣ + Nat.factorial (a + b + c + d) := by + simpa [fourCounts, mul_assoc, add_assoc, add_comm, add_left_comm] using + (Nat.multinomial_dvd_factorial (s := Finset.univ) (fourCounts a b c d)) + +/-- Cast of `multinomial4` equals the exact rational factorial quotient. -/ +theorem cast_multinomial4_eq_qMultinomial4 (a b c d : ℕ) : + (multinomial4 a b c d : ℚ) = qMultinomial4 a b c d := by + rw [multinomial4, Nat.cast_div (multinomial4_denominator_dvd a b c d)] + simp [qMultinomial4, qFactorial] + +/-- Rational version of the original alternating-sum definition. -/ +def qGeode5Diagonal (n : ℕ) : ℚ := + ∑ j₂ ∈ Finset.range (n + 1), + ∑ j₃ ∈ Finset.range (n + 1), + ∑ j₄ ∈ Finset.range (n + 1), + ∑ j₅ ∈ Finset.range (n + 1), + (-1 : ℚ) ^ (j₂ + j₃ + j₄ + j₅) * + qMultinomial4 j₂ j₃ j₄ j₅ * + qHyperCatalan5 (n + 1 + j₂ + j₃ + j₄ + j₅) + (n - j₂) (n - j₃) (n - j₄) (n - j₅) + +/-- Casting the exact benchmark definition gives the rational alternating sum. -/ +theorem cast_geode5Diagonal_eq_qGeode5Diagonal (n : ℕ) : + (geode5Diagonal n : ℚ) = qGeode5Diagonal n := by + simp only [geode5Diagonal, qGeode5Diagonal, Int.cast_sum, Int.cast_mul, + Int.cast_pow, Int.cast_neg, Int.cast_one, Nat.cast_ofNat] + apply Finset.sum_congr rfl + intro j₂ hj₂ + apply Finset.sum_congr rfl + intro _ _ + apply Finset.sum_congr rfl + intro _ _ + apply Finset.sum_congr rfl + intro j₅ hj₅ + rw [cast_multinomial4_eq_qMultinomial4, + cast_hyperCatalan5_eq_qHyperCatalan5] + norm_num + +#print axioms cast_multinomial4_eq_qMultinomial4 +#print axioms cast_geode5Diagonal_eq_qGeode5Diagonal + +end Arxiv.«2508.10245».Geode5Proof From 3629ede0493712742d6d7a548a8c3bb0a8a972cd Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:53:34 -0700 Subject: [PATCH 28/30] Sync kernel-verified Geode5 raw recurrence --- proofs/geode5/Geode5Recurrence.lean | 50 ++++++++++++++++++++++------- 1 file changed, 38 insertions(+), 12 deletions(-) diff --git a/proofs/geode5/Geode5Recurrence.lean b/proofs/geode5/Geode5Recurrence.lean index 58e78420..eaa96d5f 100644 --- a/proofs/geode5/Geode5Recurrence.lean +++ b/proofs/geode5/Geode5Recurrence.lean @@ -59,11 +59,12 @@ theorem qMoment_division_identity (k : ℕ) : /-- Evaluation at `t = 1` vanishes because the `w = 0` factor is `1 - t`. -/ theorem qKernel_eval_one : qKernel.eval 1 = 0 := by - native_decide + simp [qKernel, qy, qt, Finset.prod_range_succ] /-- Evaluation at `t = 0` is `y^(0+1+2+3+4) = y^10`. -/ theorem qKernel_eval_zero : qKernel.eval 0 = qy ^ 10 := by - native_decide + simp [qKernel, qy, qt, Finset.prod_range_succ] + ring /-- The exact polynomial moment `J_{n,k}(y)`. -/ def qMoment (n k : ℕ) : QYPoly := @@ -87,23 +88,48 @@ theorem qMoment_recurrence_raw (n k : ℕ) (hk : 0 < k) : have hboundary : integral01 ((qt ^ k * qKernel ^ (n + 1)).derivative) = 0 := by rw [integral01_derivative] - simp [Polynomial.eval_mul, qKernel_eval_one, hk.ne'] + simp [Polynomial.eval_mul, qt, qKernel_eval_one, hk.ne'] have hderiv : (qt ^ k * qKernel ^ (n + 1)).derivative = - Polynomial.C (k : QYPoly) * qt ^ (k - 1) * qKernel ^ (n + 1) + - Polynomial.C (n + 1 : QYPoly) * + (k : QYPoly) • (qt ^ (k - 1) * qKernel ^ (n + 1)) + + (n + 1 : QYPoly) • (qMomentQuotient k * qKernel ^ (n + 1) + qMomentRemainder k * qKernel ^ n) := by - rw [Polynomial.derivative_mul, Polynomial.derivative_X_pow, - Polynomial.derivative_pow_succ, qMoment_division_identity] - ring + rw [Polynomial.derivative_mul] + simp only [qt, Polynomial.derivative_X_pow, + Polynomial.derivative_pow_succ] + have hdiv := qMoment_division_identity k + simp only [qt] at hdiv + simp only [Polynomial.smul_eq_C_mul] + calc + Polynomial.C (k : QYPoly) * Polynomial.X ^ (k - 1) * + qKernel ^ (n + 1) + + Polynomial.X ^ k * + (Polynomial.C (n + 1 : QYPoly) * qKernel ^ n * + qKernel.derivative) = + Polynomial.C (k : QYPoly) * + (Polynomial.X ^ (k - 1) * qKernel ^ (n + 1)) + + Polynomial.C (n + 1 : QYPoly) * + ((Polynomial.X ^ k * qKernel.derivative) * qKernel ^ n) := by + ring + _ = Polynomial.C (k : QYPoly) * + (Polynomial.X ^ (k - 1) * qKernel ^ (n + 1)) + + Polynomial.C (n + 1 : QYPoly) * + ((qMomentQuotient k * qKernel + qMomentRemainder k) * + qKernel ^ n) := by rw [hdiv] + _ = Polynomial.C (k : QYPoly) * + (Polynomial.X ^ (k - 1) * qKernel ^ (n + 1)) + + Polynomial.C (n + 1 : QYPoly) * + (qMomentQuotient k * qKernel ^ (n + 1) + + qMomentRemainder k * qKernel ^ n) := by ring rw [hderiv] at hboundary - simp only [map_add, ← Polynomial.smul_eq_C_mul, map_smul] at hboundary + simp only [map_add, map_smul, smul_eq_mul] at hboundary change - (k : QYPoly) * qMoment (n + 1) (k - 1) + + (k : QYPoly) * integral01 (qt ^ (k - 1) * qKernel ^ (n + 1)) + (n + 1 : QYPoly) * - (integral01 (qMomentQuotient k * qKernel ^ (n + 1)) + - integral01 (qMomentRemainder k * qKernel ^ n)) = 0 at hboundary + integral01 (qMomentQuotient k * qKernel ^ (n + 1)) = + -(n + 1 : QYPoly) * + integral01 (qMomentRemainder k * qKernel ^ n) linear_combination hboundary #print axioms qMoment_recurrence_raw From bc9977e93a0c26ad5b3cb82b98e09d9a704dc948 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:57:05 -0700 Subject: [PATCH 29/30] Use mathlib's multinomial recurrence for Geode5 integrality --- .../geode5/Geode5MultinomialDivisibility.lean | 70 +++++++++---------- 1 file changed, 32 insertions(+), 38 deletions(-) diff --git a/proofs/geode5/Geode5MultinomialDivisibility.lean b/proofs/geode5/Geode5MultinomialDivisibility.lean index 04d3acb9..2f666bb4 100644 --- a/proofs/geode5/Geode5MultinomialDivisibility.lean +++ b/proofs/geode5/Geode5MultinomialDivisibility.lean @@ -20,10 +20,9 @@ import FormalConjectures.Arxiv.«2508.10245».Geode5Proof.IntegralityReduction /-! # Multinomial divisibility for the Geode hyper-Catalan quotient -This avoids formalizing the full cycle lemma. For every symbol `a`, the total -word length divides `count a * multinomial`. The Geode counts satisfy an explicit -Bézout relation with coefficient one, so the word length divides the -multinomial coefficient itself. +For every symbol `a`, the total word length divides +`count a * multinomial`. The Geode counts then supply an explicit coefficient-one +linear relation, so the word length divides the multinomial coefficient itself. -/ namespace Arxiv.«2508.10245».Geode5Proof @@ -36,41 +35,36 @@ theorem sum_dvd_apply_mul_multinomial {α : Type*} [DecidableEq α] (∑ i ∈ s, f i) ∣ f a * Nat.multinomial s f := by by_cases hfa : f a = 0 · simp [hfa] - obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero hfa - let r := ∑ i ∈ s.erase a, f i - have hsum : ∑ i ∈ s, f i = (k + 1) + r := by - calc - ∑ i ∈ s, f i = ∑ i ∈ insert a (s.erase a), f i := by - rw [Finset.insert_erase ha] - _ = f a + ∑ i ∈ s.erase a, f i := by - rw [Finset.sum_insert (Finset.notMem_erase a s)] - _ = (k + 1) + r := by rw [hk] - have hmulti : - Nat.multinomial s f = - ((k + 1) + r).choose (k + 1) * - Nat.multinomial (s.erase a) f := by - calc - Nat.multinomial s f = - Nat.multinomial (insert a (s.erase a)) f := by - rw [Finset.insert_erase ha] - _ = (f a + ∑ i ∈ s.erase a, f i).choose (f a) * - Nat.multinomial (s.erase a) f := by - rw [Nat.multinomial_insert (Finset.notMem_erase a s)] - _ = ((k + 1) + r).choose (k + 1) * - Nat.multinomial (s.erase a) f := by rw [hk] - refine ⟨(k + r).choose k * Nat.multinomial (s.erase a) f, ?_⟩ - rw [hsum, hk, hmulti] - have hchoose := Nat.add_one_mul_choose_eq (k + r) k + let g := Function.update f a (f a - 1) + have hfa_pos : 0 < f a := Nat.pos_of_ne_zero hfa + have hga : g a + 1 = f a := by + simp [g, Nat.sub_add_cancel hfa_pos] + have hupdate : Function.update g a (g a).succ = f := by + funext x + by_cases hxa : x = a + · subst x + simp [hga] + · simp [g, hxa] + have hsum_erase : + ∑ x ∈ s.erase a, g x = ∑ x ∈ s.erase a, f x := by + apply Finset.sum_congr rfl + intro x hx + have hxa : x ≠ a := ne_of_mem_erase hx + simp [g, hxa] + have hsum : + (∑ x ∈ s, g x).succ = ∑ x ∈ s, f x := by + rw [← Finset.sum_erase_add _ ha, ← Finset.sum_erase_add _ ha] + rw [hsum_erase] + omega + have hmul := Nat.succ_mul_multinomial (s := s) (f := g) ha + refine ⟨Nat.multinomial s g, ?_⟩ calc - (k + 1) * - (((k + 1) + r).choose (k + 1) * - Nat.multinomial (s.erase a) f) = - (((k + r) + 1).choose (k + 1) * (k + 1)) * - Nat.multinomial (s.erase a) f := by ring - _ = (((k + r) + 1) * (k + r).choose k) * - Nat.multinomial (s.erase a) f := by rw [← hchoose] - _ = ((k + 1) + r) * - ((k + r).choose k * Nat.multinomial (s.erase a) f) := by ring + f a * Nat.multinomial s f = + (g a).succ * + Nat.multinomial s (Function.update g a (g a).succ) := by + rw [hupdate] + _ = (∑ x ∈ s, g x).succ * Nat.multinomial s g := hmul.symm + _ = (∑ x ∈ s, f x) * Nat.multinomial s g := by rw [hsum] /-- The six symbols in the Raney-word interpretation. -/ inductive HyperLetter From ca03b71938770282cde42aee9e017dc18c0d3f8a Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 02:59:43 -0700 Subject: [PATCH 30/30] Use the current factorial divisibility theorem --- proofs/geode5/Geode5CastBridges.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/proofs/geode5/Geode5CastBridges.lean b/proofs/geode5/Geode5CastBridges.lean index 0f604777..f4c4de93 100644 --- a/proofs/geode5/Geode5CastBridges.lean +++ b/proofs/geode5/Geode5CastBridges.lean @@ -40,7 +40,7 @@ theorem multinomial4_denominator_dvd (a b c d : ℕ) : Nat.factorial a * Nat.factorial b * Nat.factorial c * Nat.factorial d ∣ Nat.factorial (a + b + c + d) := by simpa [fourCounts, mul_assoc, add_assoc, add_comm, add_left_comm] using - (Nat.multinomial_dvd_factorial (s := Finset.univ) (fourCounts a b c d)) + (Nat.prod_factorial_dvd_factorial_sum Finset.univ (fourCounts a b c d)) /-- Cast of `multinomial4` equals the exact rational factorial quotient. -/ theorem cast_multinomial4_eq_qMultinomial4 (a b c d : ℕ) : @@ -67,9 +67,9 @@ theorem cast_geode5Diagonal_eq_qGeode5Diagonal (n : ℕ) : apply Finset.sum_congr rfl intro j₂ hj₂ apply Finset.sum_congr rfl - intro _ _ + intro j₃ hj₃ apply Finset.sum_congr rfl - intro _ _ + intro j₄ hj₄ apply Finset.sum_congr rfl intro j₅ hj₅ rw [cast_multinomial4_eq_qMultinomial4,