Alphabeta Math
PropositionStatement: 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.

The Weyl vector in fundamental coordinates

Statement

Let Φ⊆E be a reduced crystallographic root system with positive system Φ+, base Δ={α1,…,αr} and Weyl vector ρ (The Weyl vector). Then (ρ,αi∨)=1(i=1,…,r), and therefore ρ=∑i=1rωi, where ω1,…,ωr are the fundamental weights (Fundamental weights).

Facts & Assumptions

Given: Such a root system Φ⊆E, its positive system Φ+ with base Δ={α1,…,αr}, the Weyl vector ρ and the fundamental weights ωi.

[L1]

The reflection si=sαi acts by si(x)=x−(x,αi∨)αi with αi∨=2αi/(αi,αi), and si(αi)=−αi (Weyl group, Coroot and dual root system).

[L2]

Every positive root is a nonnegative integral combination of the simple roots, and these coefficients are unique; Rα∩Φ={α,−α} (Simple roots form a signed integral basis, Reduced crystallographic Euclidean root system).

[L3]

The fundamental weights are the vectors dual to the simple coroots, (ωi,αj∨)=δij, and they form a basis of the weight lattice; the simple coroots form a basis of E (Fundamental weights).

Proof

technique · direct
1.1L1L2

Let α∈Φ+ with α≠αi; writing α=∑jnjαj with nj≥0 by [L2], some nj with j≠i is positive, since otherwise α=niαi and reducedness with α a positive root forces ni=1 and α=αi; hence si(α) has the positive coefficient nj>0 at position j≠i, and since si(α) is a root its coefficient vector has one sign by [L2], so si(α)∈Φ+; moreover si(α)≠αi because si(αi)=−αi and si is an involution; thus si maps Φ+∖{αi} onto itself.

2.1L1step 1.1

Using step 1.1 and si(αi)=−αi, si(2ρ)=∑α∈Φ+si(α)=∑α≠αiα−αi=2ρ−2αi, hence si(ρ)=ρ−αi.

3.1L1step 2.1

On the other hand si(ρ)=ρ−(ρ,αi∨)αi by [L1]; comparing with step 2.1 and using that αi≠0 gives (ρ,αi∨)=1 for every i.

4.1L3step 3.1

The difference ρ−∑jωj satisfies (ρ−∑jωj,αi∨)=1−1=0 for every i by [L3] and step 3.1; since the simple coroots form a basis of E and the inner product is nondegenerate, ρ−∑jωj=0, that is, ρ=∑jωj.

5.1step 3.1step 4.1∎

Both assertions are proved.

Depends on

Used by

Dependency tree · two levels

10 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