Alphabeta Math
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.

The root sl_2 triple inside sl_n

Example

Assume AC (The Axiom of Choice). In sln(C) with the diagonal Cartan subalgebra h and the root α=εi−εj of Diagonal Cartan subalgebra and roots of sln (i≠j), the triple eα=Eij,fα=Eji,hα=Eii−Ejj satisfies [eα,fα]=hα, [hα,eα]=2eα and [hα,fα]=−2fα, so it is a root sl2 triple in the sense of The root sl2 triple; moreover the Killing-dual vector is Hα=12n(Eii−Ejj), consistently with hα=2Hα/α(Hα) (Killing-dual vector of a root, Coroot of a Lie-algebra root).

Facts & Assumptions

Given: AC; the algebra sln(C) with its diagonal Cartan subalgebra h and root α=εi−εj, i≠j, as in Diagonal Cartan subalgebra and roots of sln, the matrix units Eab, and the notions of Killing-dual vector and coroot from Killing-dual vector of a root and Coroot of a Lie-algebra root.

Verification

technique · direct
1.1givenalgebra

The Killing form of sln(C) is B(X,Y)=2ntr⁡(XY) on traceless matrices: on the basis of matrix units, ad⁡Eab(Ecd)=δbcEad−δdaEcb, and summing the diagonal contributions of ad⁡Eabad⁡Ecd over the basis gives 2nδadδbc−2δabδcd, which is 2ntr⁡(EabEcd) on traceless elements because the correction term vanishes there.

2.1givenstep 1.1algebra

With this form, B(12n(Eii−Ejj),H)=tr⁡((Eii−Ejj)H)=xi−xj=α(H) for H=diag⁡(x1,…,xn)∈h, so Hα=12n(Eii−Ejj). Since Hα is a multiple of the traceless diagonal matrix Eii−Ejj, we get α(Hα)=12nα(Eii−Ejj)=22n=1n, and therefore 2Hα/α(Hα)=2nHα=Eii−Ejj.

3.1givenstep 2.1algebra∎

The bracket relations are matrix multiplications: [Eij,Eji]=Eii−Ejj, [Eii−Ejj,Eij]=2Eij and [Eii−Ejj,Eji]=−2Eji. Hence the displayed triple satisfies exactly the relations of The special linear Lie algebra sl_2 with hα in the role of h, which is the claim of The root sl2 triple realized concretely.

Depends on

Used by

Dependency tree · two levels

27 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