ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Low-rank Dynkin coincidences

Example

The low-rank coincidences among the classical types are $B_{1} = C_{1} = A_{1}, B_{2} = C_{2}, D_{2} = A_{1} ⊔ A_{1}, D_{3} = A_{3} .$

Facts & Assumptions

Given: The classical coordinate models.

[L1]

The set ${\pm α}$ in a Euclidean line is the root system $A_{1}$ (The root system A_1).

[L2]

The coordinate root systems $B_{2}$ and $C_{2}$ are isomorphic: an explicit orthogonal transformation followed by a uniform rescaling carries one root set to the other (Root systems of the classical complex Lie algebras).

[L3]

In the classical coordinate models, $D_{n} = {\pm e_{i} \pm e_{j} : 1 \leq i < j \leq n} .$ For $D_{3}$ , the roots $δ_{1} = e_{1} - e_{2}, δ_{2} = e_{2} - e_{3}, δ_{3} = e_{2} + e_{3}$ form a simple system (Classical root systems in coordinates).

Proof

technique · direct

1.1

Extending the coordinate notation to rank one gives $B_{1} = {\pm e_{1}}$ and $C_{1} = {\pm 2 e_{1}}$ . The linear maps $e_{1} \mapsto α$ and $2 e_{1} \mapsto α$ identify these systems with $A_{1}$ from [L1]. Thus $B_{1} = C_{1} = A_{1}$ up to root-system isomorphism.

L1algebra

1.2

The explicit similarity in [L2] identifies the eight roots of $B_{2}$ with those of $C_{2}$ and preserves every Cartan integer. Hence $B_{2} = C_{2}$ up to root-system isomorphism.

1.3

For $D_{2}$ , [L3] gives $D_{2} = {\pm (e_{1} + e_{2}), \pm (e_{1} - e_{2})}$ , the orthogonal disjoint union of two rank-one systems, so $D_{2} = A_{1} ⊔ A_{1}$ by [L1].

L1L3algebra

2.1

For the simple roots of $D_{3}$ in [L3], all squared lengths are $2$ , while $(δ_{1}, δ_{2}) = (δ_{1}, δ_{3}) = - 1$ and $(δ_{2}, δ_{3}) = 0$ . Their Dynkin graph therefore has the three-vertex path $δ_{2} - δ_{1} - δ_{3}$ , the $A_{3}$ diagram. Hence $D_{3} = A_{3}$ up to root-system isomorphism.

L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19-24 (standard reference, not scraped)
Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed., Chapter II (standard reference, not scraped)