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

기술 요약: 정형화된 q-급수: 로저스-라마누잔 항등식과 그 너머

문제 정의
$q$-급수 및 기본 초기하 급수 이론은 조합론, 정수론, 표현론이 교차하는 중요한 지점이다. 그러나 이 이론을 증명 보조기(proof assistant)에서 정형화하는 것은 독특한 과제를 안겨준다. 고전적인 수학적 표기법은 형식적 멱급수, 수렴하는 해석 함수, 그리고 다양한 환(ring)에서의 대수적 항등식 사이의 결정적인 차이를 묵인하는 경-향이 있다. 인간 독자는 $q$-급수 항등식을 형식적 급수의 등식, 단위 원판 위의 해석 함수의 정리, 또는 분할(partition)에 관한 진술로 자유롭게 해석하며 넘나들 수 있다. 반면, 증명 보조기는 모든 전이를 명시적으로 요구하며, 수렴성, 강제 변환(coercion), 인덱싱 관례에 대한 엄격한 정의를 요구한다. 본 논문이 다루는 주요 문제는, 심도 있는 정수론적 응용에 필요한 일반성을 희생하지 않으면서도 대수적 관점과 해석적 관점을 조화시키는 Lean 증명 보조기 기반의 확장 가능하고 다재다능한 정형 프레임워크를 구축하는 것이다.

방법론 및 설계 원칙
저자들은 대수적 일반성을 우선시하면서도 특정 위상 구조를 통해 해석적 수렴을 수용하는 Lean 기반의 라이브러리(mathlib 구축)를 개발하였다.

• 대수적 vs 해석적 분리: 대수적 조작을 복잡하게 만드는 복소 해석 함수를 직접 다루는 대신, 저자들은 비아르키메데스 환(non-Archimedean rings)을 사용하여 이론을 대수적인 것으로 변환하였다. 저자들은 StrongNonarchimedeanRing이라는 새로운 클래스의 환을 도입하였는데, 이는 열린 가법 부분환(단위원을 포함하지 않는)이 0의 근방에 대한 기저를 형성하는 위상 환이다. 이 구조는 강력하여, 만약 수열 $a_n \to 0$이면 무한 곱 $\prod (1+a_n)$이 수렴함을 보장한다. 이는 일반적인 비아르키메데스 환에서는 보장되지 않는 성질이다.
• "정크 값(Junk Values)" 처리: mathlib의 철학을 따라, 저자들은 역원이 존재하지 않을 때 "정크 값"(예: 1)을 반환하는 bInv와 같은 함수를 정의하여 도메인을 제한하는 대신 데이터와 증명을 분리하였다. 이를 통해 논리적 엄밀성을 유지하면서도 더 깔끔한 진술을 가능하게 하였다.
• 보편적 환 및 다변량 로랑 급수: $z^{-1}$과 같이 음수 차수를 포함하는 항등식(Jacobi Triple Product의 경우 등)을 처리하기 위해, 저자들은 특정 순서 군(ordered group) 상의 Hahn 급수를 사용하는 다변량 로랑 급수 이론을 구현하였다. 이를 통해 계수를 추출하고 "전체 차수(total degree)"에 의해 유도된 위상 하에서 환이 완비됨을 보장한다.
• 핵심 프리미티브(Core Primitives): 라이브러리는 $q$-정수, $q$-계승, $q$-이항 계수, 그리고 $q$-포코하머 기호(유한 및 무한 형태 모두)를 포함한 기초적인 대상들을 정형화한다. 결정적으로, 이러한 정의들은 함수적(functorial)이다. 즉, 환 준동형 사상 하에서도 올바르게 동작한다.
• 베일리 보조정리(Bailey's Lemma): 정형화의 핵심 요소는 베일리 쌍(Bailey pairs)과 베일리 보조정리의 구현이다. 저자들은 기존의 베일리 쌍으로부터 새로운 베일리 쌍을 생성하는 변환 메커니즘을 정형화하였으며, 여기에는 파라미터가 무한대로 가는 극한 사례도 포함된다. 이는 중간 대수적 단계에서 위상적 가정을 피하기 위해 $q$-Pfaff–Saalschütz 항등식의 "분모 제거된(denominator-cleared)" 버전을 사용하여 달성되었다.

주요 기여 및 결과
본 논문은 다음 두 가지 기념비적인 결과의 완전 검증된 증명을 제공함으로써 이 인프라의 유용성을 입증한다:

1. 야코비 삼중 곱 항등식(Jacobi Triple Product Identity): 저자들은 다음 항등식의 증명을 정형화하였다:
   $$\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$를 만족할 때,$b$나$c$의 역원이 존재할 필요 없이$q$가 완전한(complete) StrongNonarchimedeanRing에서 위상적으로 멱영(topologically nilpotent)이라면 일반화되는 표준 형태를 다룬다. 이 증명은 $\mathbb{Z}[[q]]$에서의 가산 멱급수 항등식 집합인 "핵심 본질(core essence)" 렘마에 의존하며, 이후 이를 위상적 환경으로 일반화한다.

2. 로저스-라마누잔 항등식(Rogers-Ramanujan Identities): 본 논문은 두 유명한 합-곱 항등식에 대한 정형 증명을 제공한다:
   $$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)$을 정의하고, 베일리 보조정리의 극한 형태를 두 번 적용하며, 야코비 삼중 곱을 사용하여 결과 급수를 무한 곱 전개와 일치시킨다. 이 과정은 비사소한 재인덱싱, 수렴 제어, 그리고 초기하 변환과 곱 전개 사이의 인터페이스를 처리하는 라이브러리의 능력을 검증한다.

3. 따름정리: 보너스로, 저자들은 정형화된 야코비 삼중 곱으로부터 오일러의 오각형 수 정리(Euler's Pentagonal Number Theorem)와 야코비의 오일러 함수 세제곱 항등식을 직접적인 결과로서 도출하고 검증하였다.

의의 및 주장
본 논문은 이 작업이 고급 정수론 및 수학 물리학 주제의 정형화를 위한 기초적인 단계임을 위치시킨다. 저자들은 자신들의 정형화가 다음과 같은 기능을 수행한다고 주장한다:

• 엄격한 계산적 토대 구축: 대수적 골격과 해석적 가설을 분리함으로써, 라이브러리는 향후 연구를 위한 견고한 프레임워크를 제공한다.
• 미래의 정형화 지원: 이 인프라는 모크 세타 함수(mock theta functions), 모듈러 형식(modular forms), 그리고 그 응용을 뒷받는 다양한 대수적 구조의 정형화를 지원하도록 설계되었다.
• 일반 환 상의 모듈러 형식 지원: 비아르키메데스(강한 의미의) 환에서 작업함으로써, 본 정형화는 $p$-진 모듈러 형식 및 일반적인 환(Katz 또는 Serre의 의미에서) 상의 모듈러 형식을 연구할 수 있는 길을 열어주며, 이는 모듈러 형식 계수의 합동식에 관한 결과를 정형화하는 데 매우 중요하다.
• 벤치마크 역할: 유한 및 무한 곱, 재인덱싱, 수렴의 복잡한 상호작용을 요구하는 로저스-라마누잔 항등식의 성공적인 정형화는 개발된 라이브러리의 확장성과 다재다능함을 입증한다.

본 연구는 $q$-급수의 미해결 문제를 해결하는 것을 목표로 하는 것이 아니라, 수학자들이 기계 검증된 증명의 확신을 가지고 이 분야를 탐구할 수 있도록 필요한 검증되고 재사용 가능한 기계(machinery)를 제공하는 데 목적이 있다.