TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Kac Moody denominator identity

Statement

For a finite symmetrizable generalized Cartan matrix, with Weyl vector $ρ$ , positive roots $Δ^{+}$ and root multiplicities $m_{α}$ , $e^{ρ} \prod_{α \in Δ^{+}} (1 - e^{- α})^{m_{α}} = \sum_{w \in W} (- 1)^{ℓ (w)} e^{w ρ} .$ Both sides are coefficientwise locally finite in the downward-cone completion.

Facts & Assumptions

Given: The stated symmetrizable root datum.

[F1]

The denominator quotient has only imaginary cone support constructs the locally finite alternant $A_{ρ}$ and quotient $C = D / A_{ρ}$ .

[F2]

Casimir norm excludes nonzero denominator corrections proves $C = 1$ .

Proof

1.1

By F1 the normalized alternant $a = e^{- ρ} A_{ρ}$ has constant coefficient one and an inverse, and the normalized product $p = e^{- ρ} D$ satisfies $p = a C$ . The product is coefficientwise defined.

F1algebra

2.1

F2 gives $C = 1$ , hence $p = a$ by step 1.1. Multiplying by the monomial $e^{ρ}$ gives exactly the asserted equality, with the original exponents $m_{α}$ on every factor. All products used are coefficientwise finite by F1.

F1F2step 1.1algebra∎

Depends on

Used by

Affine denominator separates real and imaginary root factors Proposition
Weyl Kac character formula Theorem

Dependency tree · two levels

13 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

Kleshchev, Theorem 10.2.1 at Lambda=0 (standard reference, not scraped)
Perrin, Theorem 11.2.1 at lambda=0 (standard reference, not scraped)