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

Resumen Técnico: Series $q$ Formalizadas: Las Identidades de Rogers-Ramanujan y Más Allá

Planteamiento del Problema
La teoría de las series $q$ y las series hipergeométricas básicas sirve como una intersección crítica para la combinatoria, la teoría de números y la teoría de la representación. Sin embargo, la formalización de esta teoría en asistentes de pruebas presenta desafíos únicos. La notación matemática clásica suele omitir distinciones cruciales entre series de potencias formales, funciones analíticas convergentes e identidades algebraicas en diversos anillos. Un lector humano puede transitar fluidamente entre interpretar una identidad de series $q$ como una igualdad de series formales, un teorema sobre funciones analíticas en el disco unidad o una declaración sobre particiones. En contraste, un asistente de pruebas requiere que cada transición sea explícita, exigiendo definiciones rigurosas de convergencia, coerciones y convenciones de indexación. El problema principal abordado en este artículo es la construcción de un marco formal escalable y versátil en el asistente de pruebas Lean que reconcilie estas perspectivas algebraicas y analíticas sin sacrificar la generalidad requerida para aplicaciones profundas de la teoría de números.

Metodología y Principios de Diseño
Los autores desarrollaron una biblioteca formal en Lean (basada en mathlib) que prioriza la generalidad algebraica al tiempo que acomoda la convergencia analítica mediante estructuras topológicas específicas.

• Separación Algebraica vs. Analítica: En lugar de trabajar directamente con funciones analíticas complejas, lo que complica la manipulación algebraica, los autores transformaron la teoría en una algebraica utilizando anillos no arquimedianos. Introdujeron una nueva clase de anillos, StrongNonarchimedeanRing, que es un anillo topológico donde los subanillos aditivos abiertos (sin unidad) forman una base para los entornos de 0. Esta estructura es lo suficientemente fuerte como para garantizar que si una secuencia $a_n \to 0$, entonces el producto infinito $\prod (1+a_n)$ converge, una propiedad que no se garantiza en anillos no arquimedianos generales.
• Manejo de "Valores Basura" (Junk Values): Adheriéndose a la filosofía de mathlib, los autores definieron funciones como los inversos multiplicativos (bInv) para que devuelvan un "valor basura" (por ejemplo, 1) cuando un elemento no es invertible, en lugar de restringir el dominio. Esto separa los datos de las pruebas, permitiendo declaraciones más limpias manteniendo la rigurosidad lógica.
• Anillos Universales y Series de Laurent Multivariables: Para manejar identidades que involucran potencias negativas (por ejemplo, $z^{-1}$ en el Producto Triple de Jacobi), los autores implementaron una teoría de series de Laurent multivariables utilizando series de Hahn sobre un grupo ordenado específico. Esto permite la extracción de coeficientes y asegura que el anillo sea completo bajo una topología inducida por el "grado total".
• Primitivos Centrales: La biblioteca formaliza objetos fundamentales incluyendo enteros $q$, factoriales $q$, coeficientes $q$-binomiales y símbolos $q$-Pochhammer (tanto finitos como infinitos). Crucialmente, estas definiciones son de naturaleza funcional, lo que significa que se comportan correctamente bajo homomorfismos de anillos.
• Lema de Bailey: Un componente central de la formalización es la implementación de pares de Bailey y el Lema de Bailey. Los autores formalizaron la maquinaria de transformación que genera nuevos pares de Bailey a partir de los existentes, incluyendo los casos límite donde los parámetros tienden al infinito. Esto se logró utilizando una versión del producto $q$-Pfaff–Saalschütz con el "denominador eliminado" para evitar suposiciones topológicas durante los pasos algebraicos intermedios.

Contribuciones Clave y Resultados
El artículo demuestra la utilidad de esta infraestructura proporcionando pruebas totalmente verificadas de dos resultados fundamentales en el campo:

1. La Identidad del Producto Triple de Jacobi: Los autores formalizaron una prueba de la identidad:
   $$\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)$$
   Su enfoque generaliza la forma estándar a un entorno donde $b, c, q$ satisfacen $bc=q$ sin requerir que $b$ o $c$ sean invertibles, siempre que $q$ sea topológicamente nilpotente en un StrongNonarchimedeanRing completo. La prueba se basa en un lema de "esencia central": una familia contable de identidades de series de potencias en $\mathbb{Z}[[q]]$ que luego se generalizan al entorno topológico.

2. Las Identidades de Rogers-Ramanujan: El artículo proporciona pruebas formales para las dos famosas identidades de suma-producto:
   $$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 prueba formal utiliza la implementación de la biblioteca del Lema de Bailey. Los autores definen pares de Bailey específicos $(\alpha_n, \beta_n)$, aplican la forma límite del Lema de Bailey dos veces y utilizan el Producto Triple de Jacobi para identificar las series resultantes con las expansiones de productos infinitos. Este proceso valida la capacidad de la biblioteca para manejar la reindexación no trivial, el control de convergencia y la interfaz entre las transformaciones hipergeométricas y las expansiones de productos.

3. Corolarios: Como un beneficio adicional, los autores derivaron y verificaron el Teorema del Número Pentagonal de Euler y la identidad de Jacobi para el cubo de la función de Euler como consecuencias directas del Producto Triple de Jacobi formalizado.

Significación y Reivindicaciones
El artículo posiciona este trabajo como un paso fundacional hacia la formalización de temas avanzados de la teoría de números y la física matemática. Los autores afirman que su formalización:

• Establece una Base Computacional Rigurosa: Al separar los esqueletos algebraicos de las hipótesis analíticas, la biblioteca proporciona un marco robusto para trabajos futuros.
• Permite Formalizaciones Futuras: Los autores declaran explícitamente que esta infraestructura está diseñada para soportar la formalización de funciones theta mock, formas modulares y las diversas estructuras algebraicas que sustentan sus aplicaciones.
• Soporta Formas Modulares sobre Anillos Generales: Al trabajar en anillos (fuertemente) no arquimedianos, la formalización allana el camino para estudiar formas modulares $p$-ádicas y formas modulares sobre anillos generales (en el sentido de Katz o Serre), lo cual es crucial para formalizar resultados sobre congruencias de coeficientes de formas modulares.
• Sirve como Punto de Referencia: La formalización exitosa de las identidades de Rogers-Ramanujan, que requieren una compleja interacción de productos finitos e infinitos, reindexación y convergencia, demuestra la escalabilidad y versatilidad de la biblioteca desarrollada.

El trabajo no pretende resolver problemas abiertos de series $q$, sino proporcionar la maquinaria verificada y reutilizable necesaria para que los matemáticos exploren estas áreas con la certeza de las pruebas verificadas por máquina.