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.

Existence and uniqueness of the highest root

Statement

Let ΦE be a nonempty irreducible reduced crystallographic finite root system with a chosen positive system and base Δ (Positive systems and simple roots). Then Φ has a unique highest root θ relative to this base (Height and highest root): a positive root θ such that θγ for no positive root γθ. Moreover θ is dominant: (θ,γ)0 for every positive root γ.

Facts & Assumptions

Given: A nonempty irreducible reduced crystallographic root system ΦE with positive system Φ+, base Δ={α1,,αr}, height function and root order.

[L1]

Φ is finite and spans E; 0Φ; the Cartan integers are integral, reflections preserve Φ, and the only proportional roots on a root line are a root and its negative (Reduced crystallographic Euclidean root system).

[L2]

Δ is a basis of E, every root is a unique integral combination of Δ whose nonzero coefficients have one sign, positive roots have nonnegative coefficients, and βγ means γβ is a nonnegative integral combination of simple roots (Simple roots form a signed integral basis, Height and highest root).

[L3]

If γ,δΦ are nonproportional and (γ,δ)<0 then γ+δΦ; if (γ,δ)>0 then γδΦ (Rank-two root-system classification).

[L4]

Distinct simple roots satisfy (α,β)0 (Distinct simple roots have nonpositive inner product).

[L5]

An irreducible root system admits no decomposition into two orthogonal nonempty parts spanning nonzero orthogonal subspaces that span E; the decomposition into nonempty pairwise orthogonal irreducible root systems is unique (Reducible and irreducible root systems, Unique irreducible decomposition).

Proof

technique · direct
1.1

The set Φ+ is finite and nonempty: since Φ is nonempty, choose a root and its negative, exactly one of which is positive. Hence the root order is a partial order, and a comparison chain of positive roots is finite because heights strictly increase along it; hence Φ+ has a maximal element θ, i.e. a positive root such that θγ for no positive root γθ.

L1L2algebra
1.2

Let W0 be the subgroup of the orthogonal group generated by the simple reflections; every root is in its orbit of a simple root. The generators are sα for αΔ. Let γ=iniαi, ni0, be a positive root that is not simple. Then 0<(γ,γ)=ini(γ,αi) produces an index i with (γ,αi)>0; put k=2(γ,αi)(αi,αi)>0, so that the reflected root sαi(γ)=γkαi lies in Φ by [L1]. Its simple-root coordinates are those of γ except the i-th, which is nik. If nik<0, the one-sign assertion of [L2] forces every other coordinate, which is unchanged and nonnegative, to vanish. Thus sαi(γ) is a negative multiple of αi, hence equal to αi by the reducedness clause of [L1]; applying sαi again would then give sαi(αi)=αi=γ, contrary to the choice of γ. Therefore sαi(γ) is a positive root, of height ht(γ)k<ht(γ). Iterating this strict descent, which stays at height 1 while the root is positive, must end at a simple root, since the argument would strictly lower the height of any nonsimple positive root; a simple root has height 1. Hence γ=w(δ) for a simple root δ and a product w of simple reflections. Negative roots are negatives of positive ones, and δ=sδ(δ).

L1L2algebra
2.1

The maximal root θ is dominant: (θ,αi)0 for every simple root αi. Indeed, if (θ,αi)<0, then the positive roots θ,αi cannot be proportional: reducedness would force equality, giving a positive pairing. Thus θ+αiΦ by [L3] applied to the nonproportional pair (αi,θ); this root is positive (a sum of positive roots) and θ+αi>θ because the difference is the simple root αi, contradicting maximality of θ.

L2L3step 1.1algebra
2.2

The Dynkin diagram of Φ, with vertices Δ and an edge between αi,αj when (αi,αj)0, is connected. Otherwise Δ=ST with (αi,αj)=0 for all iS, jT; then each sαi, iS, fixes every αj, jT, and vice versa, so the subgroup generated by the two families is their commuting product WSWT and W0Δ=(WSS)(WTT) by step 1.2; the spans of WSSspanS and WTTspanT are nonzero, orthogonal, and span E, so Φ would be reducible, contradicting [L5].

L5step 1.2algebra
3.1

The support of θ is all of Δ: write θ=iniαi with ni0. If ni=0 for some i, then by step 2.1 and [L4] 0(θ,αi)=j:nj>0nj(αj,αi)0, so (αj,αi)=0 for every j with nj>0, that is, no vertex outside the nonempty support of θ is adjacent in the diagram to any vertex of the support; this contradicts the connectedness of step 2.2.

L4step 2.1step 2.2algebra
4.1

At least one simple root pairs strictly positively with θ. Indeed step 3.1 writes θ=iniαi with every ni>0, while step 2.1 gives (θ,αi)0 for every i. Since 0<(θ,θ)=ini(θ,αi), not all these nonnegative pairings can vanish.

step 2.1step 3.1algebra
5.1

Uniqueness: let θ be a second highest root. Steps 2.1 through 3.1 apply equally to θ, so θ=iciαi with every ci>0. Together with steps 2.1 and 4.1 this gives (θ,θ)=ici(θ,αi)>0. If θ and θ were proportional, reducedness and positivity would already force θ=θ. Otherwise [L3] gives θθΦ; this root is positive, in which case θ<θ and θ is not maximal, or negative, in which case θ<θ and θ is not maximal. Both alternatives are impossible, so θ=θ.

L1L2L3step 2.1step 3.1step 4.1algebra
6.1

The dominance statement for all positive roots follows because (θ,γ)=ici(θ,αi)0 whenever γ=iciαi is positive with ci0, using step 2.1. Every positive root lies below a maximal root by finiteness; uniqueness makes that maximal root θ, so θ is also the greatest positive root. In rank one Φ={α,α}, and θ=α. The empty system in E=0 remains irreducible under the library definition but is expressly excluded here; it has no highest root. Dominance need not be strict on every simple root: in A3, θ=ε1ε4 pairs to zero with α2=ε2ε3. This completes the proof.

step 2.1step 5.1algebra

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