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

Résumé Technique : Séries en $q$ formalisées : Les identités de Rogers-Ramanujan et au-delà

Énoncé du problème
La théorie des séries en $q$ et des séries hypergéométriques basiques constitue une intersection critique entre la combinatoire, la théorie des nombres et la théorie des représentations. Cependant, la formalisation de cette théorie dans les assistants de preuve présente des défis uniques. La notation mathématique classique occulte souvent des distinctions cruciales entre les séries formelles de puissances, les fonctions analytiques convergentes et les identités algébriques dans divers anneaux. Un lecteur humain peut passer fluidement d'une interprétation d'une identité de série en $q$ comme égalité de séries formelles, à un théorème sur des fonctions analytiques sur le disque unité, ou à une affirmation concernant les partitions. En revanche, un assistant de preuve exige que chaque transition soit explicite, demandant des définitions rigoureuses de la convergence, des coercitions et des conventions d'indexation. Le problème principal traité dans cet article est la construction d'un cadre formel évolutif et polyvalent dans l'assistant de preuve Lean qui réconcilie ces perspectives algébriques et analytiques sans sacrifier la généralité requise pour les applications approfondies de la théorie des nombres.

Méthodologie et principes de conception
Les auteurs ont développé une bibliothèque formelle dans Lean (s'appuyant sur mathlib) qui privilégie la généralité algébrique tout en accommodant la convergence analytique par le biais de structures topologiques spécifiques.

• Séparation Algébrique vs Analytique : Plutôt que de travailler directement avec des fonctions analytiques complexes, ce qui complique la manipulation algébrique, les auteurs ont transformé la théorie en une théorie algébrique utilisant des anneaux non archimédiens. Ils ont introduit une nouvelle classe d'anneaux, StrongNonarchimedeanRing, qui est un anneau topologique où les sous-anneaux additifs ouverts (sans unité) forment une base pour les voisinages de 0. Cette structure est suffisamment forte pour garantir que si une suite $a_n \to 0$, alors le produit infini $\prod (1+a_n)$ converge, une propriété qui n'est pas garantie dans les anneaux non archimédiens généraux.
• Gestion des « Valeurs Junk » : Adhérant à la philosophie de mathlib, les auteurs ont défini des fonctions comme les inverses multiplicatifs (bInv) pour retourner une « valeur junk » (par exemple, 1) lorsqu'un élément n'est pas inversible, plutôt que de restreindre le domaine. Cela sépare les données des preuves, permettant des énoncés plus clairs tout en maintenant la rigueur logique.
• Anneaux Universels et Séries de Laurent Multivariées : Pour gérer les identités impliquant des puissances négatives (par exemple, $z^{-1}$ dans le Produit Triple de Jacobi), les auteurs ont implémenté une théorie des séries de Laurent multivariées utilisant des séries de Hahn sur un groupe ordonné spécifique. Cela permet l'extraction de coefficients et garantit que l'anneau est complet sous une topologie induite par le « degré total ».
• Primitives Centrales : La bibliothèque formalise des objets fondamentaux incluant les $q$-entiers, les $q$-factorielles, les coefficients $q$-binomiaux et les symboles $q$-Pochhammer (tant finis qu'infinis). Crucialement, ces définitions sont fonctorelles, ce qui signifie qu'elles se comportent correctement sous les homomorphismes d'anneaux.
• Lemme de Bailey : Un composant central de la formalisation est l'implémentation des paires de Bailey et du Lemme de Bailey. Les auteurs ont formalisé la machinerie de transformation qui génère de nouvelles paires de Bailey à partir de paires existantes, incluant les cas limites où les paramètres tendent vers l'infini. Ceci a été réalisé en utilisant une version « à dénominateur éliminé » de l'identité $q$-Pfaff–Saalschütz afin d'éviter les hypothèses topologiques lors des étapes algébriques intermédiaires.

Contributions clés et résultats
L'article démontre l'utilité de cette infrastructure en fournissant des preuves entièrement vérifiées de deux résultats marquants dans le domaine :

1. L'Identité du Produit Triple de Jacobi : Les auteurs ont formalisé la preuve de l'identité :
   $$\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)$$
   Leur approche généralise la forme standard à un cadre où $b, c, q$ satisfont $bc=q$ sans exiger que $b$ ou $c$ soit inversible, à condition que $q$ soit topologiquement nilpotent dans un StrongNonarchimedeanRing complet. La preuve repose sur un lemme d'« essence centrale » : une famille dénombrable d'identités de séries de puissances dans $\mathbb{Z}[[q]]$ qui sont ensuite généralisées au cadre topologique.

2. Les Identités de Rogers-Ramanujan : L'article fournit des preuves formelles pour les deux célèbres identités somme-produit :
   $$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}$$
   La preuve formelle utilise l'implémentation du Lemme de Bailey de la bibliothèque. Les auteurs définissent des paires de Bailey spécifiques $(\alpha_n, \beta_n)$, appliquent la forme limite du Lemme de Bailey deux fois, et utilisent le Produit Triple de Jacobi pour identifier les séries résultantes avec les développements en produits infinis. Ce processus valide la capacité de la bibliothèque à gérer le réindexage non trivial, le contrôle de la convergence, et l'interface entre les transformations hypergéométriques et les développements de produits.

3. Corollaires : En guise de bonus, les auteurs ont dérivé et vérifié le Théorème des Nombres Pentagonaux d'Euler et l'identité de Jacobi pour le cube de la fonction d'Euler comme conséquences directes du Produit Triple de Jacobi formalisé.

Signification et Revendications
L'article positionne ce travail comme une étape fondamentale vers la formalisation de sujets avancés de la théorie des nombres et de la physique mathématique. Les auteurs affirment que leur formalisation :

• Établit une Fondation Computationnelle Rigoureuse : En séparant les squelettes algébriques des hypothèses analytiques, la bibliothèque fournit un cadre robuste pour des travaux futurs.
• Permet des Formalisations Futures : Les auteurs déclarent explicitement que cette infrastructure est conçue pour soutenir la formalisation des fonctions theta mock, des formes modulaires, et des diverses structures algébriques sous-tendant leurs applications.
• Supporte les Formes Modulaires sur des Anneaux Généraux : En travaillant dans des anneaux (fortement) non archimédiens, la formalisation ouvre la voie à l'étude des formes modulaires $p$-adiques et des formes modulaires sur des anneaux généraux (au sens de Katz ou Serre), ce qui est crucial pour formaliser les résultats sur les congruences des coefficients des formes modulaires.
• Sert de Référence : La formalisation réussie des identités de Rogers-Ramanujan, qui nécessitent une interaction complexe entre produits finis et infinis, le réindexage et la convergence, démontre la scalabilité et la polyvalence de la bibliothèque développée.

Le travail ne prétend pas résoudre des problèmes ouverts de séries en $q$, mais plutôt fournir la machinerie vérifiée et réutilisable nécessaire pour que les mathématiciens explorent ces domaines avec la certitude de preuves vérifiées par machine.