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 H∈h, the operator ad⁡H of Derivations of Lie algebras is a derivation: ad⁡H[x,y]=[ad⁡Hx,y]+[x,ad⁡Hy] (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 H∈h} and the root-space decomposition holds (Root and root space, Root-space decomposition).

Proof

technique · direct
1.1L1algebra

Let x∈gα, y∈gβ and H∈h. By [L1], [H,[x,y]]=[ [H,x],y ]+[x,[H,y]]=[α(H)x,y]+[x,β(H)y]=(α+β)(H)[x,y].

2.1L2step 1.1algebra∎

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

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