发表机构
Emory University; Axiom Math（埃默里大学; Axiom数学公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明 Huang-Jiang-Oblomkov 猜想，通过有限恒等式将环面纽结奇点的 Rogers-Ramanujan 型恒等式与有界圆柱分拆生成函数联系起来，并给出 Lean 形式化证明。
AI 中文摘要
我们证明了 Huang、Jiang 和 Oblomkov (HJO) 的猜想，该猜想对每个具有互素 $1<a<b$ 的环面纽结奇点 $X^a=Y^b$ 给出了 Rogers--Ramanujan 和 Andrews--Gordon 恒等式的几何推广。对于素数幂 $q$，设 $\mathcal{NC}_n^{a,b}(\mathbb F_q)$ 表示 $\mathbb F_q$ 上满足 $A^a=B^b$ 的交换幂零 $n\times n$ 矩阵对 $(A,B)$ 的集合。我们建立了它们的归一化计数、HJO $q$-级数 $Z_{a,b}$ 和显式无穷乘积 $P_{a,b}$ 之间的三重等式：\\[ \underbrace{\vphantom{\Bigg|} \prod_{m\geq1}(1-q^{-m}) \Biggl(\sum_{n=0}^{\infty} \frac{\lvert\mathcal{NC}_n^{a,b}(\mathbb F_q)\rvert} {\lvert\operatorname{GL}_n(\mathbb F_q)\rvert}\Biggr) }_{\text{点计数}} = \underbrace{\vphantom{\Bigg|}Z_{a,b}(q^{-1}) }_{\text{\\(q\\)-级数}} = \underbrace{\vphantom{\Bigg|}P_{a,b}(q^{-1}) }_{\text{无穷乘积}}. \\] 我们的主要结果是一个更强的有限恒等式：秩 $N$ 的 HJO 和等于 $(q;q)_N$ 乘以条目以 $N$ 为界的平衡圆柱分拆的生成函数。令 $N\to\infty$ 即得 HJO 猜想。证明结合了 Bergeron--Garsia--Leven--Xin 和 Mellit 的组合有理洗牌定理、斜率算子的乘性定理以及有界圆柱分拆的行列式模型，它们通过一个共同的 $q$-差分方程联系起来。有限恒等式和 HJO 猜想已由 AxiomProver 在 Lean 中形式化，条件依赖于两个所述文献输入。
英文摘要
We prove the conjecture of Huang, Jiang, and Oblomkov (HJO) giving a geometric extension of the Rogers--Ramanujan and Andrews--Gordon identities for every torus-knot singularity $X^a=Y^b$ with coprime $1<a<b.$ For a prime power $q$, let $\mathcal{NC}_n^{a,b}(\mathbb F_q)$ denote the set of pairs of commuting nilpotent $n\times n$ matrices $(A,B)$ over $\mathbb F_q$ satisfying $A^a=B^b$. We establish the threefold equality between their normalized counts, the HJO $q$-series $Z_{a,b}$, and the explicit infinite product $P_{a,b}$: \[ \underbrace{\vphantom{\Bigg|} \prod_{m\geq1}(1-q^{-m}) \Biggl(\sum_{n=0}^{\infty} \frac{\lvert\mathcal{NC}_n^{a,b}(\mathbb F_q)\rvert} {\lvert\operatorname{GL}_n(\mathbb F_q)\rvert}\Biggr) }_{\text{point count}} = \underbrace{\vphantom{\Bigg|}Z_{a,b}(q^{-1}) }_{\text{\(q\)-series}} = \underbrace{\vphantom{\Bigg|}P_{a,b}(q^{-1}) }_{\text{infinite product}}. \] Our main result is a stronger finite identity: the rank $N$ HJO sum equals $(q;q)_N$ times the generating function for balanced cylindric partitions with entries bounded by $N$. Taking $N\to\infty$ yields the HJO conjecture. The proof combines the compositional rational shuffle theorem of Bergeron--Garsia--Leven--Xin and Mellit with a multiplicativity theorem for slope operators and a determinantal model for bounded cylindric partitions, linked by a common $q$-difference equation. The finite identity and the HJO conjecture have been formalized unconditionally in Lean by AxiomProver.
CommentsThere are two changes from V1. We have expanded the AI declaration, and we have updated the Lean formalization. In V1 the Lean formalization depended on two results from preexisting literature. The new Lean formalization is unconditional. In other words, we have formalized the earlier external prerequisites
