Alphabeta MathHow 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.
Finite-dimensional simple complex Lie algebra
Definition
A finite-dimensional complex Lie algebra is simple if it is nonabelian and its only ideals are and . In the local convention of def-finite-semisimple-lie-algebra-and-symmetric-adjoint-action, a finite-dimensional Lie algebra is semisimple when it has no nonzero solvable ideal.
Definition references
Facts & Assumptions
Given: A finite-dimensional complex Lie algebra that is simple in the stated sense.
Finite semisimple Lie algebras and the symmetric adjoint action: a solvable Lie algebra has a derived series that terminates at zero; semisimple means having no nonzero solvable ideal.
Proof
Let be a solvable ideal of . Simplicity gives or . The second option is impossible: nonabelianness makes a nonzero ideal, hence equal to ; then every term of the derived series equals , contradicting solvability. Thus .
Since every solvable ideal is zero, is semisimple under [F1]. This implication uses finite-dimensionality and the stated complex Lie algebra convention.