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

技術要約：形式化された $q$-級数：ロジャース・ラマヌジャン恒等式とその先へ

問題提起
$q$-級数および基本超幾何級数の理論は、組合せ論、数論、および表現論の重要な交差点となっている。しかし、これらを証明助手（proof assistant）において形式化することには特有の課題が存在する。古典的な数学的記法は、形式的冪級数、収束する解析関数、および様々な環における代数的恒等式の間の決定的な区別をしばしば省略している。人間の読者は、$q$-級数の恒等式を形式的級数の等式として、あるいは単位円上の解析関数の定理として、あるいは分割に関する言明として、自在に解釈して読み進めることができる。対照的に、証明助手はすべての遷移を明示的に行う必要があり、収束、強制（coercion）、および添字の慣習に関する厳密な定義を要求する。本論文が取り組む主要な問題は、深い数論的応用を可能にするための汎用性を損なうことなく、代数的および解析的な視点を調和させる、Lean証明助手におけるスケーラブルで多用途な形式的フレームワークの構築である。

手法と設計原理
著者らは、代数的な汎用性を優先しつつ、特定の位相構造を通じて解析的な収束を許容する、Lean（mathlibを基盤とする）によるライブラリを開発した。

• 代数的側面と解析的側面の分離： 解析的な収束を複雑にする複素解析関数を直接扱うのではなく、著者らは非アルキメデス環を用いることで、理論を代数的なものへと変換した。著者らは、新しいクラスの環である StrongNonarchimedeanRing を導入した。これは、単位元を持たない開加法的部分環が0の近傍の基底を形成する位相環である。この構造は十分に強力であり、$a_n \to 0$ であれば、無限積 $\prod (1+a_n)$ が収束することを保証する（これは一般的な非アルキメデス環では保証されない性質である）。
• 「ジャンク値（Junk Values）」の扱い： mathlib の哲学に従い、著者らは、要素が可逆でない場合に（例えば 1 などの）「ジャンク値」を返すような bInv などの関数を定義した。これにより、データの定義と証明を分離し、論理的な厳密性を維持しながら、より簡潔な記述を可能にした。
• 普遍的な環と多変数ローラン級数： Jacobiの三重積恒等式に含まれる負の冪（例：$z^{-1}$）を扱うため、著者らは特定の順序群上のハーン級数を用いた多変数ローラン級数の理論を実装した。これにより、係数の抽出が可能となり、「全次数」によって誘導される位相の下で環が完備であることを保証している。
• コア・プリミティブ： ライブラリは、$q$-整数、$q$-階乗、$q$-二項係数、および（有限および無限の）$q$-ポッホマーマー記号を含む基本的な対象を形式化している。極めて重要なことに、これらの定義は関手的（functorial）であり、環準同型の下で正しく振る舞う。
• ベイリーの補題（Bailey's Lemma）： 形式化の中心的な構成要素は、ベイリー対（Bailey pairs）およびベイリーの補題の実装である。著者らは、既存のベイリー対から新しいベイリー対を生成する変換機構を形式化した。これには、パラメータが無限大に発散する極限ケースも含まれる。これは、中間的な代数的ステップにおいて位相的な仮定を回避するために、$q$-Pfaff–Saalschütz恒等式の「分母除去済み（denominator-cleared）」バージョンを用いて達成された。

主な貢献と結果
本論文は、以下の2つの分野における画期的な結果の完全な検証済み証明を提供することで、このインフラストラクチャの有用性を実証している。

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)$$
   彼らのアプローチは、標準的な形式を、$b, c, q$ が $bc=q$を満たす設定へと一般化している。ここでは、$q$ が完全なStrongNonarchimedeanRingにおいて位相的に冪零であれば、$b$ または $c$ が可逆である必要はない。証明は「核となる本質（core essence）」の補題、すなわち $\mathbb{Z}[[q]]$ における可算な冪級数恒等式の族に基づき、それが位相的な設定へと一般化されている。

2. ロジャース・ラマヌジャン恒等式： 本論文は、以下の2つの有名な和・積恒等式に対する形式的な証明を提供している：
   $$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}$$
   形式的な証明は、ライブラリのベイリーの補題の実装を利用している。著者らは特定のベイリー対 $(\alpha_n, \beta_n)$ を定義し、ベイリーの補題の極限形式を2回適用し、Jacobiの三重積を用いて、結果として得られる級数を無限積展開と一致させている。このプロセスは、非自明な再添字、収束制御、および超幾何変換と積展開のインターフェースを扱うライブラリの能力を検証している。

3. 系： おまけとして、著者らは、形式化されたJacobiの三重積恒等式の直接的な帰結として、オイラーの五角数定理およびJacobiのオイラー関数の3乗に関する恒等式を導出し、検証した。

意義と主張
本論文は、本研究を数論および数理物理学の高度なトピックの形式化に向けた基礎的な一歩として位置づけている。著者らは、その形式化が以下の点において寄与すると主張している：

• 厳密な計算基盤の確立： 代数的な骨格と解析的な仮定を分離することで、ライブラリは将来の研究のための堅牢なフレームワークを提供する。
• 将来の形式化の実現： 著者らは、このインフラストラクチャが、モック・テータ関数、モジュラー形式、およびそれらの応用を支える多様な代数的構造の形式化をサポートするように設計されていることを明示している。
• 一般の環上のモジュラー形式のサポート： （強）非アルキメデス環で作業することにより、本形式化は、$p$ 進モジュラー形式や、一般の環（KatzやSerreの意味での）上のモジュラー形式の研究への道を開く。これは、モジュラー形式の係数の合同式に関する結果を形式化する上で極めて重要である。
• ベンチマークとしての役割： 有限および無限の積、再添字、および収束の複雑な相互作用を必要とするロジャース・ラマヌジャン恒等式の形式化成功は、開発されたライブラリのスケーラビリティと汎用性を実証している。

本研究は、$q$-級数の未解決問題を解決することを目的としているのではなく、数学者が機械照合された証明の確信を持ってこれらの領域を探索するために必要な、検証済みで再利用可能な道具立てを提供することを目的としている。