ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Rank one gcm recovers sl2

Example

For $A = (2)$ , the minimal Cartan is $C h$ with $α (h) = 2$ , and $g (A) ≅ {s l}_{2} (C)$ .

Facts & Assumptions

Given: A=(2) and D=(1).

[F1]

The Cartan and Serre relations give exactly the algebra. (Serre presentation of a kac moody algebra).

Verification

1.1

There are no distinct indices, so no Serre relations. The Cartan relations are $[h, e] = 2 e$ , $[h, f] = - 2 f$ , $[e, f] = h$ . Their right sides lie in the span of $e, h, f$ , which is closed under brackets and contains all generators; thus the algebra has dimension at most three.

F1given

2.1

In traceless $2 \times 2$ matrices put $E = E_{12}$ , $F = E_{21}$ and $H = E_{11} - E_{22}$ . Matrix multiplication gives $E F = E_{11}$ , $F E = E_{22}$ , $H E = E$ , $E H = - E$ , $H F = - F$ , and $F H = F$ . Thus $[E, F] = H$ , $[H, E] = 2 E$ and $[H, F] = - 2 F$ . These three matrices are independent and span every traceless matrix. The presentation map is onto this three-dimensional space and step 1.1 bounds its source dimension by three, so it is an isomorphism.

F1step 1.1∎

Sources

Source comparison: Kleshchev, Example 1.5.2, pp.20–21; explicit 2×2 computation.

Depends on

Serre presentation of a kac moody algebra

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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 — Example 1.5.2, pp.20–21; explicit 2×2 computation (standard reference, not scraped)