LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07

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 simple-root singular vector in a Verma module

Statement

Let $α_{i}$ be simple and put $m = ⟨ λ + ρ, α_{i}^{\lor} ⟩$ . If $m \in Z_{> 0}$ , then $f_{i}^{m} v_{λ}$ is a singular vector in $M (λ)$ of weight $s_{i} \cdot λ$ .

Facts & Assumptions

Given: The Verma convention Verma modules, the reflection and Weyl-vector conventions Root reflections and the Weyl group action and The Weyl vector rho for a chosen positive system, and the root ${s l}_{2}$ line Opposite root spaces bracket to the Killing-dual line.

[L1]

The PBW model identifies $M (λ)$ with $U (n^{-}) v_{λ}$ as a vector space (The PBW model of a Verma module).

Proof

technique · direct

1.1

Choose nonzero $e_{i} \in g_{α_{i}}$ and scale $f_{i} \in g_{- α_{i}}$ so that $[e_{i}, f_{i}] = α_{i}^{\lor}$ ; the cited opposite-root bracket line permits this normalization. The resulting ${s l}_{2}$ relations give, by induction, $e_{i} f_{i}^{r} v_{λ} = r (⟨ λ, α_{i}^{\lor} ⟩ - r + 1) f_{i}^{r - 1} v_{λ} .$ At $r = m = ⟨ λ, α_{i}^{\lor} ⟩ + 1$ this is zero, while [L1] shows $f_{i}^{m} v_{λ} \neq 0$ .

L1givenalgebra

2.1

For $j \neq i$ , $[e_{j}, f_{i}] = 0$ because $α_{j} - α_{i}$ is not a root; hence every $e_{j}$ also kills $f_{i}^{m} v_{λ}$ . Its weight is $λ - m α_{i} = s_{i} (λ + ρ) - ρ$ , so it is singular of the stated dot weight.

step 1.1algebra∎

Depends on

Used by

Simple-reflection embeddings of Verma modules Proposition

Dependency tree · two levels

14 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

Pavel Etingof, Representations of Lie Groups, Exercise 8.15(i) (standard reference, not scraped)