TheoremStatement: 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 Weyl character formula

Statement

Assume the Axiom of Choice (The Axiom of Choice). For every dominant integral weight $λ \in Λ^{+}$ , the character of the finite-dimensional simple module $L (λ)$ is $ch L (λ) = A (λ + ρ) \cdot A (ρ)^{- 1} = (\sum_{w \in W} (- 1)^{ℓ (w)} e^{w (λ + ρ)}) / (e^{ρ} \prod_{α \in Φ^{+}} (1 - e^{- α})),$ the quotient being taken in the completed character ring $R$ of The completed formal character ring, where $A (ρ)$ is invertible with inverse $e^{- ρ} \prod_{α \in Φ^{+}} (1 - e^{- α})^{- 1}$ (The Weyl denominator identity, Geometric series are invertible in the completed character ring). No quotient of ordinary functions is intended before this formal cancellation is justified.

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , the character $ch L (λ)$ , the Weyl vector $ρ$ , the alternants $A (ν)$ and the ring $R$ .

[A1]

The Axiom of Choice is assumed; it enters through the BGG numerator identity [F1] (The Axiom of Choice).

[F1]

$ch L (λ) \cdot A (ρ) = A (λ + ρ)$ in $R$ (The BGG Euler identity gives the Weyl numerator).

[F2]

$A (ρ) = e^{ρ} \prod_{α \in Φ^{+}} (1 - e^{- α})$ and $A (ρ)^{- 1} = e^{- ρ} \prod_{α \in Φ^{+}} (1 - e^{- α})^{- 1}$ , the product $\prod_{α \in Φ^{+}} (1 - e^{- α})$ being invertible in $R$ (The Weyl denominator identity, Geometric series are invertible in the completed character ring).

[F3]

$R$ is a commutative ring, so multiplication by the invertible element $A (ρ)^{- 1}$ is well defined, and $A (λ + ρ) = \sum_{w \in W} (- 1)^{ℓ (w)} e^{w (λ + ρ)}$ (The completed formal character ring, The Weyl alternation operator).

[F4]

$ch L (λ)$ is an element of $R$ , namely the finite sum $\sum_{μ} m_{λ} (μ) e^{μ}$ (The formal character of a finite-dimensional weight module).

Proof

technique · direct

1.1F1F2F3F4algebraA1

By [F1] and [F2] the element $A (ρ)$ is invertible in $R$ and $ch L (λ) A (ρ) = A (λ + ρ)$ ; multiplying this identity on the right by $A (ρ)^{- 1}$ and using associativity and commutativity of the product in the ring $R$ of [F3] gives first $A (ρ) A (ρ)^{- 1} = e^{0}$ and then $ch L (λ) = ch L (λ) A (ρ) A (ρ)^{- 1} = A (λ + ρ) A (ρ)^{- 1}$ .

2.1F2F3step 1.1∎

Substituting into step 1.1 the explicit finite sum of [F3] for the numerator and the product form and inverse of [F2] for the denominator gives the displayed quotient in $R$ ; the quotient is by definition the product of the finite alternant $A (λ + ρ)$ with the element $A (ρ)^{- 1} = e^{- ρ} \prod (1 - e^{- α})^{- 1}$ of $R$ , so it is a formal quotient in the completed ring and no quotient of ordinary functions is involved.

Depends on

Used by

Dependency tree · two levels

28 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)
A. W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)
A. Moreau, Representation Theory of Lie Algebras (M2, Université Paris-Saclay, 2025--2026) (standard reference, not scraped)
B. Weber, Weyl Character Formula II: Formulas of Weyl and Kostant (Penn Math 651, March 2013) (standard reference, not scraped)