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.

Dominant weights in fundamental coordinates

Statement

Assume the Axiom of Choice. Let g be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra h and a chosen base of simple roots, and let ω1,,ωr be the fundamental weights (Fundamental weights). For λh the following are equivalent:

(i) λ is dominant integral (Integral, dominant, and strictly dominant weights);

(ii) λ=i=1rniωi with integers ni0.

Facts & Assumptions

Given: The Axiom of Choice, such g,h and a chosen base of simple roots α1,,αr with fundamental weights ω1,,ωr.

[A1]

The Axiom of Choice is assumed; it enters through the root-space theory supplying the real form and the coroot basis of [L1] (The Axiom of Choice).

[L1]

The simple coroots hα1,,hαr form a basis of h; the simple roots form a basis of E=spanRΦ; and the fundamental weights are the dual basis to the simple coroots, (ωi,αj)=δij, and form a basis of the weight lattice P (The roots form a reduced crystallographic Euclidean root system, Simple roots form a signed integral basis, Fundamental weights, Root, coroot, weight, and coweight lattices).

[L2]

λ is integral when λ,αi=λ(hαi)Z for all i, dominant integral when all these integers are nonnegative, and every integral functional lies in E; for λE the expansion in the dual basis is λ=iλ,αiωi (Integral, dominant, and strictly dominant weights).

Proof

technique · direct
1.1

Assume (i): then by [L2] λE and ni:=λ,αiZ0 for every i, so the expansion λ=iniωi of [L2] exhibits λ in the form (ii).

A1L2
1.2

Conversely assume (ii), say λ=iniωi with niZ0; then λPE by [L1], and by the duality (ωi,αj)=δij of [L1] we get λ,αj=iniδij=njZ0 for each j.

L1
2.1

By [L2] the pairings of step 1.2 are exactly the values that make λ dominant integral; hence (ii) implies (i), and steps 1.1 and 2.1 prove the equivalence.

L2step 1.1step 1.2

Depends on

Used by

Dependency tree · two levels

27 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