Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass
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.

Root strings in type A2

Example

Assume AC (The Axiom of Choice). In sl3(C) with the diagonal Cartan subalgebra and the roots εi−εj of Diagonal Cartan subalgebra and roots of sln, take α=ε1−ε2 and β=ε2−ε3, so that hα=E11−E22 by The root sl2 triple inside sln. The α-string through β consists of β and β+α=ε1−ε3, that is, it has the form β−pα,…,β+qα with p=0 and q=1, and indeed p−q=−1=β(hα)=(ε2−ε3)(E11−E22), in agreement with The root-string property. The α-string through α is {−α,0,α}, so p=2, q=0, p−q=2, and α(hα)=2.

Facts & Assumptions

Given: AC; the algebra sl3(C) with the roots εi−εj of Diagonal Cartan subalgebra and roots of sln, the roots α=ε1−ε2, β=ε2−ε3, the coroot hα=E11−E22 from The root sl2 triple inside sln and Coroot of a Lie-algebra root, and the string description of The root-string property with the root set of Root and root space.

Verification

technique · direct
1.1givenalgebra

The roots of sl3(C) are the six functionals εi−εj, i≠j, so β, β+α=ε1−ε3, α and −α are roots while 2α=2ε1−2ε2 is not, by the reducedness statement that the only scalar multiples of a root that are roots are ± themselves.

1.2givenalgebra

The Cartan integer evaluates as β(hα)=(ε2−ε3)(E11−E22): the diagonal matrix E11−E22 has coordinate vector (1,−1,0), so ε2−ε3 gives (−1)−0=−1, matching p−q=0−1=−1.

2.1givenstep 1.1algebra

For the α-string through β: the indices k∈Z with β+kα a root or 0 are k=0,1; indeed β+α=ε1−ε3 is a root, while β−α=2ε2−ε1−ε3 and β+2α=2ε1−ε2−ε3 are not among the six roots and are nonzero. Hence p=0, q=1.

3.1givenstep 1.1algebra∎

For the α-string through β=α, the terms are β+kα=(k+1)α. They are roots or zero exactly for k∈{−2,−1,0}, giving the terms −α,0,α and hence p=2, q=0, and p−q=2. Also α(hα)=(ε1−ε2)(E11−E22)=1−(−1)=2, so the string identity p−q=β(hα) holds.

Remarks

The two rows below are index schematics, with each arrow adding α (increasing k by one). The upper row shows β+kα for k=0,1; the lower shows α+kα for k=−2,−1,0. Here α=(1,−1,0) and β=(0,1,−1) in the coordinate-functional notation of the example. The open circle marks the zero weight, not a root; it is included because the root-string convention uses g0=h. The verification above is independent of the figure.

p=0;q=1p¡q=¡1+®¯¯+®k=0k=1p=2;q=0p¡q=2+®+®¡®0®k=¡2k=¡1k=0

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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