A Solution to Iima–Yoshino Problem 2.3
Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi
math.AC
Sep 6, 2026 · v1
math.RA
TL;DR
Formalizes in Lean 4 with Mathlib the complex specialization of a solution to the Iima–Yoshino Gröbner-basis problem, including reduced basis and partition bijection.
Abstract
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.
Problem
Iima and Yoshino asked for an ideal I in a graded polynomial ring with infinitely many variables and a monomial order such that the quotient is a polynomial algebra on parts congruent to ±1 mod 5 and the initial ideal equals a specified monomial ideal. Solving it gives an algebraic realization of the first Rogers–Ramanujan identity.
Approach
An explicit homogeneous ideal is constructed from coefficients of a single quadratic generating-function relation, valid over any field of characteristic ≠5 containing c with c²+c=1. A five-periodic syzygy derived from a pentagon identity proves the basis relations lie in the ideal and supplies standard representations for critical pairs, while triangular elimination establishes the graded quotient isomorphism. The complex specialization and the partition-matching theorem are formalized in Lean 4 using Mathlib and an earlier set-based theory of infinite Gröbner bases, reusing the infinite Buchberger criterion, polynomial division, and normal-form theory.
Results
The construction yields an explicit infinite homogeneous reduced Gröbner basis and the required quotient and initial ideal descriptions, giving an algebraic proof of the first Rogers–Ramanujan identity via perfect matchings between the two partition classes. The main theorem and the partition bijection are formally verified in Lean 4 for the complex case.
