LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The quantum Pascal recurrences, the Gauss product formula and Gaussian integrality

Statement

Fix a symmetrizable Cartan datum and $i \in I$ , and use the conventions of Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ . Write $C_{m, r} : = {(\binom{m}{r})}_{i}$ , with $C_{m, r} = 0$ when $r < 0$ or $r > m$ .

(i) Pascal recurrences. For $m \geq 1$ and every integer $r$ ,

$C_{m, r} = q_{i}^{- r} C_{m - 1, r} + q_{i}^{m - r} C_{m - 1, r - 1} = q_{i}^{r} C_{m - 1, r} + q_{i}^{r - m} C_{m - 1, r - 1} .$

(ii) Symmetry. For $0 \leq r \leq m$ , $C_{m, r} = C_{m, m - r}$ .

(iii) Gauss product formula. For every $N \geq 0$ , in the polynomial ring $Q (q) [z]$ ,

$\prod_{j = 0}^{N - 1} (1 + q_{i}^{2 j} z) = \sum_{r = 0}^{N} q_{i}^{r (N - 1)} C_{N, r} z^{r} .$

Consequently, for $N \geq 1$ ,

$\sum_{r = 0}^{N} (- 1)^{r} q_{i}^{r (N - 1)} C_{N, r} = 0.$

(iv) Integrality. For $0 \leq r \leq m$ ,

$C_{m, r} \in q_{i}^{- r (m - r)} Z [q_{i}^{2}] \subseteq Z [q_{i}^{\pm 1}] .$

Thus every Gaussian quotient is a Laurent polynomial in $q_{i}$ with integer coefficients, and the Pascal recurrences hold in that Laurent polynomial ring.

Facts & Assumptions

Given: A symmetrizable Cartan datum, a fixed $i \in I$ , and the symmetric $q_{i}$ -integer, factorial and Gaussian quotient from Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ .

[F1]

$q_{i} = q^{d_{i}}$ for an indeterminate $q$ and positive integer $d_{i}$ ; all symmetric $q_{i}$ -factorials in the quotient are nonzero (Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ ).

[F2]

$R [z]$ is the polynomial ring over a commutative ring $R$ , and $Z [t^{\pm 1}]$ consists of finite Laurent sums with integer coefficients (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, The Laurent polynomial ring as the principal localisation of Z[t] at t).

Proof

technique · Derive the recurrences from a symmetric $q_i$-integer identity, then use induction

1.1givenF1algebra

For $0 \leq r \leq m$ , the numerator identity $q_{i}^{- r} (q_{i}^{m - r} - q_{i}^{- (m - r)}) + q_{i}^{m - r} (q_{i}^{r} - q_{i}^{- r}) = q_{i}^{m} - q_{i}^{- m}$ gives $[m]_{i} = q_{i}^{- r} [m - r]_{i} + q_{i}^{m - r} [r]_{i}$ .

2.1step 1.1F1algebra

For $1 \leq r \leq m - 1$ , multiply the identity of step 1.1 by $[m - 1]_{i}! / ([r]_{i}! [m - r]_{i}!)$ and use the factorial quotient to obtain $C_{m, r} = q_{i}^{- r} C_{m - 1, r} + q_{i}^{m - r} C_{m - 1, r - 1}$ . The same formula holds at $r = 0, m$ by $C_{m, 0} = C_{m, m} = 1$ and the out-of-range zero convention; for $r < 0$ or $r > m$ every term is zero. The factorial definition gives $C_{m, r} = C_{m, m - r}$ for $0 \leq r \leq m$ ; applying the first recurrence at $m - r$ and using this symmetry gives the second recurrence.

3.1step 2.1F1F2algebra

Put $G_{m, r} : = q_{i}^{r (m - r)} C_{m, r}$ . The first recurrence in step 2.1 gives, for $1 \leq r \leq m - 1$ , $G_{m, r} = G_{m - 1, r} + q_{i}^{2 (m - r)} G_{m - 1, r - 1}$ . Since $G_{m, 0} = G_{m, m} = 1$ , induction on $m$ shows $G_{m, r}$ is a polynomial in $q_{i}^{2}$ with integer coefficients; this proves $C_{m, r} \in q_{i}^{- r (m - r)} Z [q_{i}^{2}]$ . Because $d_{i} > 0$ and $q$ is indeterminate, distinct powers of $q_{i}$ are linearly independent over $Z$ , so this evaluation embeds the Laurent polynomial ring and gives the stated inclusion and Laurent-polynomial recurrences.

3.2step 2.1F2algebra

Let $P_{N} (z) : = \prod_{j = 0}^{N - 1} (1 + q_{i}^{2 j} z)$ . For $N = 0$ both sides of the Gauss formula are $1$ . If it holds for $N - 1$ , the coefficient of $z^{r}$ in $P_{N}$ is $q_{i}^{r (N - 2)} C_{N - 1, r} + q_{i}^{(r - 1) (N - 2) + 2 (N - 1)} C_{N - 1, r - 1}$ ; by the first recurrence in step 2.1 this equals $q_{i}^{r (N - 1)} C_{N, r}$ , since $(r - 1) (N - 2) + 2 (N - 1) = r (N - 1) + N - r$ . Thus induction proves the product formula in $Q (q) [z]$ .

4.1step 3.2algebra∎

For $N \geq 1$ , evaluate the formula of step 3.2 at $z = - 1$ . The factor with $j = 0$ makes the product zero, so its right side is the alternating Gaussian sum in the statement and is zero. This proves the final assertion and completes all parts.

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Kyeonghoon Jeong, Seok-Jin Kang and Masaki Kashiwara, Crystal Bases for Quantum Generalized Kac-Moody Algebras, arXiv:math/0305390 (standard reference, not scraped)
Benjamin Enriquez, PBW and Duality Theorems for Quantum Groups and Quantum Current Algebras, Journal of Lie Theory 13 (2003), 21–64 (standard reference, not scraped)