ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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 A1 Nakajima correspondence in the fundamental sl2 representation

Example

For the one-vertex, no-arrow quiver with framing dimension one, the two nonempty Nakajima fibres are points at $v = 0$ and $v = 1$ . On their fundamental classes $e_{0}, e_{1}$ , the Hecke correspondence gives $E = (\begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array}), F = (\begin{array}{cc} 0 & 0 \\ 1 & 0 \end{array}), H = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}) .$

Facts & Assumptions

Given: The A1 quiver varieties and their point Hecke correspondence, with basis ordered $(e_{0}, e_{1})$ by dimension $v = 0, 1$ .

[F1]

The A1 Nakajima Hecke correspondence gives the fundamental sl2 action: $E e_{0} = 0$ , $E e_{1} = e_{0}$ , $F e_{0} = e_{1}$ , $F e_{1} = 0$ , $H e_{0} = e_{0}$ and $H e_{1} = - e_{1}$ .

Verification

1.1givenF1algebra

In the ordered basis $(e_{0}, e_{1})$ , the six actions in [F1] give the displayed matrices column by column.

2.1F1step 1.1algebra∎

Direct multiplication gives $E F = diag (1, 0)$ , $F E = diag (0, 1)$ , $H E - E H = 2 E$ and $H F - F H = - 2 F$ . Therefore $[E, F] = H$ , $[H, E] = 2 E$ and $[H, F] = - 2 F$ , the defining ${s l}_{2}$ brackets.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Hiraku Nakajima, Introduction to quiver varieties—for ring and representation theorists, §§4.2, 4.4–4.5 (standard reference, not scraped)