Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Sl2 kostant harmonic decomposition

Example

For sl2(C), choose complex coordinates in which the normalized Killing quadratic is q=x2+y2+z2, and put Δ=x2+y2+z2. Multiplication gives an isomorphism of graded vector spaces C[q]CkerΔ  C[x,y,z]. The invariant ring is C[q], so kerΔ is precisely the common kernel of the positive-degree invariant constant-coefficient operators. Its homogeneous degree-n component has dimension 2n+1 for every n0.

Facts & Assumptions

Given: Use matrices h=diag(1,1), e=E12, f=E21, with commutator bracket. Polynomial adjoint invariance means that the derivations with vector fields X[u,X] kill the polynomial for u=h,e,f; the opposite pullback sign gives the same kernels.

The Killing form here is defined by B(u,v)=tr(aduadv) on this three-dimensional matrix algebra.

Verification

1.1

Matrix multiplication gives [h,e]=2e, [h,f]=2f, and [e,f]=h. The matrices of these adjoint maps on (h,e,f) give B(h,h)=8, B(e,f)=B(f,e)=4, and all other basis pairings zero. For example adh has diagonal (0,2,2); adeadf maps h2h, e2e, f0, so its trace is four. The squares of ade,adf and mixed products with adh have zero trace. Thus for X=ah+be+cf, B(X,X)=8(a2+bc). Put x=a, y=(b+c)/2, z=(bc)/(2i); then a2+bc=x2+y2+z2=q. These are orthonormal coordinates for B/8, and B is nondegenerate by this explicit diagonal matrix.

given
2.1

The h-derivation on C[a,b,c] is 2bb2cc. Its kernel consists of sums of monomials with equal b,c exponents, hence polynomials F(a,u) with u=bc. The e-derivation is ca2ab, which on such a polynomial is c(Fa2aFu). Since the polynomial ring is a domain, its vanishing is equivalent to Fa2aFu=0. In the invertible polynomial change v=a2+u, write G(a,v)=F(a,va2). The equation is aG=0, so characteristic zero gives G=P(v). Hence every invariant is a polynomial in q. Conversely the displayed h,e derivations kill q, and the f-derivation ba+2ac also kills q. Therefore the invariant ring is exactly C[q].

step 1.1
3.1

In the orthonormal coordinates for B/8, replacement of a linear coordinate by its corresponding directional derivative sends q to Δ and qk to Δk. Replacing B/8 by B scales the identification on each degree by a nonzero scalar, so the kernels do not change. Positive-degree elements of C[q] are finite linear combinations of qk with k1. Thus their common differential kernel is exactly kerΔ: necessity uses q, and sufficiency uses every power of Δ.

step 1.1step 2.1
4.1

For a homogeneous harmonic polynomial u of degree m, the product rule and the monomial Euler identity xxu+yyu+zzu=mu give Δ(qku)=2k(2m+2k+1)qk1u for k1. Indeed jqk=2kxjqk1 and Δqk=2k(2k+1)qk1 in three variables; the cross term contributes 4kmqk1u and qkΔu=0. Every displayed coefficient is nonzero when k1,m0. For k=0 the Laplacian vanishes by harmonicity.

step 3.1
5.1

Write Sn for homogeneous polynomials of degree n, and Hn=ker(ΔSn). We prove Sn=k=0n/2qkHn2k by induction on n. For n=0,1, differentiation twice gives zero, so Sn=Hn. For n2, the induction decomposition of Sn2 shows that the map Δ:qSn2Sn2 is an isomorphism: on each summand qk+1Hm it is multiplication by the nonzero scalar in 4.1 onto qkHm, and multiplication by the nonzero polynomial q is injective. For any pSn, there is therefore a unique vqSn2 with Δv=Δp; then pvHn. The same injectivity shows HnqSn2=0. This proves the inductive direct decomposition.

step 4.1
6.1

Summing the finite decompositions of 5.1 over degrees proves that multiplication C[q]kerΔS is surjective and injective: each tensor has finite support in the powers of q, and the degreewise decomposition makes all its harmonic coefficients unique. Counting the monomials xaybzc with a+b+c=n gives dimSn=(n+1)(n+2)/2. For n2, 5.1 gives dimHn=dimSndimSn2=2n+1; for n=0,1 the dimensions are directly 1,3. Constants and all linear polynomials are harmonic, zero is allowed throughout, and the nonzero coefficients in 4.1 cover every higher step. The inverse decomposition is uniquely specified by finite calculations in each degree; no AC, general Chevalley restriction or general Kostant theorem is used.

step 3.1step 4.1step 5.1

Used by

Nothing in the library uses this result yet.

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources