ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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 Clebsch--Gordan tensor decomposition for sl2

Example

Assume the Axiom of Choice. Take $g = {s l}_{2}$ with positive root $α$ and Weyl group $W = {1, s}$ , so that $ρ = α / 2 = : ω$ and the dominant integral weights are $m ω$ , $m \geq 0$ (Root systems of the classical complex Lie algebras, Classical complex matrix Lie algebras, Integral, dominant, and strictly dominant weights, The Weyl vector rho for a chosen positive system). For an integer $m \geq 0$ let $L (m) = L (m ω)$ be the finite-dimensional simple module of highest weight $m ω$ ; it has dimension $m + 1$ and weights $m ω, (m - 2) ω, \dots, - m ω$ , each of multiplicity one (Finite-dimensional representations of sl_2, Highest-weight classification). Then for all integers $a, b \geq 0$ the tensor-product multiplicities of Tensor-product multiplicities for finite-dimensional simple modules are $c_{a b}^{c} = {\begin{cases} 1, & ∣ a - b ∣ \leq c \leq a + b, c \equiv a + b (m o d 2), \\ 0, & otherwise, \end{cases} equivalently L (a) \otimes L (b) ≅ ⨁_{j = 0}^{\min (a, b)} L (a + b - 2 j) .$ In particular there are exactly $\min (a, b) + 1$ simple summands, with extreme summands $L (a + b)$ and $L (∣ a - b ∣)$ . The number matches the Racah--Speiser sum of The Racah--Speiser tensor-product algorithm: in the $ρ = ω$ normalisation a weight $φ$ of $L (b)$ is irregular relative to $a ω$ exactly when $φ + a ω + ρ = 0$ , i.e. $φ = - (a + 1) ω$ , which is a weight of $L (b)$ exactly when $a + 1 \leq b$ and $a + b$ is odd; the remaining $b + 1$ (or $b$ ) weights contribute $\pm 1$ , and the contributions with sign $- 1$ cancel the overlapping range $0 \leq c \leq b - a - 2$ when $a < b$ , leaving exactly the multiplicities $1$ above.

Facts & Assumptions

Given: AC, integers $a, b \geq 0$ , $g = {s l}_{2}$ with $Φ^{+} = {α}$ , $ρ = ω = α / 2$ , $W = {1, s}$ where $s$ acts by $s (λ ω) = - λ ω$ , and the modules $L (m) = L (m ω)$ of dimension $m + 1$ with weights $(m - 2 j) ω$ , $j = 0, \dots, m$ , of multiplicity one.

[F1]

Racah--Speiser algorithm: for dominant integral $λ, μ$ , $c_{λ μ}^{ν} = \sum_{\begin{array}{c} φ weight of L (μ) \\ φ regular relative to λ, ν (φ) = ν \end{array}} (- 1)^{ℓ (u (φ))} m_{μ} (φ),$ where $φ$ is regular relative to $λ$ when $ψ + ρ = φ + λ + ρ$ is fixed by no reflection, $u (φ)$ is the unique element of $W$ with $u (φ) (ψ + ρ)$ strictly dominant, and $ν (φ) = u (φ) (ψ + ρ) - ρ$ ; irregular weights are discarded and every $ν$ with $c_{λ μ}^{ν} \neq 0$ occurs as $ν (φ)$ for a regular weight $φ$ (The Racah--Speiser tensor-product algorithm).

[F2]

The reflections of $W = {1, s}$ act on weights by $s (λ ω) = - λ ω$ ; an element $χ ω$ is strictly dominant exactly when $χ > 0$ , and $u (φ) = 1$ for a regular weight $φ$ with $φ + λ + ρ > 0$ , while $u (φ) = s$ when $φ + λ + ρ < 0$ . The trivial Weyl group element has length $0$ and the reflection has length $1$ (The Weyl vector rho for a chosen positive system, Root systems of the classical complex Lie algebras, The Racah--Speiser tensor-product algorithm, Integral, dominant, and strictly dominant weights).

[F3]

A weight $φ = (b - 2 j) ω$ of $L (b)$ is irregular relative to $a ω$ exactly when $φ = - (a + 1) ω$ , i.e. $b - 2 j = - (a + 1)$ or equivalently $2 j = a + b + 1$ ; this happens for a unique $j$ exactly when $a + b$ is odd and $0 \leq j \leq b$ , which for $a, b \geq 0$ means $a < b$ and $j = (a + b + 1) / 2$ , and this weight exists automatically in that case. Sums of weights are computed in the one-dimensional space $R ω$ (The Racah--Speiser tensor-product algorithm, Finite-dimensional representations of sl_2).

Verification

1.1F1givenalgebra

Fix integers $a, b \geq 0$ and let $c \geq 0$ be an integer; the coefficient to compute is $c_{a ω, b ω}^{c ω}$ . By [F1] its value is the alternating sum of the multiplicities $m_{b} (φ) = 1$ over the regular weights $φ$ of $L (b)$ with $ν (φ) = c ω$ ; recall $λ = a ω$ , $μ = b ω$ , $ρ = ω$ .

1.2F1F2F3givenalgebra

Regularity and the value of $u$ . For a weight $φ = φ_{0} ω$ of $L (b)$ , the shifted weight $φ + a ω + ρ = (φ_{0} + a + 1) ω$ is fixed by $s$ exactly when it is zero, i.e. $φ_{0} = - (a + 1)$ . Such a weight exists in $L (b)$ exactly when $a + 1 \leq b$ and $b + a + 1$ is even, by [F3]; it is then the unique irregular weight. For every other weight, $φ_{0} + a + 1 \neq 0$ , so $u (φ) = 1$ if $φ_{0} + a + 1 > 0$ and $u (φ) = s$ if $φ_{0} + a + 1 < 0$ [F2].

2.1F1F2step 1.2algebra

Contributions of the regular weights. Write $φ = (b - 2 j) ω$ , $j = 0, \dots, b$ , and put $t = φ_{0} + a + 1 = b - 2 j + a + 1$ . If $t > 0$ , then $ν (φ) = (b - 2 j + a) ω$ and the sign is $(- 1)^{0} = + 1$ ; this contributes $+ 1$ to $c_{a b}^{ν}$ with $ν = b + a - 2 j$ , i.e. to $c = a + b - 2 j$ with $0 \leq j < (a + b + 1) / 2$ . If $t < 0$ , then $u (φ) = s$ , $ν (φ) = s (t ω) - ω = - t ω - ω = (- t - 1) ω = (2 j - a - b - 2) ω$ and the sign is $(- 1)^{1} = - 1$ ; this contributes $- 1$ to the coefficient of $c = 2 j - a - b - 2$ . The inequality $t < 0$ means $j > (a + b + 1) / 2$ , so $j$ ranges over the integers from $⌊ (a + b + 1) / 2 ⌋ + 1$ to $b$ (if any), and the corresponding $c = 2 j - a - b - 2$ are exactly the integers congruent to $a + b$ modulo $2$ lying in the interval $0 \leq c \leq b - a - 2$ when $a + b$ is even and $1 \leq c \leq b - a - 2$ when $a + b$ is odd, the empty interval when the bound $b - a - 2$ is negative.

3.1F1step 1.2step 2.1algebra

The $+ 1$ family has $0 \leq j \leq \min (b, ⌊ (a + b) / 2 ⌋)$ , so its output weights are exactly the integers $c \equiv a + b (m o d 2)$ with $\max (0, a - b) \leq c \leq a + b$ . If $b \leq a$ , there is no $- 1$ family, and the least output is $a - b$ . If $b > a$ , the $- 1$ family of step 2.1 cancels exactly the same-parity $+ 1$ outputs below $b - a$ , namely $0 \leq c \leq b - a - 2$ . In either case the survivors are precisely $∣ a - b ∣ \leq c \leq a + b$ with the stated parity, each with coefficient one; all other coefficients are zero.

4.1F1step 3.1algebra∎

Reading the multiplicities: the values $c$ with $c_{a b}^{c} = 1$ are $a + b, a + b - 2, \dots, ∣ a - b ∣$ , exactly $\min (a, b) + 1$ values, with extremes $a + b$ and $∣ a - b ∣$ ; hence $L (a) \otimes L (b) ≅ ⨁_{j = 0}^{\min (a, b)} L (a + b - 2 j)$ , and the dimension check is $\sum_{j = 0}^{\min (a, b)} (a + b - 2 j + 1) = (a + 1) (b + 1) = \dim L (a) \dim L (b)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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

A. W. Knapp, Lie Groups Beyond an Introduction, 2nd ed., Birkhäuser 2002 (standard reference, not scraped)
P. Etingof, Lie Groups and Lie Algebras II (MIT 18.755, Spring 2024), complete lecture notes (standard reference, not scraped)