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

技术摘要：形式化 $q$-级数：Rogers-Ramanujan 恒等式及其延伸

问题陈述
$q$-级数与基本超几何级数理论是组合数学、数论与表示论的一个关键交汇点。然而，在证明辅助器（proof assistants）中形式化这一理论面临着独特的挑战。经典的数学符号往往忽略了形式幂级数、收敛解析函数以及各种环中的代数恒等式之间的关键区别。人类读者可以流利地在将一个 $q$-级数恒等式解释为形式级数的等式、关于单位圆盘内解析函数的定理、或关于分区的陈述之间进行切换。相比之下，证明辅助器要求每一个转换都必须是显式的，要求对收敛性、强制转换（coercions）和索引约定进行严谨的定义。本文解决的核心问题是：如何在 Lean 证明辅助器中构建一个可扩展且通用的形式化框架，既能协调这些代数与解析视角，又不牺牲深度数论应用所需的普适性。

方法论与设计原则
作者开发了一个基于 Lean（构建于 mathlib 之上）的库，该库优先考虑代数上的普适性，同时通过特定的拓扑结构来容纳解析收敛性。

• 代数与解析的分离： 作者并未直接处理复杂的解析函数（这会增加代数操作的复杂度），而是利用非阿基米德环将该理论转化为代数理论。他们引入了一种新的环类——强非阿基米德环（StrongNonarchimedeanRing）。这是一种拓扑环，其开加法子环（不含单位元）构成了 0 的邻域基。这种结构足够强大，能够保证如果序列 $a_n \to 0$，则无穷乘积 $\prod (1+a_n)$ 收敛，而这一性质在一般的非阿基米德环中并不一定成立。
• 处理“无效值”（Junk Values）： 遵循 mathlib 的哲学，作者定义了如乘法逆（bInv）之类的函数，当元素不可逆时返回一个“无效值”（例如 1），而不是限制定义域。这种做法实现了数据与证明的分离，在保持逻辑严密性的同时使陈述更加简洁。
• 通用环与多元洛朗级数： 为了处理涉及负幂次的恒等式（例如 Jacobi 三重积中的 $z^{-1}$），作者利用特定有序群上的 Hahn 级数实现了一套多元洛朗级数理论。这使得提取系数成为可能，并确保该环在由“总次数”诱导的拓扑下是完备的。
• 核心原语： 该库形式化了包括 $q$-整数、$q$-阶乘、$q$-二项式系数以及 $q$-Pochhammer 符号（包括有限和无限形式）在内的基本对象。至关重要的是，这些定义是函子的（functorial），这意味着它们在环同态下表现正确。
• Bailey 引理： 形式化的核心组件是 Bailey 对（Bailey pairs）及其引理的实现。作者形式化了从现有 Bailey 对生成新 Bailey 对的变换机制，包括参数趋于无穷大的极限情况。这是通过使用 $q$-Pfaff–Saalschütz 恒等式的“分母消除”版本实现的，以避免在中间代数步骤中引入拓扑假设。

主要贡献与结果
本文通过提供两个领域内里程碑式结果的完全验证证明，展示了该基础设施的效用：

1. Jacobi 三重积恒等式： 作者形式化了如下恒等式的证明：
   $$\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)$$
   他们的方法将标准形式推广到了满足 $bc=q$的设定中，且无需要求$b$或$c$可逆，只要$q$在完备的强非阿基米德环中是拓扑幂零的。该证明依赖于一个“核心本质”引理：即$\mathbb{Z}[[q]]$ 中一系列可数幂级数恒等式的集合，随后将其推广到拓扑设定中。

2. Rogers-Ramanujan 恒等式： 本文为两个著名的求和-乘积恒等式提供了形式化证明：
   $$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}$$
   形式化证明利用了库中实现的 Bailey 引理。作者定义了特定的 Bailey 对 $(\alpha_n, \beta_n)$，两次应用 Bailey 引理的极限形式，并使用 Jacobi 三重积将所得级数与无穷乘积展开式进行识别。这一过程验证了该库处理非平凡重索引、收敛控制以及超几何变换与乘积展开之间接口的能力。

3. 推论： 作为附加成果，作者将 Euler 五边形数定理和 Jacobi 关于 Euler 函数立方体的恒等式作为形式化 Jacobi 三重积的直接推论进行了推导与验证。

意义与主张
本文将此工作定位为形式化数论与数学物理高级课题的基础性步骤。作者声称其形式化工作具有以下意义：

• 建立了严密的计算基础： 通过将代数骨架与解析假设分离，该库为未来的工作提供了一个稳健的框架。
• 赋能未来的形式化工作： 作者明确指出，该基础设施旨在支持对 mock theta 函数、模形式以及支撑其应用的各种代数结构的正式化。
• 支持一般环上的模形式： 通过在（强）非阿基米德环中工作，该形式化为研究 $p$ 进模形式以及一般环上的模形式（如 Katz 或 Serre 意义下的模形式）铺平了道路，这对于形式化模形式系数的同余性质至关重要。
• 作为基准测试： 成功形式化 Rogers-Ramanujan 恒等式（该恒等式涉及复杂的有限与无限乘积、重索引及收敛性控制）证明了所开发库的可扩展性与多功能性。

这项工作并不声称解决了 $q$-级数中的开放问题，而是提供了一套经过验证的、可复用的工具，使数学家能够以机器检查证明的确定性来探索这些领域。