Rogers-Ramanujan Identities from the Geometry of X^a=Y^b

This is a Lean formalization of the Huang–Jiang–Oblomkov conjecture on the point counts of pairs of commuting nilpotent matrices satisfying A^a = B^b.

Main Results

• The finite identity: for coprime 1 < a < b and every N, the HJO polynomial is (q)_N times the generating function of the balanced cylindric partitions with largest entry at most N.
• The Huang–Jiang–Oblomkov conjecture for every coprime 1 < a < b.

Both assume two results quoted from the literature: the collinear commutation of the slope operators, and the compositional rational shuffle identity.

See §Formal Challenge for a formal certificate.

Dependencies

This depends on Mathlib and Axiom Math's repository QSeriesLib.

Formal Challenge

A formal challenge file certifying that this repository does formalize the results claimed above is located at Challenge/Basic.lean. This file only depends on the dependencies above. It contains formal statements of §Main Results with sorry as proof.

This repository can be verified against the formal challenge with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator. Then, run the following command:

lake env comparator Comparator/comparator.json

This repository has been locally verified with the comparator.