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

Centralizer dimension from vanishing roots

Statement

Assume the Axiom of Choice. Let h be a Cartan subalgebra of a finite-dimensional complex semisimple Lie algebra g with root set Φ (Root and root space). For H∈h, gH=ker⁡(ad⁡H)=h⊕⨁α∈Φα(H)=0gα, and consequently dim⁡gH=dim⁡h+#{α∈Φ:α(H)=0}. In particular gH=h exactly for the regular elements H∈hreg of Regular root hyperplanes.

Facts & Assumptions

Given: The Axiom of Choice, such g,h and an element H∈h.

[A1]

The Axiom of Choice is The Axiom of Choice; it licenses [L1] and the regular-set definition [L2].

[L1]

g=h⊕⨁α∈Φgα is a direct sum, each gα is the eigenspace of ad⁡h with eigenvalue α, and gα is one-dimensional (Root-space decomposition, Root and root space, Root spaces of a complex semisimple Lie algebra are one-dimensional).

[L2]

hreg={H∈h:α(H)≠0 for all α∈Φ} (Regular root hyperplanes).

Proof

technique · direct
1.1A1L1algebra

Write x=H0+∑α∈Φxα with H0∈h and xα∈gα, using the direct sum [L1]. Then ad⁡H(x)=∑αα(H)xα because h is abelian, and this vanishes exactly when α(H)xα=0 for every root.

2.1L1L2step 1.1algebra∎

Hence ker⁡(ad⁡H)=h⊕⨁α(H)=0gα and its dimension is dim⁡h plus the number of roots vanishing at H, by the direct sum of [L1]. By [L2] that number is zero exactly when H∈hreg, in which case gH=h.

Depends on

Used by

Dependency tree · two levels

20 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