Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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 a,b0 and the irreducible sl2-modules V(a), V(b) of All irreducible finite-dimensional sl2 modules, V(a)V(b)i=0min(a,b)V(a+b2i), each summand occurring with multiplicity one.

Facts & Assumptions

Given: The modules V(n) with basis v0,,vn and h-eigenvalues n2k, and the tensor product V(a)V(b) with the action x(uw)=xuw+uxw (All irreducible finite-dimensional sl2 modules, Direct-sum, dual, Hom, and tensor representations).

[L1]

Each V(n) has weights n,n2,,n, each with multiplicity one (All irreducible finite-dimensional sl2 modules, Weight and weight space).

[L2]

Every finite-dimensional sl2-module is a direct sum of irreducible submodules, and an irreducible submodule with top weight m0 has weights m,m2,,m, each with multiplicity one (Finite-dimensional representations of sl_2, Irreducible, completely reducible, and faithful representations, The special linear Lie algebra sl_2).

Verification

technique · direct
1.1

The weight multiplicities of the tensor product are wm=#{(r,s):0ra, 0sb, a+b2(r+s)=m} by [L1]: the sum m of the two weights a2r and b2s occurs once for each such pair.

L1
1.2

For the right-hand side i=0min(a,b)V(a+b2i) the same weight m occurs in the summand V(a+b2i) exactly when ma+b2i and ma+b modulo 2, so its multiplicity is wm=max(0,min(min(a,b),(a+bm)/2)+1) in that parity case and 0 otherwise.

L1L2
2.1

The counts agree, wm=wm for every integer m. If m≢a+b(mod2) or m>a+b, both counts are zero. Otherwise put j=(a+bm)/2. For m0 one has 0j(a+b)/2, and the tensor count is cj=max(0,min(j,a)max(0,jb)+1). A direct case check for ab and a>b identifies this with the right-hand count of step 1.2. The identity for m<0 follows from the symmetries wm=wm and wm=wm obtained by reflecting the weight strings.

L1step 1.1step 1.2
2.2

Both sides are direct sums of irreducibles and the left side is completely reducible by [L2]; moreover in a completely reducible sl2-module the multiplicity cn of V(n) is determined by the weight multiplicities through wn=mn, mn (2)cm, so that cn=wnm>n, mn (2)cm is recovered by downward induction on n.

L1L2step 1.1
3.1

Applying the recovery of step 2.2 to the two modules, whose weight multiplicities agree by step 2.1, gives equal multiplicities of every V(n) and hence the multiplicity-one decomposition V(a)V(b)i=0min(a,b)V(a+b2i).

step 2.1step 2.2

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