切比雪夫商、德马鲁威数量与Dyck路径模型

我们研究切比雪夫商，这些商出现在Lie代数表示论中，具体位于Demazure旗帜理论中，用于fusion $\mathfrak{sl}_2[t]$-模块的表示。使用将数值Demazure数量表示为此类商系数的 recent 公式，我们证明了一个关于计算这些数量的有理函数的普遍最终非负性定理：每个商要么终止，要么在足够大的度数下具有严格正系数，我们进而解释为匹配和受限步行。在几个自然无限系列中，这些是无符号受限Dyck路径模型，为观察到的正性现象提供了结构解释，并为关键Demazure数量族提供具体的组合模型。本文中的定理是由AxiomProver从自然语言声明中自主产生并在Lean/Mathlib中形式化的。