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 affine A1 simple roots and GCM
Example
For finite with root and coroot , the affine simple roots and coroots are , , , . Their Cartan matrix is
Facts & Assumptions
Given: The rank-one root convention .
Highest-root affine data are The affine simple root alpha zero is delta minus the highest root.
The loop generators give the GCM realization by Loop and affine GCM presentations are isomorphic.
Verification
The finite roots are , so the highest root is . F1 gives the displayed data. Since , we compute , , , and . These are all four entries in the stated row-coroot, column-root convention.
By F2, and , with ; the finite generators lie in degree zero. The matrix has rank one since its second row is the negative of its first, and its null vector is . Accordingly and , both nonzero in the full realization. Thus the two off-diagonal double entries describe an affine, not finite rank-one, matrix. All data are explicit and choice-free.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
12 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 6.1 and 7.2 (standard reference, not scraped)
- Perrin, Introduction to Kac-Moody Groups and Lie Algebras, Proposition 12.2.13 (standard reference, not scraped)