Formalized $q$-series: The Rogers-Ramanujan Identities and Beyond

Technische Samenvatting: Formalisering van q-reeksen: De Rogers-Ramanujan Identiteiten en Verder

Probleemstelling
De theorie van $q$-reeksen en basis hypergeometrische series vormt een cruciaal snijvlak voor combinatoriek, getaltheorie en representatietheorie. Het formaliseren van deze theorie in bewijsassistenten presenteert echter unieke uitdagingen. Klassieke wiskundige notatie onderdrukt vaak cruciale onderscheiden tussen formele machtreeksen, convergente analytische functies en algebraïsche identiteiten in verschillende ringen. Een menselijke lezer kan vloeiend schakelen tussen het interpreteren van een $q$-reeks identiteit als een gelijkheid van formele reeksen, een stelling over analytische functies op de eenheidsschijf, of een uitspraak over partities. In tegenstelling hiertoe vereist een bewijsassistent elke transitie expliciet, wat rigoureuze definities van convergentie, coercities en indexeringsconventies eist. Het primaire probleem dat in dit artikel wordt behandeld, is de constructie van een schaalbaar, veelzijdig formeel kader in de Lean bewijsassistent dat deze algebraïsche en analytische perspectieven verenigt zonder het algemeenheid vereist voor diepe getaltheoretische toepassingen op te offeren.

Methodologie en Ontwerpprincipes
De auteurs hebben een formele bibliotheek ontwikkeld in Lean (gebouwd op mathlib) die prioriteit geeft aan algebraïsche algemeenheid terwijl zij analytische convergentie faciliteert via specifieke topologische structuren.

• Scheiding van Algebraïsch versus Analytisch: In plaats van direct te werken met complexe analytische functies, wat algebraïsche manipulatie bemoeilijkt, hebben de auteurs de theorie getransformeerd naar een algebraïsche theorie met behulp van niet-Archimedische ringen. Ze introduceerden een nieuwe klasse ringen, de StrongNonarchimedeanRing, die een topologische ring is waarbij open additieve subringen (zonder eenheid) een basis vormen voor de omgevingen van 0. Deze structuur is sterk genoeg om te garanderen dat als een sequentie $a_n \to 0$, de oneindige product $\prod (1+a_n)$ convergeert, een eigenschap die in algemene niet-Archimedische ringen niet gegarandeerd is.
• Omgaan met "Junk Values": In lijn met de filosofie van mathlib hebben de auteurs functies zoals multiplicatieve inversen (bInv) gedefinieerd die een "junk waarde" (bijv. 1) teruggeven wanneer een element niet inversibel is, in plaats van het domein te beperken. Dit scheidt data van bewijzen, wat zorgt voor schonere stellingen terwijl de logische rigor behouden blijft.
• Universele Ringen en Multivariate Laurent-reeksen: Om identiteiten te behandelen die negatieve machten bevatten (bijv. $z^{-1}$ in de Jacobi Triple Product), hebben de auteurs een theorie van multivariate Laurent-reeksen geïmplementeerd met behulp van Hahn-reeksen over een specifieke geordende groep. Dit maakt het mogelijk om coëfficiënten te extraheren en garandeert dat de ring compleet is onder een topologie geïnduceerd door de "totale graad".
• Kernprimitieven: De bibliotheek formaliseert fundamentele objecten waaronder $q$-integers, $q$-factorials, $q$-binomiale coëfficiënten en $q$-Pochhammer symbolen (zowel eindig als oneindig). Cruciaal is dat deze definities functorieel zijn, wat betekent dat ze correct gedragen onder ringhomomorfismen.
• Bailey's Lemma: Een centraal onderdeel van de formalisering is de implementatie van Bailey-paren en Bailey's Lemma. De auteurs hebben de transformatiemachinerie geformaliseerd die nieuwe Bailey-paren genereert uit bestaande paren, inclusclusief limietgevallen waarbij parameters naar oneindig tenderen. Dit werd bereikt met behulp van een "noemer-gezuiverde" versie van de $q$-Pfaff–Saalschütz identiteit om topologische aannames tijdens tussenliggende algebraïsche stappen te vermijden.

Belangrijkste Bijdragen en Resultaten
Het artikel demonstreert het nut van deze infrastructuur door het leveren van volledig geverifieerde bewijzen voor twee baanbrekende resultaten in het veld:

1. De Jacobi Triple Product Identiteit: De auteurs hebben een bewijs geformaliseerd van de identiteit:
   $$\sum_{n \in \mathbb{Z}} (-1)^n z^n q^{n(n-1)/2} = \prod_{m=1}^{\infty} (1-q^m)(1-zq^{m-1})(1-z^{-1}q^m)$$
   Hun aanpak generaliseert de standaardvorm naar een setting waar $b, c, q$ voldoen aan $bc=q$ zonder dat $b$ of $c$ inversibel hoeft te zijn, mits $q$ topologisch nilpotent is in een complete StrongNonarchimedeanRing. Het bewijs steunt op een "core essence" lemma: een tellbare familie van machtreeksidentiteiten in $\mathbb{Z}[[q]]$ die vervolgens worden gegeneraliseerd naar de topologische setting.

2. De Rogers-Ramanujan Identiteiten: Het artikel biedt formele bewijzen voor de twee beroemde som-product identiteiten:
   $$G(q) = \sum_{n \ge 0} \frac{q^{n^2}}{(q;q)_n} = \frac{1}{(q;q^5)_\infty (q^4;q^5)_\infty}$$
   $$H(q) = \sum_{n \ge 0} \frac{q^{n(n+1)}}{(q;q)_n} = \frac{1}{(q^2;q^5)_\infty (q^3;q^5)_\infty}$$
   Het formele bewijs maakt gebruik van de implementatie van Bailey's Lemma in de bibliotheek. De auteurs definiëren specifieke Bailey-paren $(\alpha_n, \beta_n)$, passen de limietvorm van Bailey's Lemma tweemaal toe, en gebruiken de Jacobi Triple Product om de resulterende reeks te identificeren met de oneindige productexpansies. Dit proces valideert het vermogen van de bibliotheek om complexe herindexering, convergentiecontrole en de interface tussen hypergeometrische transformaties en productexpansies te hanteren.

3. Corollaria: Als bonus hebben de auteurs de Euler Pentagonaal Getal Stelling en Jacobi's identiteit voor de kubus van de Euler-functie afgeleid en geverifieerd als directe consequenties van de geformaliseerde Jacobi Triple Product.

Betekenis en Claims
Het artikel positioneert dit werk als een fundamentele stap naar de formalisering van geavanceerde onderwerpen in de getaltheorie en de mathematische fysica. De auteurs claimen dat hun formalisering:

• Een Rigoureuze Computationele Basis Vestigt: Door algebraïsche skeletten te scheiden van analytische hypothesen, biedt de bibliotheek een robuust kader voor toekomstig werk.
• Toekomstige Formaliseringen Mogelijk Maakt: De auteurs stellen expliciet dat deze infrastructuur is ontworpen om de formalisering van mock theta functies, modulaire vormen en de diverse algebraïsche structuren die hun toepassingen onderbouwen te ondersteunen.
• Modulaire Vormen over Algemene Ringen Ondersteunt: Door te werken in (sterk) niet-Archimedische ringen, plaveit de formalisering de weg voor het bestuderen van $p$-adische modulaire vormen en modulaire vormen over algemene ringen (in de zin van Katz of Serre), wat cruciaal is voor het formaliseren van resultaten over congruenties van modulaire vorm coëfficiënten.
• Dient als Benchmark: De succesvolle formalisering van de Rogers-Ramanujan identiteiten, die een complexe interactie vereisen tussen eindige en oneindige producten, herindexering en convergentie, demonstreert de schaalbaarheid en veelzijdigheid van de ontwikkelde bibliotheek.

Het werk claimt geen openstaande problemen in de $q$-reeksen op te lossen, maar beoogt de geverifieerde, herbruikbare machinerie te bieden die nodig is voor wiskundigen om deze gebieden te verkennen met de zekerheid van door de machine gecontroleerde bewijzen.