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 , the Lie algebra of strictly upper triangular matrices is nilpotent of class .
Facts & Assumptions
Given: A field , an integer , and the matrix units .
The lower central series satisfies (Lower central series and nilpotent Lie algebras).
Class means and for a nonzero nilpotent algebra (Nilpotency class of a Lie algebra).
Verification
For , let be the span of with ; thus and . The identity shows that : either product is zero, or its surviving matrix unit has superdiagonal distance equal to the sum of the two input distances.
Induction using [L1] and step 1.1 gives . Conversely, , and if and , then and ; induction puts , so . Hence for every .
In particular, , while . Equivalently, the explicit left-normed chain witnesses sharpness. Thus [L2] gives class . When , the chain has one entry and is abelian of class one; for , outside the stated range, has class zero. No choice is used.
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
- Milne, Lie Algebras, strictly upper triangular example (standard reference, not scraped)