LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Positive root strings sum the Freudenthal correction

Statement

Assume the Axiom of Choice. Keep the notation of The Casimir comparison on a weight space: $g$ is a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra $h$ and positive system $Φ^{+}$ , the vectors $e_{α} \in g_{α}$ and $f_{α} \in g_{- α}$ satisfy $B (e_{α}, f_{α}) = 1$ , so that $[e_{α}, f_{α}] = H_{α}$ is the Killing-dual vector of $α$ , and $m_{λ} (μ) = \dim L (λ)_{μ}$ for $λ \in Λ^{+}$ . Then for every $λ \in Λ^{+}$ , $μ \in h^{*}$ and $α \in Φ^{+}$ , ${tr}_{L (λ)_{μ}} (e_{α} f_{α} + f_{α} e_{α}) = m_{λ} (μ) (μ, α) + 2 \sum_{j \geq 1} m_{λ} (μ + j α) (μ + j α, α),$ the sum being finite because $L (λ)$ has only finitely many weights.

Facts & Assumptions

Given: The Axiom of Choice, such $g, h, Φ^{+}$ , vectors $e_{α}, f_{α}$ with $B (e_{α}, f_{α}) = 1$ for a fixed $α \in Φ^{+}$ , a dominant integral weight $λ$ , and an element $μ \in h^{*}$ .

[A1]

The Axiom of Choice is assumed; it enters only through the published classification and Casimir suppliers used in [F4] (The Axiom of Choice).

[F1]

On the weight space $L (λ)_{ν}$ the Cartan element $H_{α}$ acts by the scalar $(ν, α)$ , and $[e_{α}, f_{α}] = H_{α}$ (The Casimir comparison on a weight space, Opposite root spaces bracket to the Killing-dual line).

[F2]

$e_{α}$ maps $L (λ)_{ν}$ into $L (λ)_{ν + α}$ and $f_{α}$ maps it into $L (λ)_{ν - α}$ (Root vectors shift weights, Weight and weight space).

[F3]

The weight set of $L (λ)$ is finite, since its distinct nonzero weight spaces are independent in a finite-dimensional vector space (Weight and weight space, Highest-weight classification).

[F4]

$L (λ)$ is a finite-dimensional irreducible highest weight module of highest weight $λ$ , so all its weight spaces are finite-dimensional and the traces below are finite sums of matrix traces (Highest-weight classification, The Casimir comparison on a weight space).

Proof

technique · direct

1.1F2F3F4A1

Fix $α \in Φ^{+}$ and set $V_{i} = L (λ)_{μ + i α}$ for every $i \in Z$ , allowing $V_{i} = 0$ . Let $A_{i} : V_{i} \to V_{i + 1}$ and $B_{i + 1} : V_{i + 1} \to V_{i}$ be the actions of $e_{α}, f_{α}$ , and put $T_{i} = {tr}_{V_{i}} (B_{i + 1} A_{i})$ . By [F3] there is an integer $N \geq 0$ such that $V_{i} = 0$ for all $i > N$ , even if the whole line contains no weights; in particular $T_{N} = 0$ .

2.1F1F4step 1.1algebra

For maps $A : U \to Z$ and $B : Z \to U$ between finite-dimensional spaces, ${tr}_{U} (B A) = {tr}_{Z} (A B)$ : in bases both traces equal $\sum_{p, q} B_{p q} A_{q p}$ , including zero-dimensional spaces. Applying this to $A_{i}, B_{i + 1}$ and using $[e_{α}, f_{α}] = H_{α}$ on $V_{i + 1}$ gives $T_{i} = T_{i + 1} + m_{λ} (μ + (i + 1) α) (μ + (i + 1) α, α)$ . Telescoping from $i = 0$ to $N$ therefore gives $T_{0} = \sum_{j \geq 1} m_{λ} (μ + j α) (μ + j α, α)$ , with only finitely many nonzero terms.

3.1F1step 1.1step 2.1algebra∎

On $V_{0}$ , the commutator identity gives $tr (e_{α} f_{α}) = tr (f_{α} e_{α}) + m_{λ} (μ) (μ, α) = T_{0} + m_{λ} (μ) (μ, α)$ . Adding the trace of $f_{α} e_{α}$ and substituting step 2.1 proves the asserted formula, including absent weights and an empty line.

Depends on

Used by

Freudenthal's weight multiplicity recursion Theorem

Dependency tree · two levels

40 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

A. Moreau, Representation Theory of Lie Algebras (M2, Université Paris-Saclay, 2025--2026) (standard reference, not scraped)
R. Borcherds, Berkeley Math 261 course notes, page on the Freudenthal multiplicity formula (standard reference, not scraped)
P. Etingof, Lie Groups and Lie Algebras II (MIT 18.755, Spring 2024), complete lectures (standard reference, not scraped)