ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 for the sl3 adjoint zero weight

Example

Assume the Axiom of Choice (The Axiom of Choice). Keep the setting of Kostant multiplicity in the sl3 adjoint module: $g = {s l}_{3}$ , $λ = θ = α_{1} + α_{2} = ρ$ , $μ = 0$ . Then $(λ + ρ, λ + ρ) - (μ + ρ, μ + ρ) = (2 θ, 2 θ) - (θ, θ) = 3 (θ, θ)$ , and in the right side of Freudenthal's weight multiplicity recursion only $j = 1$ contributes, since $2 α, 3 α, \dots$ are not weights of the adjoint module $L (θ)$ ; hence the recursion reads $3 (θ, θ) m_{λ} (0) = 2 \sum_{α \in Φ^{+}} (α, α) m_{λ} (α)$ . In the realization $α_{1} = e_{1} - e_{2}$ , $α_{2} = e_{2} - e_{3}$ , $θ = e_{1} - e_{3}$ of Root systems of the classical complex Lie algebras the three positive roots have the same length, and $m_{λ} (α_{1}) = m_{λ} (α_{2}) = m_{λ} (θ) = 1$ , so $3 (θ, θ) m_{λ} (0) = 2 \cdot 3 (θ, θ)$ and $m_{λ} (0) = 2$ , recovering Kostant multiplicity in the sl3 adjoint module. The extremal weights $\pm α_{1}, \pm α_{2}, \pm θ = W λ$ are the Weyl orbit of the top weight and each has multiplicity one (Extremal Weyl-orbit weights); among them only the top weight $θ = λ$ has the vanishing recursion coefficient of the indeterminate case $0 = 0$ in Freudenthal recursion terminates from the highest weight, whose base value $m_{λ} (λ) = 1$ is stated there.

Facts & Assumptions

Given: The Axiom of Choice, the realization of ${s l}_{3}$ with positive roots $α_{1}, α_{2}, θ = α_{1} + α_{2}$ of equal length, the Weyl vector $ρ = θ$ , the top weight $λ = θ$ , the weight $μ = 0$ , the adjoint module $L (θ)$ , and the multiplicities $m_{θ} (ν)$ .

[A1]

The Axiom of Choice is assumed; it enters through the Freudenthal recursion and the highest-weight suppliers below (The Axiom of Choice).

[F1]

In the realization $α_{1} = e_{1} - e_{2}$ , $α_{2} = e_{2} - e_{3}$ the positive roots are $α_{1}, α_{2}, θ$ with $(α_{1}, α_{1}) = (α_{2}, α_{2}) = (θ, θ)$ , and $ρ = α_{1} + α_{2} = θ$ (Root systems of the classical complex Lie algebras, Classical complex matrix Lie algebras, The Weyl vector rho for a chosen positive system).

[F2]

The adjoint module is $L (θ)$ and its weights are $0$ with multiplicity $2$ , and $\pm α_{1}, \pm α_{2}, \pm θ$ each with multiplicity $1$ (The adjoint highest weight is the highest root, Kostant multiplicity in the sl3 adjoint module).

[F3]

Freudenthal's recursion reads $((λ + ρ, λ + ρ) - (μ + ρ, μ + ρ)) m_{λ} (μ) = 2 \sum_{α \in Φ^{+}} \sum_{j \geq 1} (μ + j α, α) m_{λ} (μ + j α)$ (Freudenthal's weight multiplicity recursion).

[F4]

The extremal weights $W λ$ each have multiplicity one, and the recursion has the base value $m_{λ} (λ) = 1$ with the indeterminate case $0 = 0$ occurring, among actual weights of $L (λ)$ , only at $μ = λ$ (Extremal Weyl-orbit weights, Freudenthal recursion terminates from the highest weight).

Verification

1.1F2F3A1

With $λ = θ = ρ$ and $μ = 0$ the recursion coefficient of [F3] is $(2 θ, 2 θ) - (θ, θ) = 3 (θ, θ)$ , and the weights $0 + j α = j α$ of $L (θ)$ are nonzero only for $j = 1$ by the weight list [F2], so each inner sum of $2 \sum_{α \in Φ^{+}} \sum_{j \geq 1} (α j, α) m (j α)$ reduces to its $j = 1$ term $(α, α) m (α)$ .

1.2F1F2

By [F1] all three positive roots have the same squared length, and by [F2] $m (α_{1}) = m (α_{2}) = m (θ) = 1$ , so the right side of the recursion is $2 ((α_{1}, α_{1}) + (α_{2}, α_{2}) + (θ, θ)) = 6 (θ, θ)$ .

2.1F2step 1.1step 1.2

Combining steps 1.1 and 1.2, the recursion reads $3 (θ, θ) m_{θ} (0) = 6 (θ, θ)$ , and since $(θ, θ) \neq 0$ this gives $m_{θ} (0) = 2$ , recovering the value computed by Kostant's formula in [F2].

3.1F4step 1.1∎

The extremal weights are the six Weyl translates of $λ = θ$ , each of multiplicity one by [F4]; the recursion coefficient $4 (θ, θ) - (μ + ρ, μ + ρ)$ vanishes, among actual weights of $L (θ)$ , only at $μ = λ$ by [F4], so among the extremal weights only the top weight is the indeterminate case of the recursion, whose value $m_{θ} (θ) = 1$ is the stated base case; this is consistent with the recursion fixing every other multiplicity from that base.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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