TheoremStatement: 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.

Simple roots form a signed integral basis

Statement

Let $Φ \subseteq E$ be a reduced crystallographic root system with positive system $Φ^{+}$ and simple roots $Δ \subseteq Φ^{+}$ (Positive systems and simple roots). Then $Δ$ is a basis of $E$ ; more precisely:

$Δ$ is linearly independent and spans $E$ , so $∣ Δ ∣ = \dim E$ ;
every positive root is a sum of simple roots with nonnegative integer coefficients, and every negative root is a sum of simple roots with nonpositive integer coefficients.

Consequently every root is a unique integral combination $\sum_{α \in Δ} n_{α} α$ of the simple roots in which the nonzero coefficients all have the same sign, positive for positive roots and negative for negative roots.

Facts & Assumptions

Given: A reduced crystallographic root system $Φ \subseteq E$ with a regular vector $v \in E$ , the positive system $Φ^{+} = {α : (v, α) > 0}$ , and the set $Δ$ of simple roots, a root being simple when it is not a sum of two positive roots.

[L1]

$Φ$ is finite, spans $E$ , $0 \notin Φ$ , $s_{α} (Φ) = Φ$ , all Cartan integers are integral, and $R α \cap Φ = {\pm α}$ (Reduced crystallographic Euclidean root system).

[L2]

$Φ^{+} = {α : (v, α) > 0}$ and $Φ^{-} = - Φ^{+}$ are disjoint and cover $Φ$ ; a positive root is simple when it is not a sum of two positive roots (Positive systems and simple roots).

[L3]

If $α, β$ are nonproportional roots with $(α, β) > 0$ then $α - β \in Φ$ (Rank-two root-system classification).

Proof

technique · direct

1.1

Every positive root is a nonnegative integral sum of simple roots: if $α \in Φ^{+}$ is not simple, it is a sum $α = β + γ$ of two positive roots, and $(v, β), (v, γ)$ are positive and add up to $(v, α)$ ; iterating this decomposition and always choosing a summand that is not simple cannot continue forever, since the finitely many values $(v, δ)$ , $δ \in Φ^{+}$ , strictly decrease along each branch, so the process terminates and exhibits $α$ as a sum of simple roots.

L1L2algebra

1.2

Distinct simple roots $α, β$ satisfy $(α, β) \leq 0$ . Indeed, if $(α, β) > 0$ then $α - β \in Φ$ by [L3]; this root is positive or negative, and if it is positive then $α = (α - β) + β$ is a nontrivial sum of two positive roots, while if it is negative then $β = (β - α) + α$ is a nontrivial sum of two positive roots, contradicting the simplicity of $α$ or of $β$ .

L2L3algebra

2.1

The simple roots are linearly independent. Suppose $\sum_{i \in I} c_{i} α_{i} = \sum_{j \in J} c_{j} α_{j}$ with disjoint nonempty index sets and all $c_{i}, c_{j} > 0$ ; this is the shape of every nontrivial real linear relation, after moving negative coefficients to the other side. The common vector $γ = \sum_{i \in I} c_{i} α_{i}$ is nonzero, so $(γ, γ) > 0$ ; on the other hand, expanding one side against the other gives $(γ, γ) = \sum_{i \in I, j \in J} c_{i} c_{j} (α_{i}, α_{j}) \leq 0$ , because $I \cap J = \emptyset$ and distinct simple roots have nonpositive inner product by step 1.2. This contradiction shows all coefficients vanish, so $Δ$ is linearly independent.

L1step 1.2algebra

3.1

The simple roots span $E$ : every root is a simple-root combination by step 1.1 or its negative, and $Φ$ spans $E$ . Together with step 2.1 the set $Δ$ is a basis of $E$ , and with step 1.1 every root is an integral combination whose coefficients all have the sign of the root. Uniqueness of the coefficients is basis uniqueness, and no choice-theoretic input is used.

L1step 1.1step 2.1algebra∎

Depends on

Used by

Height and highest root Definition
Integral, dominant, and strictly dominant weights Definition
Open and closed Weyl chambers Definition
Positive and negative nilpotent subalgebras and the Borel Definition
Root order on weights Definition
Root, coroot, weight, and coweight lattices Definition
Satake diagram Definition
Vogan diagram Definition
Positive roots and highest root of G₂ Example
Chevalley basis and real structure constants Lemma
Every finite-dimensional irreducible module has a highest-weight vector Lemma
Highest weight modules lie below the top weight Lemma
Simple-root integrability bounds the dominant cyclic module Lemma
The dominant cyclic generator survives Lemma
Weyl denominator and anti-invariant orbit sums Lemma
Central quotients and intermediate character lattices Proposition
Dominant weights in fundamental coordinates Proposition
Duality exchanges B and C Proposition
Existence and uniqueness of the highest root Proposition
Extremal Weyl-orbit weights Proposition
Highest weight of the dual representation Proposition
Irreducibility and connected Dynkin diagrams Proposition
Positive systems, bases, and chambers Proposition
Properties of finite-type Cartan matrices Proposition
Restricted root systems may be nonreduced Proposition
Root and weight lattice sandwich Proposition
The adjoint highest weight is the highest root Proposition
The roots form a reduced crystallographic Euclidean root system Proposition
The Weyl vector in fundamental coordinates Proposition
Top summand in a tensor product Proposition
Weyl length equals inversion number Proposition
Analytic and root-system Weyl groups agree Theorem
Classification of irreducible root systems Theorem
Classification of real forms by Vogan diagrams Theorem
Existence and uniqueness up to isomorphism of the split real form Theorem
Existence of each classified root system Theorem
Existence theorem for complex semisimple Lie algebras Theorem
Semisimple compact groups up to isogeny Theorem
Serre presentation theorem Theorem
Simple transitivity on Weyl chambers Theorem

…and 3 more results.

Dependency tree · two levels

9 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

Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed., Chapter II (standard reference, not scraped)