LemmaStatement: Literature-sourcedProof: 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.

Restricted Sugawara quadratic mode sums are well defined

Statement

Let $g$ be a finite-dimensional complex simple Lie algebra as in Loop algebra of a simple Lie algebra, with the normalized nondegenerate invariant form $B$ from Residue two cocycle on a loop algebra. Let $ρ$ be a restricted affine-current module of level $k$ as in Restricted affine-current module. For any $B$ -dual bases $(x_{a})$ and $(x^{a})$ , define $Q_{m} = \frac{1}{2} \sum_{a} \sum_{r \in Z} : J_{x_{a}} (r) J_{x^{a}} (m - r) :,$ where $J_{x} (n) = ρ (x \otimes t^{n})$ and $: J_{x} (r) J_{y} (s) : = {\begin{cases} J_{x} (r) J_{y} (s), & r < 0, \\ J_{y} (s) J_{x} (r), & r \geq 0. \end{cases}$ Then each $Q_{m}$ is locally finite on every vector of the module and is independent of the chosen dual bases.

Facts & Assumptions

Given: A restricted affine-current module, a finite-dimensional simple Lie algebra, and the displayed normal-ordering convention.

[F1]

Restricted affine-current module: for every vector $v$ and current $x$ , all sufficiently large positive modes $J_{x} (n)$ annihilate $v$ .

[F2]

Loop algebra of a simple Lie algebra: $g$ is finite-dimensional.

[F3]

Casimir operator relative to an invariant form: $\sum_{a} x_{a} x^{a}$ is the Casimir element for any pair of $B$ -dual bases.

[F4]

The Casimir operator is basis-independent and intertwining: the inverse tensor $\sum_{a} x_{a} \otimes x^{a}$ is independent of the chosen dual bases.

[F5]

Residue two cocycle on a loop algebra: the normalized invariant form is nondegenerate.

Proof

1.1F1F2givenalgebra

Fix a vector $v$ . By [F1], each of the finitely many basis currents $x_{a}, x^{a}$ has a positive-mode cutoff on $v$ ; taking the maximum of these finitely many cutoffs gives one cutoff for all basis elements. For $r \geq 0$ , normal ordering puts $J_{x_{a}} (r)$ on the right, so the summand vanishes on $v$ for all sufficiently large $r$ . For $r < 0$ , the rightmost mode is $J_{x^{a}} (m - r)$ , whose index tends to $+ \infty$ as $r \to - \infty$ , so those summands also vanish on $v$ outside a finite range. Thus only finitely many $r$ contribute to $Q_{m} v$ .

2.1F3F4F5step 1.1algebra∎

For fixed $m, r$ , the map $x \otimes y \mapsto : J_{x} (r) J_{y} (m - r) :$ is bilinear, with its factor order fixed by the sign of $r$ . The dual bases in the statement exist by [F5]. Therefore [F4] makes the sum over $a$ equal for every pair of $B$ -dual bases, term by term in $r$ . By step 1.1, on each vector only finitely many $r$ contribute, so summing these equal operators proves that $Q_{m}$ is independent of the dual bases.

Depends on

Used by

Sugawara modes and their normal ordering Definition

Dependency tree · two levels

15 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

Antony Wassermann, Kac–Moody and Virasoro Algebras, Chapter III §6 (standard reference, not scraped)
David Ben-Zvi and Edward Frenkel, Geometric Realization of the Segal–Sugawara Construction, §§3.2–3.3 (standard reference, not scraped)