Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)
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 Killing form is invariant and nondegenerate on a complex semisimple Lie algebra

Statement

Let g be a complex semisimple Lie algebra, and let B be its Killing form from The Killing form of a semisimple Lie algebra. Then

B([x,y],z)=B(x,[y,z])(x,y,z∈g),

and B is nondegenerate.

Facts & Assumptions

Given: A finite-dimensional complex semisimple Lie algebra g and its Killing form B.

[L1]

The finite Engel/trace argument proves that the Killing form of every finite-dimensional complex semisimple Lie algebra is invariant and nondegenerate (Engel, the trace criterion, and Killing nondegeneracy).

Proof

technique · direct
1.1givenalgebra

Using ad⁡[x,y]=[ad⁡x,ad⁡y] and cyclicity of trace, one gets B([x,y],z)=tr⁡([ad⁡x,ad⁡y]ad⁡z)=tr⁡(ad⁡x[ad⁡y,ad⁡z])=B(x,[y,z]).

1.2L1given

The nondegeneracy clause of [L1] applies to g. It proves that the radical {x∈g:B(x,g)=0} is zero by an explicit finite trace-solvability argument, rather than leaving Cartan's criterion as an unproved appeal.

2.1step 1.1step 1.2L1∎

Hence B is invariant and has zero radical, so it is nondegenerate.

Depends on

Used by

Dependency tree · two levels

6 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