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

Simple-root integrability relations

Statement

Assume the Axiom of Choice. Let g be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra h and a chosen positive system with simple roots α1,,αr, let λ be dominant integral with mi=λ,αi (Integral, dominant, and strictly dominant weights), and let V be a finite-dimensional highest weight module of highest weight λ with highest weight vector vλ (Highest-weight vectors and modules). For every simple root αi and a lowering vector figαi with [ei,fi]=hαi for a suitable ei (The root sl_2 triple), fimi+1vλ=0.

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a dominant integral λ with mi=λ,αi, a finite-dimensional highest weight module V of highest weight λ, and for each i a pair eigαi, figαi forming, together with hαi, a copy of sl2.

[A1]

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

[L1]

For every i, [ei,fi]=hαi, [hαi,ei]=2ei and [hαi,fi]=2fi (The root sl_2 triple).

[L2]

vλ0 is killed by n+ and satisfies hαivλ=λ(hαi)vλ=mivλ (Highest-weight vectors and modules, Integral, dominant, and strictly dominant weights).

[L3]

A finite-dimensional sl2-module is a direct sum of irreducibles, and an irreducible submodule with highest weight m0 has dimension m+1 and weights m,m2,,m (Finite-dimensional representations of sl_2).

Proof

technique · direct
1.1

Fix i and consider W=U(span{ei,fi,hαi})vλ, the sl2-submodule of V generated by vλ; it is finite dimensional because V is, and eivλ=0 while hαivλ=mivλ by [L1] and [L2].

A1L1L2
2.1

By [L3] write W=a=1sWa as a direct sum of irreducible sl2-submodules, and write vλ=ava with vaWa. Because every Wa is stable under ei and hαi, uniqueness of the direct sum and step 1.1 give eiva=0 and hαiva=miva for every a.

L3step 1.1
3.1

For every a with va0, step 2.1 makes va a highest weight vector of the irreducible module Wa with highest weight mi. By [L3], fimi+1va=0; the same equality is trivial when va=0. Summing over a gives fimi+1vλ=0 in W.

L3step 2.1
4.1

Since WV, the vanishing of step 3.1 holds in V; as i was arbitrary, fimi+1vλ=0 for every simple root, which is the assertion.

step 3.1

Depends on

Used by

Dependency tree · two levels

31 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