ExampleConstruction: Literature-sourcedVerification: 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.

Affine sl2 mode brackets

Example

For ${s l}_{2}$ , take $e = (\begin{matrix} 0 & 1 \\ 0 & 0 \end{matrix})$ , $f = (\begin{matrix} 0 & 0 \\ 1 & 0 \end{matrix})$ , $h = diag (1, - 1)$ , and $B (x, y) = tr (x y)$ . For every $m, n \in Z$ , $[e_{m}, f_{n}] = h_{m + n} + m δ_{m, - n} c, [h_{m}, h_{n}] = 2 m δ_{m, - n} c, [d, e_{m}] = m e_{m} .$

Facts & Assumptions

Given: The displayed matrices and integer modes.

[F1]

The central-extension bracket is Untwisted affine central extension.

[F2]

The degree bracket is Degree derivation and full untwisted affine algebra.

Verification

1.1

Multiplication gives $e f = diag (1, 0)$ , $f e = diag (0, 1)$ , so $[e, f] = h$ and $B (e, f) = 1$ ; also $h^{2} = I$ , so $B (h, h) = 2$ and $[h, h] = 0$ . Trace cyclicity makes $B$ invariant; its Gram matrix on $e, f, h$ has determinant $- 2$ , so is nondegenerate. Thus F1 yields the first two displayed brackets. In particular $[e_{1}, f_{- 1}] = h_{0} + c$ , $[h_{1}, h_{- 1}] = 2 c$ , while $[e_{0}, f_{n}] = h_{n}$ and $[h_{0}, h_{n}] = 0$ .

F1givenalgebra

2.1

F2 gives $[d, e_{m}] = m e_{m}$ , including $[d, e_{0}] = 0$ and $[d, e_{- 1}] = - e_{- 1}$ . If $m + n \neq 0$ , both central terms in step 1.1 vanish; if $m + n = 0$ , their coefficients are exactly $m$ and $2 m$ . Hence all integer signs, zero modes and the opposite-mode boundary obey the displayed formulas. No choices are needed.

F2step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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, Sections 7.1-7.2 (standard reference, not scraped)
Perrin, Introduction to Kac-Moody Groups and Lie Algebras, Definition 12.2.3 (standard reference, not scraped)