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.
Clebsch–Gordan decomposition for sl2
Example
For integers and the irreducible -modules , of All irreducible finite-dimensional sl2 modules, each summand occurring with multiplicity one.
Facts & Assumptions
Given: The modules with basis and -eigenvalues , and the tensor product with the action (All irreducible finite-dimensional sl2 modules, Direct-sum, dual, Hom, and tensor representations).
Each has weights , each with multiplicity one (All irreducible finite-dimensional sl2 modules, Weight and weight space).
Every finite-dimensional -module is a direct sum of irreducible submodules, and an irreducible submodule with top weight has weights , each with multiplicity one (Finite-dimensional representations of sl_2, Irreducible, completely reducible, and faithful representations, The special linear Lie algebra sl_2).
Verification
The weight multiplicities of the tensor product are by [L1]: the sum of the two weights and occurs once for each such pair.
For the right-hand side the same weight occurs in the summand exactly when and modulo , so its multiplicity is in that parity case and otherwise.
The counts agree, for every integer . If or , both counts are zero. Otherwise put . For one has , and the tensor count is A direct case check for and identifies this with the right-hand count of step 1.2. The identity for follows from the symmetries and obtained by reflecting the weight strings.
Both sides are direct sums of irreducibles and the left side is completely reducible by [L2]; moreover in a completely reducible -module the multiplicity of is determined by the weight multiplicities through , so that is recovered by downward induction on .
Applying the recovery of step 2.2 to the two modules, whose weight multiplicities agree by step 2.1, gives equal multiplicities of every and hence the multiplicity-one decomposition .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
21 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
- Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)