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.

Root vectors shift weights

Statement

Let g be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra h, let V be a representation of g, let α be a root and let gα be its root space (Root and root space). If x∈gα and v∈Vμ for some μ∈h∗, then x⋅v∈Vμ+α (Weight and weight space); in particular x⋅v=0 is allowed.

Facts & Assumptions

Given: Such g,h,V, a root α, x∈gα, μ∈h∗ and v∈Vμ.

[L1]

The action of g on V is a Lie algebra homomorphism into the endomorphisms of V with commutator bracket (Representations of Lie algebras): for all X,Y and w, X⋅(Y⋅w)−Y⋅(X⋅w)=[X,Y]⋅w.

[L2]

gα={x:[H,x]=α(H)x for all H∈h} (Root and root space), so H⋅v=μ(H)v and [H,x]=α(H)x for H∈h.

Proof

technique · direct
1.1L1L2

Let H∈h; using [L1] with X=H, Y=x, w=v and [L2], H⋅(x⋅v)=[H,x]⋅v+x⋅(H⋅v)=α(H) x⋅v+μ(H) x⋅v=(α+μ)(H) (x⋅v).

2.1step 1.1

Equation 1.1 says precisely that x⋅v is annihilated by ρ(H)−(μ+α)(H)id⁡V for every H∈h, that is, x⋅v∈Vμ+α (Weight and weight space); this includes the possibility x⋅v=0, which lies in every subspace.

3.1step 2.1∎

Steps 1.1 and 2.1 prove the stated containment, including the zero case.

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