TheoremStatement: Literature-sourcedProof: 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.

Steinberg's tensor-product multiplicity formula

Statement

Assume the Axiom of Choice. For all dominant integral weights $λ, μ, ν \in Λ^{+}$ the tensor-product multiplicity of Tensor-product multiplicities for finite-dimensional simple modules is $c_{λ μ}^{ν} = \sum_{w \in W} (- 1)^{ℓ (w)} m_{μ} (w (ν + ρ) - (λ + ρ)),$ where $m_{μ} (σ) = \dim L (μ)_{σ}$ is the weight multiplicity (The formal character of a finite-dimensional weight module) and $W$ is the Weyl group with length function $ℓ$ ; only finitely many summands are nonzero. Equivalently, after the substitution $w \mapsto w^{- 1}$ and Weyl-invariance of the weight multiplicities (Characters of finite-dimensional modules are Weyl-invariant), $c_{λ μ}^{ν} = \sum_{w \in W} (- 1)^{ℓ (w)} m_{μ} (ν + ρ - w (λ + ρ)) .$

Facts & Assumptions

Given: AC, dominant integral weights $λ, μ, ν \in Λ^{+}$ , the alternation operator $A$ with $A (η) = \sum_{w} (- 1)^{ℓ (w)} e^{w η}$ and $A (ρ)$ the Weyl denominator, and the finite-dimensional module $L (λ) \otimes L (μ)$ .

[F1]

Coefficients of a character in the completed ring $R$ are the tensor multiplicities: with $V = L (λ) \otimes L (μ)$ , $c_{λ μ}^{ν} = [V : L (ν)]$ and $ch V = \sum_{ν \in Λ^{+}} c_{λ μ}^{ν} ch L (ν)$ (Tensor-product multiplicities for finite-dimensional simple modules, Tensor-product multiplicities are character structure constants).

[F2]

Alternation extraction: for every finite-dimensional module $V$ and $ν \in Λ^{+}$ , $[e^{ν + ρ}] A (ρ) ch V = [V : L (ν)]$ ; in particular $c_{λ μ}^{ν} = [e^{ν + ρ}] A (ρ) ch (L (λ) \otimes L (μ))$ (Weyl alternation extracts a dominant highest-weight coefficient).

[F3]

Weyl character formula and linearity: $A (ρ) ch L (λ) = A (λ + ρ) = \sum_{w} (- 1)^{ℓ (w)} e^{w (λ + ρ)}$ , the formal character is multiplicative over tensor products, and $ch L (μ) = \sum_{σ} m_{μ} (σ) e^{σ}$ with finitely many nonzero weights, each weight lying in $μ - Q_{+}$ (The Weyl character formula, Formal characters are additive and multiplicative, The formal character of a finite-dimensional weight module, Finite-dimensional modules decompose into weight spaces, Weight and weight space, The completed formal character ring, Geometric series are invertible in the completed character ring).

[F4]

The Weyl group is finite and acts on weights by the reflection action; its length function satisfies $(- 1)^{ℓ (w^{- 1})} = (- 1)^{ℓ (w)}$ , the weight multiplicities of a finite-dimensional module are Weyl-invariant, i.e. $m_{μ} (w σ) = m_{μ} (σ)$ for all $w \in W$ , and the set of weights of $L (μ)$ is finite (The Weyl group is finite and faithful, Root reflections and the Weyl group action, Characters of finite-dimensional modules are Weyl-invariant, The sign of the Weyl length is multiplicative).

Proof

1.1F3F4givenalgebra

Let $V = L (λ) \otimes L (μ)$ . By multiplicativity and the character formula [F3], $A (ρ) ch V = A (λ + ρ) ch L (μ)$ . Expanding gives $\sum_{w, σ} (- 1)^{ℓ (w)} m_{μ} (σ) e^{w (λ + ρ) + σ}$ . For each fixed $w$ , put $σ = w τ$ ; Weyl invariance [F4] gives $m_{μ} (w τ) = m_{μ} (τ)$ . The finite double sum is therefore $\sum_{w, τ} (- 1)^{ℓ (w)} m_{μ} (τ) e^{w (λ + ρ + τ)} = \sum_{τ} m_{μ} (τ) A (λ + ρ + τ)$ .

2.1F1F2F3step 1.1algebra

Extract the coefficient of $e^{ν + ρ}$ using [F2]: $c_{λ μ}^{ν} = [e^{ν + ρ}] A (ρ) ch V = \sum_{σ} m_{μ} (σ) [e^{ν + ρ}] A (λ + ρ + σ),$ and $[e^{ν + ρ}] A (λ + ρ + σ) = \sum_{w \in W} (- 1)^{ℓ (w)} [w (λ + ρ + σ) = ν + ρ]$ . Hence $c_{λ μ}^{ν} = \sum_{w \in W} (- 1)^{ℓ (w)} m_{μ} (w^{- 1} (ν + ρ) - (λ + ρ)),$ because the condition $w (λ + ρ + σ) = ν + ρ$ is equivalent to $σ = w^{- 1} (ν + ρ) - (λ + ρ)$ , and terms with $σ$ outside the finite weight set of $L (μ)$ contribute $m_{μ} (σ) = 0$ .

3.1F1F4step 1.1step 2.1algebra∎

Equivalent form. Substituting $w \mapsto w^{- 1}$ in step 2.1 and using $(- 1)^{ℓ (w^{- 1})} = (- 1)^{ℓ (w)}$ gives $c_{λ μ}^{ν} = \sum_{w} (- 1)^{ℓ (w)} m_{μ} (w (ν + ρ) - (λ + ρ))$ , which is the first displayed formula. Applying to $m_{μ}$ the Weyl-invariance of weight multiplicities [F4] with the group element $w^{- 1}$ gives $m_{μ} (w (ν + ρ) - (λ + ρ)) = m_{μ} (ν + ρ - w^{- 1} (λ + ρ));$ relabelling $w^{'} \mapsto w^{- 1}$ in the sum yields the equivalent form $c_{λ μ}^{ν} = \sum_{w \in W} (- 1)^{ℓ (w)} m_{μ} (ν + ρ - w (λ + ρ)) .$ Only finitely many summands are nonzero in either form, since $W$ is finite [F4] and $m_{μ}$ has finite support.

Depends on

Used by

The Racah--Speiser tensor-product algorithm Corollary

Dependency tree · two levels

55 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

R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants, Graduate Texts in Mathematics 255, Springer 2009 (standard reference, not scraped)
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)