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.

The shifted norm of a weight is maximal only at the top weight

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $λ \in Λ^{+}$ be a dominant integral weight and let $μ$ be a weight of the finite-dimensional simple module $L (λ)$ (Highest-weight classification, Weight and weight space). With $ρ$ the Weyl vector (The Weyl vector rho for a chosen positive system), $(μ + ρ, μ + ρ) \leq (λ + ρ, λ + ρ),$ with equality if and only if $μ = λ$ . Consequently $(λ + ρ, λ + ρ) - (μ + ρ, μ + ρ)$ is strictly positive for every weight $μ \neq λ$ of $L (λ)$ .

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , a weight $μ$ of $L (λ)$ , the form $(,)$ on $E = {span}_{R} Φ$ , the Weyl group $W$ and the Weyl vector $ρ$ .

[A1]

The Axiom of Choice is assumed; it enters through the published weight-multiplicity and highest-weight suppliers, which carry it (The Axiom of Choice).

[F1]

Every $W$ -orbit in $E$ has exactly one point in the closed chamber $\overline{C}$ , so every weight has a unique dominant representative (Finite Weyl closed chambers and stabilizers, Finite Weyl root system, lattice and chamber conventions), and the weight multiplicities of $L (λ)$ are $W$ -invariant, so the weight set of $L (λ)$ is stable under $W$ (Simple reflections preserve weight multiplicities).

[F2]

Every weight $ν$ of $L (λ)$ satisfies $ν \leq λ$ , that is, $λ - ν \in Q_{+}$ (Highest weight modules lie below the top weight, Simple roots form a signed integral basis).

[F3]

For every $w \in W$ one has $ρ - w ρ = \sum_{α \in Φ^{+}, w^{- 1} α < 0} α \in Q_{+}$ (The difference of the Weyl vector from its reflections is a sum of positive roots).

[F4]

The action of $W$ on $E$ is by isometries of $(,)$ : $(w ν, w η) = (ν, η)$ (Finite Weyl root system, lattice and chamber conventions, Root reflections and the Weyl group action).

[F5]

Pairings against $Q_{+}$ : for $δ \in Q_{+} ∖ {0}$ one has $(δ, ρ) > 0$ ; for $δ \in Q_{+}$ and a dominant $ν$ one has $(δ, ν) \geq 0$ , because writing $δ = \sum_{i} n_{i} α_{i}$ with $n_{i} \geq 0$ gives $(α_{i}, ν) = \frac{(α_{i}, α_{i})}{2} ⟨ ν, α_{i}^{\lor} ⟩$ and $⟨ ρ, α_{i}^{\lor} ⟩ > 0$ , so in particular $μ^{+} + ρ$ is strictly dominant (Positive coroot pairings of a dominant integral weight, Integral, dominant, and strictly dominant weights).

[F6]

For a dominant integral $λ$ and $v \in W$ with reduced expression $v = s_{i_{1}} \dots s_{i_{k}}$ one has $λ - v λ = \sum_{l = 1}^{k} ⟨ λ, α_{i_{l}}^{\lor} ⟩ β_{l}$ with every $β_{l} = s_{i_{1}} \dots s_{i_{l - 1}} α_{i_{l}}$ a positive root and every coefficient $⟨ λ, α_{i_{l}}^{\lor} ⟩ \geq 0$ ; this is the reduced-word telescoping with prefix positivity from Finite Weyl strong exchange and deletion and Finite Weyl positive roots and simple reflections.

Proof

technique · direct

1.1F1F2F3F4algebraA1

Let $μ^{+}$ be the unique dominant representative of the $W$ -orbit of $μ$ , which exists by [F1], and note that $μ^{+}$ is also a weight of $L (λ)$ by the $W$ -invariance in [F1]; choose $w \in W$ with $μ^{+} = w μ$ and put $δ : = λ - μ^{+}$ , so that $δ \in Q_{+}$ by [F2], and put $γ : = ρ - w ρ$ , so that $γ \in Q_{+}$ by [F3]; since $w$ is an isometry by [F4], $(μ + ρ, μ + ρ) = (w (μ + ρ), w (μ + ρ)) = (μ^{+} + w ρ, μ^{+} + w ρ)$ and $μ^{+} + w ρ = μ^{+} + ρ - γ$ .

2.1F4step 1.1algebra

With $D : = (λ + ρ, λ + ρ) - (μ + ρ, μ + ρ)$ steps 1.1 gives $D = (μ^{+} + ρ + δ, μ^{+} + ρ + δ) - (μ^{+} + ρ - γ, μ^{+} + ρ - γ) = (δ + γ, 2 (μ^{+} + ρ) + δ - γ)$ , and expanding this bilinear expression yields $D = 2 (δ, μ^{+} + ρ) + (δ, δ) + 2 (γ, μ^{+}) + (2 (γ, ρ) - (γ, γ))$ ; the last bracket is $(γ, 2 ρ - γ) = (ρ - w ρ, ρ + w ρ) = (ρ, ρ) - (w ρ, w ρ) = 0$ by symmetry and the isometry property [F4].

3.1F5step 2.1algebra

Hence $D = 2 (δ, μ^{+} + ρ) + (δ, δ) + 2 (γ, μ^{+})$ with $δ, γ \in Q_{+}$ by step 1.1; the first term is nonnegative and the third is nonnegative because $μ^{+}$ is dominant and $μ^{+} + ρ$ is strictly dominant, while $(δ, δ) \geq 0$ by positive definiteness of the form, so $D \geq 0$ ; if $δ \neq 0$ then $D \geq 2 (δ, ρ) > 0$ by [F5], so equality forces $δ = 0$ , that is, $μ^{+} = λ$ .

4.1F5F6step 1.1step 2.1step 3.1algebra∎

Suppose $δ = 0$ , so $μ^{+} = λ$ and $μ = w^{- 1} λ$ ; then steps 1.1 and 2.1 give $D = 2 (γ, λ) = 2 ((ρ, λ) - (w ρ, λ)) = 2 (ρ, λ - w^{- 1} λ) = 2 (ρ, λ - μ)$ , and [F6] applied to $v = w^{- 1}$ writes $λ - μ = \sum_{l} ⟨ λ, α_{i_{l}}^{\lor} ⟩ β_{l}$ with $β_{l} \in Φ^{+}$ and coefficients $\geq 0$ , so $D = 2 \sum_{l} ⟨ λ, α_{i_{l}}^{\lor} ⟩ (ρ, β_{l}) \geq 0$ ; by [F5] each $(ρ, β_{l}) > 0$ , and the sum vanishes exactly when $λ - μ = 0$ , that is, when $μ = λ$ , while for $w = 1$ and $μ = λ$ clearly $D = 0$ ; combining with step 3.1, $D \geq 0$ with equality exactly for $μ = λ$ , and $D > 0$ for every weight $μ \neq λ$ .

Depends on

Used by

Freudenthal recursion terminates from the highest weight Corollary

Dependency tree · two levels

53 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

P. Etingof, Lie Groups and Lie Algebras II (MIT 18.755, Spring 2024), complete lectures (standard reference, not scraped)
R. Borcherds, Berkeley Math 261 course notes, page on the Freudenthal multiplicity formula (standard reference, not scraped)