LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 Heisenberg bracket satisfies the Lie algebra axioms

Statement

For every field $k$ and integer $n \geq 1$ , the vector space and bracket specified in Finite-dimensional Heisenberg Lie algebra form a Lie algebra over $k$ .

Facts & Assumptions

Given: A field $k$ , an integer $n \geq 1$ , and the vector space $h_{n} (k)$ with the bracket in Finite-dimensional Heisenberg Lie algebra.

[F1]

Finite-dimensional Heisenberg Lie algebra: the bracket is bilinear, every bracket is a scalar multiple of $Z$ , and $[Z, v] = 0$ for every $v \in h_{n} (k)$ .

[F2]

Lie algebras over a field: a Lie bracket is bilinear and alternating and satisfies the Jacobi identity.

Proof

1.1F1F2algebra

Bilinearity is part of the bracket construction in [F1]. For $v = \sum_{i} (a_{i} X_{i} + b_{i} P_{i}) + c Z$ , its self-bracket is $[v, v] = \sum_{i} (b_{i} a_{i} - a_{i} b_{i}) Z = 0$ , since multiplication in $k$ is commutative. Thus the bracket is alternating in every characteristic, including characteristic $2$ .

2.1F1F2step 1.1algebra∎

By [F1], each bracket lies in $k Z$ and $Z$ brackets to zero with all of $h_{n} (k)$ . Every nested bracket is therefore zero, so each term in the Jacobi sum vanishes. Together with step 1.1, the axioms in [F2] hold.

Depends on

Used by

Cited to discharge well-definedness by Finite-dimensional Heisenberg Lie algebra.

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

François Dumas, Noncommutative Invariants, §3.2.1 (standard reference, not scraped)