Alphabeta Math
DefinitionDefinition: 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.

Quantum integers, factorials, Gaussian binomials and divided powers at qi

Definition

Let (I,A,D,P,P∨,q) be a symmetrizable Cartan datum for a quantum group (Symmetrizable Cartan data for quantum groups) and put qi=qdi. For m∈N, define the qi-integer

[m]i:=qim−qi−mqi−qi−1,[0]i:=0,

and the qi-factorial

[m]i!:=∏k=1m[k]i,[0]i!:=1.

For 0≤r≤m, define the Gaussian binomial (mr)i:=[m]i!/([r]i![m−r]i!), and set it to 0 when r<0 or r>m. In the published one-parameter convention, write (mr)t:=(mr,m−r)t for the two-part q-multinomial coefficient of The q-integer, q-factorial and q-multinomial coefficients.

For an element x of a unital Q(q)-algebra and m≥0, define its divided power at qi by x(m):=xm/[m]i!, so x(0)=1 and x(1)=x.

The symmetric convention and the published asymmetric convention are related, for m≥0 and 0≤r≤m, by

[m]i=qi−(m−1)[m]qi2,(mr)i=qi−r(m−r)(mr)qi2.

In particular [m]i is invariant under qi↦qi−1. These quantities depend on the symmetrizer only through qi=qdi.

Facts & Assumptions

Given: A symmetrizable Cartan datum with q indeterminate over Q, and an element x of a unital Q(q)-algebra.

[F1]

The datum has qi=qdi with positive integer di (Symmetrizable Cartan data for quantum groups).

[F2]

The asymmetric q-integer and q-factorial are [m]t=1+t+⋯+tm−1 and [m]t!=∏j=1m[j]t, with [0]t=0 and [0]t!=1; the q-multinomial is the factorial quotient (The q-integer, q-factorial and q-multinomial coefficients).

Verification

technique · Expand the symmetric $q_i$-integer and multiply the resulting finite product
1.1givenF1F2algebra

For m≥1, cancel the nonzero factors qi−qi−1=qi−1(qi2−1) to obtain [m]i=qi−(m−1)(qi2m−1)/(qi2−1)=qi−(m−1)∑j=0m−1qi2j=qi−(m−1)[m]qi2. At m=0 the same identity holds by the zero convention. For m≥1 the quotient is nonzero because its numerator and denominator are nonzero in Q(q) by [F1].

2.1step 1.1F1F2algebra

Multiplying the identity of step 1.1 for j=1,…,m gives [m]i!=qi−m(m−1)/2[m]qi2!; for m=0 this is the equality of empty products. Hence for 0≤r≤m, division by the nonzero factorials is valid and (mr)i=qi−m(m−1)/2+r(r−1)/2+(m−r)(m−r−1)/2(mr)qi2=qi−r(m−r)(mr)qi2, since −m(m−1)+r(r−1)+(m−r)(m−r−1)=−2r(m−r).

3.1step 1.1step 2.1F1algebra∎

Since every [j]i for j≥1 is nonzero, [m]i! is a nonzero scalar and therefore invertible in Q(q); this makes x(m) well-defined. Replacing qi by qi−1 negates numerator and denominator in [m]i, so [m]i is invariant, as are its factorials and Gaussian quotients.

Depends on

Used by

Dependency tree · two levels

9 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