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

The loop residue form is alternating

Statement

For all $u, v \in L g$ , $ω (u, v) = - ω (v, u)$ and $ω (u, u) = 0$ .

Facts & Assumptions

Given: A loop algebra over $C$ and its residue form.

[F1]

Residue two cocycle on a loop algebra defines $ω (x \otimes f, y \otimes q) = B (x, y) Res (f^{'} q d t)$ with $B$ symmetric.

Proof

1.1

For any Laurent polynomial $a = \sum_{j} a_{j} t^{j}$ , the coefficient of $t^{- 1}$ in $a^{'} = \sum_{j} j a_{j} t^{j - 1}$ is $0 a_{0} = 0$ . Thus $Res (a^{'} d t) = 0$ , including constant and zero $a$ .

F1algebra

2.1

For pure tensors $u = x \otimes f$ , $v = y \otimes q$ , symmetry of $B$ and the product rule give $ω (u, v) + ω (v, u) = B (x, y) Res ((f q)^{'} d t) = 0$ .

F1step 1.1algebra

3.1

Expand arbitrary $u, v$ into their finite tensor sums and apply step 2.1 term by term. This proves skewness for all inputs, including empty sums. Setting $v = u$ gives $2 ω (u, u) = 0$ ; since the field is $C$ , division by $2$ gives alternatingness.

step 2.1givenalgebra∎

Depends on

Residue two cocycle on a loop algebra

Used by

Untwisted affine central extension Definition

Dependency tree · two levels

4 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, Lectures on Infinite Dimensional Lie Algebras, equations (7.1)-(7.2) (standard reference, not scraped)
Perrin, Introduction to Kac-Moody Groups and Lie Algebras, Lemma 12.2.5 (standard reference, not scraped)