Chebyshev quotients, Demazure multiplicities, and Dyck-path models
Rekha Biswal, Ken Ono, Jujian Zhang
math.RT
Apr 28, 2026 · v1
TL;DR
Theorems autonomously produced and formalized in Lean/Mathlib by AxiomProver.
Abstract
We study Chebyshev quotients that arise in the representation theory of Lie algebras, specifically within the theory of Demazure flags for fusion products of $\mathfrak{sl}_2[t]$-modules. Using a recent formula that expresses numerical Demazure multiplicities as coefficients of such quotients, we prove a general eventual non-negativity theorem for the same rational functions that compute these multiplicities: each quotient either terminates or has strictly positive coefficients for sufficiently large degrees, which we in turn interpret in terms of matchings and bounded walks. In several natural infinite families, these are unsigned bounded Dyck path models, giving both a structural explanation for the observed positivity phenomenon and concrete combinatorial models for key families of Demazure multiplicities. The theorems in this paper were autonomously produced and formalized in Lean/Mathlib by AxiomProver from natural-language statements.
Problem
Numerical Demazure multiplicities for fusion products of sl_2[t]-modules are expressed as coefficients of Chebyshev quotients, but their eventual non-negativity and combinatorial interpretation were not understood in general.
Approach
Using a formula expressing Demazure multiplicities as coefficients of rational functions built from Chebyshev-type polynomials, the authors prove a general eventual non-negativity theorem by analyzing the roots of p_m. They interpret the coefficients in terms of matchings and bounded walks, giving unsigned bounded Dyck path models for key families. All theorems were autonomously produced and formalized in Lean/Mathlib by AxiomProver from natural-language statements.
Results
A general eventual positivity result is proved: each Chebyshev quotient either terminates or has strictly positive coefficients for sufficiently large degrees. Concrete combinatorial models (bounded Dyck paths) are provided for natural infinite families of Demazure multiplicities. The proofs are fully formalized in Lean/Mathlib.
