发表机构
Sun Yat-sen University; Academy of Mathematics and Systems Science, Chinese Academy of Sciences; University of Chinese Academy of Sciences（中山大学; 中国科学院数学与系统科学研究院; 中国科学院大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对 Iima--Yoshino 问题 2.3，构造了特征非 5 且含特定元素的域上的理想与单项式序，利用无限约化 Gröbner 基和五边形合冲证明同构，并形式化验证了 Rogers-Ramanujan 恒等式的分拆匹配。
AI 中文摘要
Iima 和 Yoshino 提出了如下问题：在 $S=k[x_1,x_2,\ldots]$ 中（其中 $\operatorname{deg} x_i=i$），求一个理想 $I$ 和一个单项式序，使得 $S/I\cong k[x_i:i\equiv\pm1\pmod5]$，且 $\operatorname{in}(I)=(x_i^2,x_ix_{i+1}:i\geq1)$。我们在每个特征不等于 $5$ 且包含满足 $c^2+c=1$ 的元素 $c$ 的域 $k$ 上构造了这样的理想和单项式序。该理想具有一个显式的无限齐次约化 Gröbner 基。由五边形恒等式导出的五周期合冲证明了所有基关系都属于 $I$，并为非互素临界对提供了标准表示。三角消元建立了分次商同构。商和初始理想的描述共同给出了第一个 Rogers-Ramanujan 恒等式的分拆形式。在每个加权次数中，正规形矩阵支撑集上的一个完美匹配给出了两个分拆类之间的双射。我们使用 Lean 4 和 Mathlib 以及我们基于集合的无限 Gröbner 基理论（包括约化基、分次商同构和分拆匹配定理）形式化了这一复杂特化。
英文摘要
Iima and Yoshino asked for an ideal $I$ in $S=k[x_1,x_2,\ldots]$, with $\operatorname{deg} x_i=i$, and a monomial order such that $S/I\cong k[x_i:i\equiv\pm1\pmod5], \operatorname{in}(I)=(x_i^2,x_ix_{i+1}:i\geq1).$ We construct such an ideal and monomial order over every field $k$ of characteristic different from $5$ containing an element $c$ with $c^2+c=1$. The ideal has an explicit infinite homogeneous reduced Gröbner basis. A five-periodic syzygy derived from a pentagon identity proves that all basis relations belong to $I$ and supplies standard representations for the non-coprime critical pairs. Triangular elimination establishes the graded quotient isomorphism. Together, the quotient and initial ideal descriptions yield the partition form of the first Rogers-Ramanujan identity. In each weighted degree, a perfect matching in the support of the normal-form matrix gives a bijection between the two partition classes. We formalize the complex specialization in Lean 4 using Mathlib and our set-based theory of infinite Gröbner bases, including the reduced basis, the graded quotient isomorphism, and the partition-matching theorem.
