arxiv: 2604.25246 · v1 · submitted 2026-04-28 · 🧮 math.RT · math.CO

Recognition: unknown

Chebyshev quotients, Demazure multiplicities, and Dyck-path models

Jujian Zhang, Ken Ono, Rekha Biswal

Pith reviewed 2026-05-07 14:22 UTC · model grok-4.3

classification 🧮 math.RT math.CO

keywords Chebyshev quotientsDemazure multiplicitiesDyck pathsbounded walksfusion productssl2 moduleseventual positivityrepresentation theory

0 comments

The pith

Chebyshev quotients whose coefficients are Demazure multiplicities eventually have only positive terms or terminate.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves a general theorem that Chebyshev quotients tied to Demazure multiplicities in the representation theory of fusion products either stop after finitely many terms or have strictly positive coefficients from some degree onward. It then gives a combinatorial reading of those positive coefficients as counts of matchings or bounded walks on the integers. In several infinite families the walks specialize to unsigned bounded Dyck paths, which therefore supply explicit counting formulas for the multiplicities themselves.

Core claim

Each Chebyshev quotient arising in this setting either terminates or has strictly positive coefficients for all sufficiently large degrees. These coefficients are realized combinatorially by matchings and bounded walks; for several natural infinite families the same counts are given exactly by the number of unsigned bounded Dyck paths, yielding concrete path models for the associated Demazure multiplicities.

What carries the argument

Chebyshev quotients whose coefficients encode Demazure multiplicities, together with the bijections that identify their eventual positive coefficients with bounded walks and Dyck paths.

If this is right

Demazure multiplicities in the studied families admit explicit enumerative formulas via counting bounded Dyck paths.
The observed positivity of coefficients is explained by a direct bijection rather than by case-by-case verification.
The same eventual-positivity statement applies uniformly to all quotients in the infinite family rather than to isolated examples.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The walk models may extend to other families of modules whose Demazure multiplicities lack known closed forms.
The Dyck-path interpretation could be used to derive new recurrence relations or generating-function identities for the multiplicities.
The theorem supplies a uniform way to certify non-negativity without computing each coefficient separately.

Load-bearing premise

That the Demazure multiplicities appear precisely as the coefficients in the given Chebyshev quotients.

What would settle it

An explicit Chebyshev quotient from the family whose coefficient sequence either fails to terminate and contains infinitely many negative terms or never becomes entirely positive after any finite degree.

read the original 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. Motivated by a recent formula that expresses certain Demazure multiplicities as coefficients of such quotients, we prove a general eventual non-negativity theorem: 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Machine-verified eventual non-negativity for Chebyshev quotients plus Dyck path models for some Demazure multiplicities.

read the letter

The main thing to know is that the paper proves a general theorem that these Chebyshev quotients either terminate or have strictly positive coefficients from some degree onward, with the proof machine-checked in Lean against Mathlib, and it supplies explicit unsigned bounded Dyck path models for several infinite families of the associated Demazure multiplicities. The formalization gives independent verification of the algebraic claim straight from the definitions, which is a clear plus. The combinatorial side interprets the positivity via matchings and bounded walks that specialize to Dyck paths in the natural cases, offering both an explanation and usable models for the multiplicities. This part feels like a genuine addition to the toolkit in algebraic combinatorics. The connection to Demazure multiplicities rests on a recent formula that is cited but not re-derived here, so the representation-theoretic payoff depends on that prior work holding up. The models are presented as interpretations of the quotients rather than independent constructions, which keeps the scope focused but limits how far the combinatorial novelty extends on its own. The note about autonomous generation by AxiomProver from natural-language statements is secondary; the Lean code stands separate from that process. This paper is aimed at people working on positivity phenomena, Demazure flags, and combinatorial models in the representation theory of sl2[t] or fusion products. It could be useful for anyone looking for concrete ways to handle these multiplicities or similar quotients. I would send it for peer review. The verified theorem and the explicit models are concrete enough to merit referee time, even if the Demazure link needs the cited reference for full context.

Referee Report

0 major / 2 minor

Summary. The paper studies Chebyshev quotients arising in Demazure flags for fusion products of sl_2[t]-modules. Motivated by a recent formula expressing Demazure multiplicities as coefficients of these quotients, it proves a general eventual non-negativity theorem: each quotient either terminates or has strictly positive coefficients for sufficiently large degrees. These are interpreted combinatorially via matchings and bounded walks, with several infinite families corresponding to unsigned bounded Dyck path models. All stated theorems are autonomously produced and machine-checked in Lean/Mathlib from natural-language statements.

Significance. The eventual non-negativity result supplies a structural explanation for observed positivity in Demazure multiplicities and yields explicit combinatorial models for key infinite families. The machine-checked formalization against Mathlib constitutes independent verification of the central algebraic claim, independent of the external motivating formula. This strengthens the connection between representation-theoretic positivity phenomena and combinatorial objects such as Dyck paths.

minor comments (2)

[§1] §1 (Introduction): the recent formula for Demazure multiplicities is cited as motivation but not restated even briefly; a one-paragraph summary of the coefficient extraction would improve accessibility for readers outside the immediate subfield.
[§4] The transition between the algebraic non-negativity theorem and the Dyck-path interpretations (around §4) would benefit from an explicit demarcation of which statements are formally proven versus which are presented as interpretive models.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. The report accurately captures the main results on eventual non-negativity of Chebyshev quotients and their combinatorial interpretations via bounded Dyck paths, as well as the independent verification through Lean/Mathlib formalization.

Circularity Check

0 steps flagged

No significant circularity; machine-checked theorem is self-contained

full rationale

The central result is an eventual non-negativity theorem for Chebyshev quotients, proven directly from algebraic definitions and formalized in Lean/Mathlib. This formalization provides independent verification against external benchmarks (Mathlib library), with no reliance on fitted parameters, self-referential equations, or load-bearing self-citations for the positivity claim itself. The Demazure multiplicity formula is cited only as motivation and is not re-derived or used in the core proof chain; combinatorial Dyck-path interpretations are presented as post-hoc explanations derived from the algebraic objects rather than as inputs. No steps reduce by construction to the paper's own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard definitions of Chebyshev polynomials, Demazure flags, and fusion products already present in the literature; no new free parameters or invented entities are introduced.

axioms (1)

standard math Standard axioms and definitions of sl2[t]-modules, Demazure flags, and Chebyshev quotients as encoded in Mathlib
The Lean formalization relies on the existing library for Lie algebra representations and combinatorics.

pith-pipeline@v0.9.0 · 5435 in / 1176 out tokens · 50200 ms · 2026-05-07T14:22:04.573680+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 1 canonical work pages · 1 internal anchor

[1]

Graded characters, demazure multiplicities, and chebyshev polynomials

R. Biswal,Graded characters, Demazure multiplicities, and Chebyshev polynomials, arXiv:2604.17437, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[2]

Biswal, V

R. Biswal, V. Chari, L. Schneider, and S. Viswanath,Demazure flags, Chebyshev polynomials, partial and mock theta functions, J. Combin. Theory Ser. A140(2016), 38–75

2016
[3]

Biswal and D

R. Biswal and D. Kus,A combinatorial formula for graded multiplicities in excellent filtrations, Transform. Groups26(2021), no. 1, 81–114

2021
[4]

Chari, L

V. Chari, L. Schneider, P. Shereen, and J. Wand,Modules with Demazure flags and character formulae, SIGMA Symmetry Integrability Geom. Methods Appl.10(2014), Paper No. 032, 16 pp

2014
[5]

Chari and R

V. Chari and R. Venkatesh,Demazure modules, fusion products and Q-systems, Comm. Math. Phys.333 (2015), no. 2, 799–830

2015
[6]

de Moura, S

L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, The Lean theorem prover (system description), inAutomated Deduction – CADE-25, Lecture Notes in Computer Science 9195, Springer, 2015, 378–388. 2The version used is4.28.0. Compatibility with other versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libr...

2015
[7]

Feigin and S

B. Feigin and S. Loktev,On generalized Kostka polynomials and the quantum Verlinde rule, inDifferential Topology, Infinite-Dimensional Lie Algebras, and Applications, Amer. Math. Soc. Transl. Ser. 2, vol. 194, Amer. Math. Soc., Providence, RI, 1999, pp. 61–79

1999
[8]

Flajolet,Combinatorial aspects of continued fractions, Discrete Math.32(1980), no

P. Flajolet,Combinatorial aspects of continued fractions, Discrete Math.32(1980), no. 2, 125–161

1980
[9]

C. D. Godsil,Algebraic Combinatorics, Chapman & Hall, New York, 1993

1993
[10]

Jakeli´ c and A

D. Jakeli´ c and A. Moura,Limits of multiplicities in excellent filtrations and tensor product decompositions for affine Kac–Moody algebras, Algebr. Represent. Theory21(2018), 239–258

2018
[11]

J. C. Mason and D. C. Handscomb,Chebyshev Polynomials, Chapman & Hall/CRC, Boca Raton, FL, 2002

2002
[12]

The mathlib Community, The Lean mathematical library, inProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020

2020
[13]

R. P. Stanley,Catalan Numbers, Cambridge University Press, New York, 2015. School of Mathematical Sciences, National Institute of Science Education and Research, Bhubaneswar, HBNI, P. O. Jatni, Khurda, 752050, Odisha, India Email address:rekhabiswal27@gmail.com Email address:rekha@niser.ac.in Axiom Math, 124 University A venue, Palo Alto, CA 94301 Email a...

2015