Chebyshev quotients, Demazure multiplicities, and Dyck-path models

Jujian Zhang; Ken Ono; Rekha Biswal

arxiv: 2604.25246 · v2 · pith:CNERJSONnew · submitted 2026-04-28 · 🧮 math.RT · math.CO

Chebyshev quotients, Demazure multiplicities, and Dyck-path models

Rekha Biswal , Ken Ono , Jujian Zhang This is my paper

Pith reviewed 2026-05-21 01:13 UTC · model grok-4.3

classification 🧮 math.RT math.CO

keywords Chebyshev quotientsDemazure multiplicitiesDyck pathsbounded walkssl_2[t]-modulesfusion productsDemazure flags

0 comments

The pith

Chebyshev quotients for Demazure multiplicities eventually have strictly positive coefficients or terminate.

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

The paper examines Chebyshev quotients that emerge in the study of Demazure flags for fusion products of modules over the Lie algebra sl_2[t]. It uses an existing formula connecting numerical Demazure multiplicities directly to the coefficients of these quotients to prove that the quotients exhibit eventual non-negativity. Specifically, each such quotient is either a finite polynomial or its power series expansion has strictly positive coefficients beyond some degree. These positivity results receive interpretations through matchings and bounded walks on paths, and for several infinite families they correspond to enumerations of unsigned bounded Dyck paths. This supplies both a reason for the positivity and explicit combinatorial models for the multiplicities.

Core claim

Using a formula that equates numerical Demazure multiplicities to coefficients in Chebyshev quotients, the paper proves that these rational functions are eventually non-negative, meaning they either terminate or have strictly positive coefficients for all sufficiently large degrees, and interprets this via matchings, bounded walks, and unsigned bounded Dyck path models in natural families.

What carries the argument

The Chebyshev quotients, rational functions whose coefficients give the numerical Demazure multiplicities through a recent formula, and whose eventual positivity is established and combinatorially modeled.

Load-bearing premise

The recent formula equating numerical Demazure multiplicities to coefficients of the Chebyshev quotients is valid.

What would settle it

A direct computation of the series expansion of one of the Chebyshev quotients for a concrete fusion product where the coefficients fail to become strictly positive after a certain degree would disprove the general claim.

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. 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.

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

This paper proves eventual non-negativity for Chebyshev quotients from Demazure multiplicities and supplies bounded Dyck path models for infinite families, with Lean formalization as support.

read the letter

This paper's main contribution is a general theorem that the Chebyshev quotients for Demazure multiplicities are eventually non-negative, together with explicit bounded Dyck path models for several infinite families. The authors take a recent formula expressing the multiplicities as coefficients of these quotients and derive the positivity from it. They then give a combinatorial reading in terms of matchings and bounded walks, which specializes to Dyck paths in key cases. The theorems were produced and formalized in Lean/Mathlib. This is useful because the combinatorial models offer a structural view of the positivity and practical ways to handle the multiplicities. The formalization in Lean stands out as it verifies the internal logic independently. Soft spots are minor and mostly about dependencies. The proof builds directly on the external formula, so any issues there would affect this work. The automated formalization is a positive but one would ideally see more on how it was set up to ensure it aligns perfectly with the mathematical statements. No major gaps or contradictions show up in the claims. The paper is for people working in representation theory of Lie algebras and algebraic combinatorics, particularly around affine types and Demazure modules. Readers interested in positivity results or combinatorial interpretations will find it relevant. It has the substance and verification to go to a serious referee. I would recommend peer review for this.

Referee Report

1 major / 2 minor

Summary. The manuscript studies Chebyshev quotients arising from Demazure flags for fusion products of sl_2[t]-modules. Leveraging a recent formula that expresses numerical Demazure multiplicities as coefficients of these quotients, it proves an eventual non-negativity theorem: each quotient either terminates or has strictly positive coefficients for sufficiently large degrees. This is interpreted combinatorially via matchings and bounded walks, with several natural infinite families yielding unsigned bounded Dyck path models. The theorems were autonomously formalized in Lean/Mathlib from natural-language statements.

Significance. If the result holds, the work supplies combinatorial models that explain the observed positivity in Demazure multiplicities and gives concrete Dyck-path realizations for infinite families. The autonomous Lean/Mathlib formalization supplies machine-checked evidence for the internal steps of the positivity argument and the combinatorial models, reducing dependence on unverified manual reasoning.

major comments (1)

The paragraph on the use of the formula: the eventual non-negativity theorem is derived from the recent external formula for Demazure multiplicities as coefficients of the Chebyshev quotients; the manuscript should state the precise reference and theorem number so that the black-box input can be verified independently.

minor comments (2)

Clarify the precise definition of the Chebyshev quotients and the normalization conventions at the first appearance in the text.
The formalization statement in the abstract would benefit from a short paragraph in the introduction or an appendix describing the scope of the Lean development (e.g., which lemmas were checked).

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the constructive comment, which will help improve the clarity of the presentation. We address the point raised below.

read point-by-point responses

Referee: The paragraph on the use of the formula: the eventual non-negativity theorem is derived from the recent external formula for Demazure multiplicities as coefficients of the Chebyshev quotients; the manuscript should state the precise reference and theorem number so that the black-box input can be verified independently.

Authors: We agree that explicitly identifying the source of the external formula will strengthen the manuscript by allowing readers to verify the black-box input independently. The relevant paragraph currently refers to 'a recent formula' without a specific citation or theorem number. In the revised version we will insert the precise reference and theorem number (e.g., 'Theorem 4.1 of [Smith et al., Adv. Math. 2023]') at the first point of use, together with a brief parenthetical reminder of the statement being invoked. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation uses external formula with machine-checked proofs

full rationale

The paper takes as input a recent external formula expressing Demazure multiplicities as coefficients of Chebyshev quotients and derives an eventual non-negativity theorem for those quotients, with combinatorial interpretations via bounded walks and Dyck paths in specific families. The internal steps of the positivity argument and models are autonomously formalized in Lean/Mathlib, supplying machine-checked independent verification. No equations reduce any claimed prediction or result to a fitted parameter, self-definition, or unverified self-citation chain; the external formula functions as a black-box starting point rather than a load-bearing self-reference. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on an external recent formula for expressing Demazure multiplicities as coefficients of Chebyshev quotients; no free parameters, invented entities, or additional ad-hoc axioms are visible in the abstract.

axioms (1)

domain assumption A recent formula expresses numerical Demazure multiplicities as coefficients of Chebyshev quotients.
Invoked in the abstract as the starting point for the positivity analysis.

pith-pipeline@v0.9.0 · 5674 in / 1268 out tokens · 31723 ms · 2026-05-21T01:13:18.928994+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We use the polynomial sequence p0(x)=p1(x)=1, pr+1(x)=pr(x)−x pr−1(x) … F(x) := pm−μ0−1(x) p_ξ(x) / p_m(x)^{μ1+1}

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

13 extracted references · 13 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

work page 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

work page 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

work page 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

work page 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...

work page 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

work page 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

work page 1980
[9]

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

work page 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

work page 2018
[11]

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

work page 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

work page 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...

work page 2015

[1] [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] [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

work page 2016

[3] [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

work page 2021

[4] [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

work page 2014

[5] [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

work page 2015

[6] [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...

work page 2015

[7] [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

work page 1999

[8] [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

work page 1980

[9] [9]

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

work page 1993

[10] [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

work page 2018

[11] [11]

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

work page 2002

[12] [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

work page 2020

[13] [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...

work page 2015