TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.1L1L2algebra

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.

1.2L2L3algebra

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 $β$ .

2.1L1L2step 1.2algebra

The simple roots are linearly independent. For coefficients $c_{i} \geq 0$ with at least one $c_{i} > 0$ , a combination $\sum_{i} c_{i} α_{i}$ of simple roots satisfies $(v, \sum_{i} c_{i} α_{i}) = \sum_{i} c_{i} (v, α_{i}) > 0$ by [L2], so it cannot vanish; negating also excludes a nonzero relation with all coefficients nonpositive. Thus any nontrivial real linear relation can be written $\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$ . Its common vector $γ = \sum_{i \in I} c_{i} α_{i}$ satisfies $(v, γ) > 0$ , hence $γ \neq 0$ and $(γ, γ) > 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$ , since distinct simple roots have nonpositive inner product by step 1.2. This contradiction proves linear independence.

3.1L1step 1.1step 2.1algebra∎

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.

Depends on

Used by

Antidominant regular Verma modules are simple Corollary
Freudenthal recursion terminates from the highest weight Corollary
I₂(5) admits no crystallographic scaling and no reduced crystallographic root system with that base pairing Counterexample
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
Standard parabolic and Levi subalgebras from a subset of simple roots Definition
The Kostant partition function Definition
Vogan diagram Definition
Degree-one Kostant classes correspond to simple reflections Example
Positive roots and highest root of G₂ Example
The extended affine Weyl group and non-trivial alcove stabilizers Example
Affine reflections: translation form, involutivity, local finiteness, and Wₐ=Q^∨⋊ W Lemma
Chevalley basis and real structure constants Lemma
Combinatorics of a reduced root datum Lemma
Crystallographic alcove diagrams: the affine list realized by Weyl types A–G Lemma
Every finite-dimensional irreducible module has a highest-weight vector Lemma
Geometric series are invertible in the completed character ring Lemma
Highest weight modules lie below the top weight Lemma
Highest-root dominance and the fundamental alcove Lemma
Minimal parabolic from one negative simple root Lemma
Minuscule weights have exactly the Weyl orbit as their weights Lemma
Normality of the nilpotent cone and Springer functions Lemma
Rational highest-weight modules from adjoint Plücker vectors Lemma
Simple-root integrability bounds the dominant cyclic module Lemma
The difference of the Weyl vector from its reflections is a sum of positive roots Lemma
The dominant cyclic generator survives Lemma
The extremal weight cochain of a Weyl element is closed and unique Lemma
The shifted norm of a weight is maximal only at the top weight 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

…and 25 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)