TheoremStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-23 (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.

The root set is a reduced crystallographic root system

Statement

Assume the Axiom of Choice (The Axiom of Choice). For a finite-dimensional complex semisimple Lie algebra and any Cartan subalgebra $h$ in the nilpotent self-normalizing sense, with the bilinear form induced on $h^{*}$ by the Killing form, its root set $Φ$ is a finite reduced crystallographic root system. Moreover, every root space $g_{α}$ is one-dimensional.

Facts & Assumptions

Given: The Axiom of Choice; a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ , and its root set $Φ \subseteq h^{*}$ .

[F0]

Under Choice, every Cartan subalgebra of $g$ in the nilpotent self-normalizing sense is maximal toral (Cartan subalgebras are exactly maximal toral subalgebras).

[F1]

For a maximal toral $h$ , the finite semisimple Cartan/root/string theorem proves that the Killing form is nondegenerate on $h$ , every root space is one-dimensional, and $Φ$ is a finite reduced crystallographic root system for its positive real dual form (Finite semisimple Cartan, root and string structure).

[F2]

The Killing-dual vector $H_{α}$ is the vector corresponding to $α$ under the restricted Killing form (The Killing-dual vector attached to a root).

Proof

technique · direct

1.1F0F1F2

By [F0], the supplied Cartan subalgebra is maximal toral, so [F1] applies. Its Killing-form restriction is nondegenerate, and its real form is positive definite. Thus its induced bilinear form on the real span of roots agrees with the dual form used in [F1]; [F2] identifies the corresponding root vectors with the Killing-dual notation of this page.

2.1F1step 1.1∎

The remaining assertions are exactly the conclusions of [F1]: $Φ$ is finite, spans the real dual, is reduced and crystallographic, and every $g_{α}$ is one-dimensional. The empty root system when $g = 0$ is included there.

Depends on

Used by

Dot-Weyl facets and single-wall translation data Definition
Fundamental weights for a chosen simple root system Definition
Minuscule weights Definition
Root reflections and the Weyl group action Definition
Standard parabolic and Levi subalgebras from a subset of simple roots Definition
The Bruhat graph and the BGG Verma sum in degree k Definition
The inversion set of a Weyl group element Definition
The A2 Weyl denominator expansion Example
The Weyl dimension formula for a fundamental sl3 module Example
Dominant integral weights are maxima of their Weyl orbits Lemma
Minuscule weights have exactly the Weyl orbit as their weights Lemma
Positive coroot pairings of a dominant integral weight Lemma
Weyl-invariant polynomials on the Cartan extend to invariant polynomials on g Lemma
Generic irreducibility and the exceptional parameter lattice Theorem

Dependency tree · two levels

28 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

Pavel Etingof, Lie Groups and Lie Algebras I (standard reference, not scraped)