LemmaStatement: 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.

PBW spanning by ordered monomials

Statement

Let $B$ be a supplied basis of $g$ equipped with a supplied total order. Then the monomials

$ι_{g} (b_{1}) \dots ι_{g} (b_{n}) (b_{1} \leq \dots \leq b_{n}),$

including the empty monomial $1$ , span $U (g)$ .

Facts & Assumptions

Given: A Lie algebra $g$ with a specified ordered basis $B$ .

[L1]

Every element of $U (g)$ is a finite linear combination of images of tensor words (PBW filtration on the enveloping algebra).

[L2]

In $U (g)$ one has $x y = y x + [x, y]$ for basis elements $x, y$ .

[L3]

Every bracket $[x, y] \in g$ has a finite expansion in $B$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

Proof

technique · strong well-founded induction on the pair (word length, inversion number), ordered lexicographically

1.1

Words of length zero or one are ordered, and every word with inversion number zero is weakly increasing. These are the base cases.

base

1.2

Assume every basis word with strictly smaller pair (length, inversion number) is a linear combination of ordered words.

ihassume-hyp

2.1

A nonordered finite word has an adjacent inversion $x y$ with $x > y$ . Replace it using [L2] by $y x + [x, y]$ . The swapped word has the same length and one fewer inversion, while after the finite basis expansion in [L3] every bracket term has length one less. Step 1.2 therefore rewrites every resulting term as a linear combination of ordered words.

step 1.2L2L3algebra

3.1

The lexicographic order on pairs of nonnegative integers is well-founded, so steps 1.1–2.1 prove that every basis word is in the ordered span. By [L1], that span is all of $U (g)$ ; for the empty basis it consists only of $1$ .

step 1.1step 2.1L1discharge-induction: step 1.1∎

Depends on

Used by

Poincaré–Birkhoff–Witt theorem Theorem

Dependency tree · two levels

20 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

Etingof, MIT 18.745 notes, §13.1, printed pp. 74–75 (standard reference, not scraped)
Kirillov, An Introduction to Lie Groups and Lie Algebras, Lemma 5.10, printed pp. 73–74 (standard reference, not scraped)