PropositionStatement: Literature-sourcedProof: 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.

Trace forms are symmetric and invariant

Statement

For every finite-dimensional representation $ρ : g \to g l (V)$ , the trace form is bilinear and symmetric, and it is invariant in the sense that

$B_{ρ} ([z, x], y) + B_{ρ} (x, [z, y]) = 0.$

Consequently the Killing form has all three properties.

Facts & Assumptions

Given: A representation $ρ : g \to g l (V)$ with $V$ finite-dimensional and elements $x, y, z \in g$ .

[L1]

The trace form is $B_{ρ} (x, y) = tr (ρ (x) ρ (y))$ (Trace form of a representation).

[L2]

Finite-dimensional endomorphisms satisfy $tr (A B) = tr (B A)$ (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ ).

Proof

technique · direct trace calculation

1.1

Linearity of $ρ$ , composition, and trace makes $B_{ρ}$ bilinear. By [L2], $B_{ρ} (x, y) = tr (ρ (x) ρ (y)) = tr (ρ (y) ρ (x)) = B_{ρ} (y, x)$ , so it is symmetric.

L1L2algebra

1.2

Put $X = ρ (x)$ , $Y = ρ (y)$ , and $Z = ρ (z)$ . Since $ρ$ preserves brackets, the left side of the invariance identity is $tr ((Z X - X Z) Y) + tr (X (Z Y - Y Z))$ . After expansion, the middle terms cancel directly and [L2] gives $tr (Z X Y) = tr (X Y Z)$ , so the remaining terms cancel as well.

L1L2algebra

2.1

The Killing form is the trace form for $ρ = ad$ , so steps 1.1–1.2 apply verbatim. The zero representation and zero-dimensional space cause no exception: every displayed trace is then zero.

L1step 1.11.2∎

Depends on

Used by

Dependency tree · two levels

8 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

Kirillov, An Introduction to Lie Groups and Lie Algebras, Lemma 6.1 (standard reference, not scraped)