PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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 pairs only opposite root spaces

Statement

Let $B$ be the Killing form from The Killing form of a semisimple Lie algebra, and let $x \in g_{α}$ , $y \in g_{β}$ for the root-space decomposition of Root-space decomposition relative to a Cartan subalgebra. If $α + β \neq 0$ , then

$B (x, y) = 0.$

In particular, $B$ pairs nontrivially only opposite root spaces and restricts nondegenerately to $h$ .

Facts & Assumptions

Given: Roots $α, β$ of a Cartan subalgebra $h$ , vectors $x \in g_{α}$ , $y \in g_{β}$ , and the Killing form $B$ .

Proof

technique · direct

1.1

For any $h \in h$ , invariance from The Killing form is invariant and nondegenerate on a complex semisimple Lie algebra gives $0 = B ([h, x], y) + B (x, [h, y]) = (α (h) + β (h)) B (x, y)$ .

givenalgebra

2.1

If $α + β \neq 0$ , choose $h \in h$ with $(α + β) (h) \neq 0$ ; then step 1.1 forces $B (x, y) = 0$ . Also, for $h_{0} \in h$ , the same argument with $x = h_{0}$ and $y \in g_{α}$ shows $B (h_{0}, y) = 0$ , so $h$ is orthogonal to every nonzero root space.

step 1.1

3.1

If $h_{0} \in h$ is orthogonal to $h$ , then step 2.1 makes it orthogonal to every summand in Root-space decomposition relative to a Cartan subalgebra, hence to all of $g$ . Nondegeneracy from The Killing form is invariant and nondegenerate on a complex semisimple Lie algebra gives $h_{0} = 0$ , so the restriction of $B$ to $h$ is nondegenerate.

step 2.1∎

Depends on

Used by

The Killing-dual vector attached to a root Definition
Opposite root spaces bracket to the Killing-dual line Proposition
The quadratic Casimir eigenvalue on a highest-weight module is (λ,λ+2ρ) Proposition
The root set is a reduced crystallographic root system Theorem

Dependency tree · one level

3 results within one dependency step 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

Pavel Etingof, Lie Groups and Lie Algebras I (standard reference, not scraped)