A Solution to Iima--Yoshino Problem 2.3

Abstract

Iima and Yoshino asked for an ideal $I$ in $S=k[x_1,x_2,\dots ]$, with $\mathrm{deg}{x}_i=i$, and a monomial order such that $S/I\cong k[x_i:i\equiv \pm 1(\mathrm{mod}5)],\mathrm{in}(I)=(x_i^2,x_i{x}_{i+1}:i\ge 1).$ 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.