Alphabeta Math
PropositionStatement: Literature-sourcedProof: 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.

Brackets of root spaces

Statement

Let h be a Cartan subalgebra of a finite-dimensional complex semisimple Lie algebra g, and let gα be the root spaces of Root and root space for αh{0}, with gγ=0 whenever γ is not a root or 0. Then [gα,gβ]gα+β for all α,βh.

Facts & Assumptions

Given: Such g,h and functionals α,β.

[L1]

For Hh, the operator adH of Derivations of Lie algebras is a derivation: adH[x,y]=[adHx,y]+[x,adHy] (Derivations form a Lie algebra and inner derivations an ideal).

[L2]

The root spaces are the eigenspaces gγ={x:[H,x]=γ(H)x for all Hh} and the root-space decomposition holds (Root and root space, Root-space decomposition).

Proof

technique · direct
1.1

Let xgα, ygβ and Hh. By [L1], [H,[x,y]]=[[H,x],y]+[x,[H,y]]=[α(H)x,y]+[x,β(H)y]=(α+β)(H)[x,y].

L1algebra
2.1

Since the functional α+β acts on [x,y] by the scalar (α+β)(H) for every Hh, step 1.1 says [x,y]gα+β whenever α+β is a root or 0, and says [x,y]=0gα+β=0 when α+β is neither, which is the convention of the statement; this covers all xgα and ygβ, so [gα,gβ]gα+β. The case α=β=0 says that h is a subalgebra, which it is.

L2step 1.1algebra

Depends on

Used by

Dependency tree · two levels

13 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