Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Strictly upper triangular matrices form a nilpotent Lie algebra

Example

For n2, the Lie algebra nn(k) of strictly upper triangular n×n matrices is nilpotent of class n1.

Facts & Assumptions

Given: A field k, an integer n2, and the matrix units Eij.

[L1]

The lower central series satisfies γr+1=[nn,γr] (Lower central series and nilpotent Lie algebras).

[L2]

Class c means γc0 and γc+1=0 for a nonzero nilpotent algebra (Nilpotency class of a Lie algebra).

Verification

technique · direct
1.1

For p1, let Fp be the span of Eij with jip; thus F1=nn and Fn=0. The identity EijEm=δjEim shows that [Fp,Fq]Fp+q: either product is zero, or its surviving matrix unit has superdiagonal distance equal to the sum of the two input distances.

givenalgebra
2.1

Induction using [L1] and step 1.1 gives γr(nn)Fr. Conversely, F1=γ1, and if r2 and EijFr, then jir and Eij=[Ei,i+1,Ei+1,j]; induction puts Ei+1,jFr1=γr1, so Eijγr. Hence γr(nn)=Fr for every r1.

L1step 1.1algebra
3.1

In particular, γn=Fn=0, while γn1=Fn1=kE1n0. Equivalently, the explicit left-normed chain [E12,E23,,En1,n]=E1n witnesses sharpness. Thus [L2] gives class n1. When n=2, the chain has one entry and n2=kE12 is abelian of class one; for n=1, outside the stated range, n1=0 has class zero. No choice is used.

L2step 2.1algebra

Depends on

Used by

Dependency tree · two levels

4 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