Chebyshev quotients, Demazure multiplicities, and Dyck-path models

TL;DR

This paper investigates Chebyshev quotients related to Demazure multiplicities in Lie algebra representations, establishing non-negativity and combinatorial models using Dyck paths, with formal verification in Lean.

Contribution

It proves a general non-negativity theorem for Chebyshev quotients associated with Demazure multiplicities and provides combinatorial Dyck path models for these multiplicities.

Findings

Proved that Chebyshev quotients either terminate or have positive coefficients for large degrees.

Established combinatorial models using Dyck paths for Demazure multiplicities.

Formalized the theorems in Lean/Mathlib for rigorous verification.

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.