CorollaryStatement: 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.

Freudenthal recursion terminates from the highest weight

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $λ \in Λ^{+}$ .

(i) $m_{λ} (λ) = 1$ , and $m_{λ} (ν) = 0$ whenever $ν \leq̸ λ$ , that is, whenever $λ - ν$ is not a nonnegative integral combination of the simple roots (The highest-weight space is one-dimensional, Highest weight modules lie below the top weight).

(ii) If $μ$ is a weight of $L (λ)$ with $μ \neq λ$ , then $(μ + ρ, μ + ρ) < (λ + ρ, λ + ρ)$ (The shifted norm of a weight is maximal only at the top weight), so Freudenthal's weight multiplicity recursion solves for $m_{λ} (μ)$ from the multiplicities $m_{λ} (μ + j α)$ , $j \geq 1$ , of strictly higher weights; since $ht (λ - (μ + j α)) < ht (λ - μ)$ and $L (λ)$ is finite-dimensional, iterating the recursion from the top weight and increasing $ht (λ - μ)$ determines $m_{λ} (μ)$ for every weight $μ \neq λ$ from the value $m_{λ} (λ) = 1$ of (i). More explicitly, for candidates $ν \in λ - Q_{+}$ put $D (ν) = (λ + ρ, λ + ρ) - (ν + ρ, ν + ρ)$ . For $ν \neq λ$ with $D (ν) \leq 0$ set $m_{λ} (ν) = 0$ , as (ii)'s strict inequality excludes such a weight. For $D (ν) > 0$ use the recursion, including candidates that turn out to have multiplicity zero. A requested candidate at height $h$ requires only the finitely many candidates of height at most $h$ .

(iii) At $μ = λ$ the recursion reads $0 = 0$ and determines nothing, so (i) is used as its base case; if $ν \leq̸ λ$ then $ν + j α \leq̸ λ$ for every $α \in Φ^{+}$ and $j \geq 1$ , and both sides of the recursion vanish by (i).

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , the finite-dimensional simple module $L (λ)$ , its multiplicities $m_{λ} (ν)$ , the positive system $Φ^{+}$ with heights, and the Weyl vector $ρ$ .

[A1]

The Axiom of Choice is assumed; it is inherited from the published highest-weight and multiplicity suppliers of [F1] and [F2] (The Axiom of Choice).

[F1]

$L (λ)$ is a finite-dimensional irreducible highest weight module of highest weight $λ$ , its $λ$ -weight space is one-dimensional, and every weight $ν$ of $L (λ)$ satisfies $ν \leq λ$ , that is, $λ - ν \in Q_{+}$ ; consequently $m_{λ} (ν) = 0$ for $ν \leq̸ λ$ (Highest-weight classification, The highest-weight space is one-dimensional, Highest weight modules lie below the top weight).

[F2]

For every weight $μ \neq λ$ of $L (λ)$ the recursion coefficient $(λ + ρ, λ + ρ) - (μ + ρ, μ + ρ)$ is strictly positive (The shifted norm of a weight is maximal only at the top weight), and the recursion of Freudenthal's weight multiplicity recursion reads $((λ + ρ, λ + ρ) - (μ + ρ, μ + ρ)) m_{λ} (μ) = 2 \sum_{α \in Φ^{+}} \sum_{j \geq 1} (μ + j α, α) m_{λ} (μ + j α) .$

[F3]

Extend root height to $Q$ by $ht (\sum_{i} n_{i} α_{i}) = \sum_{i} n_{i}$ . It is additive and positive on $Q_{+} ∖ {0}$ , so $ht (λ - (μ + j α)) = ht (λ - μ) - j ht (α) < ht (λ - μ)$ for $j \geq 1$ and $α \in Φ^{+}$ , while adding $j α$ to $ν$ can only increase it in the root order: if $ν + j α \leq λ$ then $λ - ν = (λ - ν - j α) + j α \in Q_{+}$ (Height and highest root, Finite Weyl root system, lattice and chamber conventions, Simple roots form a signed integral basis).

Proof

technique · direct

1.1F1algebraA1

By [F1] the $λ$ -weight space of $L (λ)$ is one-dimensional and every weight of $L (λ)$ lies below $λ$ , so $m_{λ} (λ) = 1$ and $m_{λ} (ν) = 0$ for every $ν \leq̸ λ$ , which is (i).

2.1F1F2F3step 1.1algebra

For every candidate $ν \in λ - Q_{+}$ put $h = ht (λ - ν)$ . We determine its actual multiplicity by induction on $h$ . At height zero the only candidate is $λ$ , whose multiplicity is $1$ . At positive height, if $D (ν) \leq 0$ , [F2] excludes $ν$ from the weight set, so its multiplicity is zero. If $D (ν) > 0$ , the recursion, valid for every $ν$ , determines its multiplicity by division by $D (ν)$ . Each term $m_{λ} (ν + j α)$ either vanishes because $ν + j α \leq̸ λ$ by [F1], or is a candidate of smaller nonnegative height by [F3] and hence already determined. In the latter case $j ht (α) \leq h$ , so only finitely many terms are required. There are finitely many tuples of nonnegative simple-root coefficients of sum at most $h$ ; thus computing any requested candidate uses finitely many induction stages and candidates. Every actual weight is among these candidates, proving (ii).

3.1F1F2F3step 1.1step 2.1algebra∎

For (iii), at $μ = λ$ the coefficient in [F2] vanishes because $μ = λ$ , while $λ + j α \leq̸ λ$ for $j \geq 1$ and $α \in Φ^{+}$ since $- j α \notin Q_{+}$ , so every multiplicity on the right vanishes by (i) and the recursion reads $0 = 0$ ; for $ν \leq̸ λ$ and $j \geq 1$ one has $ν + j α \leq̸ λ$ by [F3], so both sides of the recursion vanish by (i).

Depends on

Used by

Freudenthal recursion for the sl3 adjoint zero weight Example

Dependency tree · two levels

42 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)