Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Simple roots and fundamental weights of A_n

Example

For An realized in the sum-zero subspace E={x∈Rn+1:∑ixi=0} the simple roots are αi=ei−ei+1, 1≤i≤n, and the fundamental weights are ωk=e1+⋯+ek−kn+1∑i=1n+1ei,1≤k≤n.

Facts & Assumptions

Given: The model An={εi−εj:i≠j} in the sum-zero subspace of Rn+1, with simple roots αi=ei−ei+1 and the vectors ωk displayed.

[L1]

In this model An is a reduced crystallographic root system with simple roots αi=ei−ei+1 (Classical root systems in coordinates, Existence of each classified root system).

[L2]

The coroot of α is α∨=2α/(α,α) and the fundamental weights are the vectors dual to the simple coroots, (ωk,αi∨)=δki (Fundamental weights, Coroot and dual root system).

Verification

technique · direct
1.1L1L2algebra

(αi,αi)=2 and αi∨=αi, since αi has two nonzero coordinates equal to ±1.

2.1L2step 1.1algebra∎

For every i,k one has (ωk,αi)=(ωk,ei)−(ωk,ei+1); the vector ωk has coordinates 1−k/(n+1) in positions 1,…,k and −k/(n+1) in positions k+1,…,n+1, so the difference equals 1 when i=k and 0 otherwise. Hence (ωk,αi∨)=δki and the displayed vectors are the fundamental weights of An; they form a basis of the weight lattice by [L2].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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