Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-26 (gpt-6-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.

Restricted root space decomposition

Statement

Assume the Axiom of Choice. Let g0 be a finite-dimensional real semisimple Lie algebra with Cartan involution θ, Cartan decomposition g0=k0⊕p0, Killing form B and inner product Bθ(X,Y)=−B(X,θY) (Bracket relations and Killing signs in a Cartan decomposition). Let a⊆p0 be a maximal abelian subspace, and let Σ=Σ(g0,a) and the spaces g0λ be as in Restricted root and restricted root space. Then:

  1. g0 is the direct sum g0=g00⊕⨁λ∈Σg0λ, the summands are pairwise orthogonal for Bθ, and g00=Zg0(a); the index set Σ is finite and every multiplicity mλ=dim⁡Rg0λ is a finite positive integer;
  2. g00=a⊕m with m=Zk0(a)=k0∩g00, an orthogonal direct sum, and a=p0∩g00;
  3. [g0λ,g0μ]⊆g0λ+μ for all λ,μ∈a∗, where g0ν is understood as in Restricted root and restricted root space (so that [g0λ,g0μ]=0 whenever λ+μ∉{0}∪Σ);
  4. θg0λ=g0−λ for every λ∈a∗; in particular λ∈Σ if and only if −λ∈Σ;
  5. if H∈a satisfies λ(H)≠0 for every λ∈Σ, then Zg0(H)=g00.

Facts & Assumptions

Given: The Axiom of Choice; a real semisimple g0 with Cartan involution θ, Cartan decomposition g0=k0⊕p0, Killing form B, inner product Bθ(X,Y)=−B(X,θY), and a maximal abelian subspace a⊆p0.

[A1]

The Axiom of Choice is The Axiom of Choice. It is declared here as part of the ZFC interface of the restricted-root chain, which every consumer of this decomposition propagates; the argument below performs no selection beyond the cited finite-dimensional linear algebra of [L2] and [L3].

[L1]

The Killing form B(X,Y)=tr⁡(ad⁡Xad⁡Y) is invariant and nondegenerate, and an automorphism preserves it because it conjugates every adjoint operator and trace is similarity-invariant. Thus B(θX,θY)=B(X,Y). The summands k0,p0 are B-orthogonal, B is negative definite on k0 and positive definite on p0, and [k0,k0]⊆k0, [k0,p0]⊆p0, [p0,p0]⊆k0 (Killing form, Trace forms are symmetric and invariant, Cartan's semisimplicity criterion, Cartan involution of a real semisimple Lie algebra, Similar matrices have the same trace, Bracket relations and Killing signs in a Cartan decomposition).

[L2]

A finite family of pairwise commuting diagonalisable endomorphisms of a finite-dimensional real vector space is simultaneously diagonalisable: there is a basis consisting of common eigenvectors (A family of diagonalisable endomorphisms of a finite-dimensional space is simultaneously diagonalisable if and only if its members commute pairwise).

[L3]

A self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal basis of eigenvectors, hence is diagonalisable with real eigenvalues, and its eigenspaces for distinct eigenvalues are orthogonal for the inner product (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

Proof

technique · direct
1.1L1L3algebra

For H∈p0 the endomorphism ad⁡H of g0 is self-adjoint for Bθ: for all X,Y∈g0, using θH=−H and [L1], Bθ([H,X],Y)=−B([H,X],θY)=−B(X,[θY,H])=B(X,[H,θY])=Bθ(X,[H,Y]); moreover ad⁡[H,H′]=[ad⁡H,ad⁡H′], so for H,H′∈a the endomorphisms ad⁡H and ad⁡H′ commute because [H,H′]=0, and hence {ad⁡H:H∈a} is a commuting family of self-adjoint, therefore diagonalisable, endomorphisms of g0.

1.2algebra

If 0≠X∈g0 is a common eigenvector of the family {ad⁡H:H∈a}, define λX:a→R by ad⁡H(X)=λX(H)X for H∈a; then λX is linear, because for H,H′∈a and c∈R one has λX(H+cH′)X=ad⁡(H+cH′)X=(λX(H)+cλX(H′))X and X≠0 permits cancellation of X.

1.3algebra

Bracket relation: for X∈g0λ, Y∈g0μ and H∈a, the Jacobi identity gives ad⁡H([X,Y])=[ad⁡HX,Y]+[X,ad⁡HY]=(λ(H)+μ(H))[X,Y]=(λ+μ)(H)[X,Y], so [X,Y]∈g0λ+μ; in particular [g0λ,g0μ]⊆g0λ+μ.

1.4L1algebra

θ-stability: for X∈g0λ and H∈a one has θH=−H and θ is an automorphism, so [H,θX]=θ[θH,X]=θ[−H,X]=−θ[H,X]=−λ(H)θX, that is θX∈g0−λ; since θ is an involution, θg0λ=g0−λ, and g0λ≠0 exactly when g0−λ≠0.

1.5algebra

a=p0∩g00: the inclusion a⊆p0∩g00 holds because a⊆p0 and a is abelian; conversely, if X∈p0∩g00, then [X,a]=0 and [X,X]=0, so a+RX is an abelian subspace of p0 containing a, and maximality of a forces X∈a.

2.1L2step 1.1step 1.2algebra

Choose a finite basis H1,…,Hr of a. By [L2] the commuting operators ad⁡H1,…,ad⁡Hr have a common eigenbasis {X1,…,XN} of g0. Every H∈a is a linear combination of the Hj, so each Xi is an eigenvector of ad⁡H as well and lies in g0λXi. Thus the subspaces g0λ span g0 and only finitely many functionals λ∈a∗ occur with g0λ≠0. This includes a=0, when the operator family is empty.

2.2L3step 1.1algebra

Orthogonality: if λ≠μ are occurring functionals, there is H∈a with λ(H)≠μ(H); the spaces g0λ and g0μ are eigenspaces of the self-adjoint endomorphism ad⁡H for the distinct real eigenvalues λ(H) and μ(H), hence are orthogonal for Bθ by [L3].

2.3L1step 1.4step 1.5algebra

g00=a⊕m: by step 1.4 with λ=0 the involution θ preserves g00, so every X∈g00 decomposes as X=12(X+θX)+12(X−θX) with the first summand in k0∩g00 and the second in p0∩g00=a by step 1.5; also k0∩g00=k0∩Zg0(a)=Zk0(a)=m, so g00=m⊕a, the sum is direct because k0∩p0=0, and it is orthogonal by [L1].

3.1step 1.2step 2.1

Conversely, if an occurring functional λ is given, that is g0λ≠0, pick 0≠X∈g0λ; then X is a common eigenvector with λX=λ, so the set of functionals λ∈a∗ with g0λ≠0 is exactly the finite set of functionals λXi of step 2.1, and Σ is the set of its nonzero members: Σ is finite and each multiplicity mλ=dim⁡Rg0λ is a finite positive integer.

4.1step 2.1step 3.1algebra

The occurring spaces g0λ are linearly independent and span g0: if ∑λXλ=0 with Xλ∈g0λ and some Xλ0≠0, expand in the common eigenbasis of step 2.1; a basis vector with functional λXi can appear with nonzero coefficient in Xλ0 only when λXi=λ0, and distinct occurring functionals involve disjoint groups of basis vectors, so ∑λXλ≠0, a contradiction; hence g0=⨁λ∈a∗g0λ, the sum extending over the finitely many occurring functionals, and discarding λ=0 while using that the occurring nonzero functionals are exactly the elements of Σ and that g00=Zg0(a) by Restricted root and restricted root space gives the direct sum of statement 1.

5.1step 4.1algebra

If H∈a satisfies λ(H)≠0 for every λ∈Σ, then Zg0(H)=⨁λ:λ(H)=0g0λ=g00, because g0λ lies in the kernel of ad⁡H exactly when λ(H)=0.

6.1A1step 2.2step 2.3step 3.1step 4.1step 5.1step 1.3step 1.4step 1.5∎

Statements 1–5 are now established: the direct-sum decomposition in step 4.1; the finiteness of Σ and of the multiplicities in step 3.1; the orthogonality in step 2.2; the description of g00 in steps 1.5 and 2.3; the bracket relation in step 1.3; the θ-stability in step 1.4; and the regular-element centralizer in step 5.1. The Axiom of Choice was declared in [A1], and no selection was made in the argument.

Depends on

Used by

Dependency tree · two levels

32 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