ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedverified 2026-09-23 (gpt-6-sol)

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.

Reducible and generic sl2 Verma modules

Example

$M (λ)$ for ${s l}_{2}$ is reducible exactly when $λ = m \in Z_{\geq 0}$ ; then $f^{m + 1} v_{m}$ is a singular vector. When $λ \notin Z_{\geq 0}$ it is simple.

Facts & Assumptions

Given: The ${s l}_{2}$ relations $[h, f] = - 2 f$ and $[e, f] = h$ , the highest vector $v_{λ}$ with $e v_{λ} = 0$ and $h v_{λ} = λ v_{λ}$ (Verma modules), and the PBW basis $w_{n} = f^{n} v_{λ}$ for $n \geq 0$ (The PBW model of a Verma module).

Verification

technique · direct

1.1givenalgebra

The commutator $[h, f] = - 2 f$ gives $h w_{n} = (λ - 2 n) w_{n}$ by induction. Similarly $[e, f] = h$ gives $e w_{n + 1} = f e w_{n} + h w_{n}$ . Starting with $e w_{0} = 0$ , induction yields $e w_{n} = n (λ - n + 1) w_{n - 1}$ for $n \geq 1$ . PBW makes every $w_{n}$ nonzero, and their $h$ -eigenvalues are pairwise distinct.

2.1step 1.1algebra

If $λ = m \in Z_{\geq 0}$ , step 1.1 gives $e w_{m + 1} = 0$ . The tail $W = span {w_{n} : n \geq m + 1}$ is invariant under $f$ and $h$ , and under $e$ because $e w_{m + 1} = 0$ and $e w_{n}$ is a scalar multiple of $w_{n - 1}$ for larger $n$ . It is nonzero and proper by PBW, so $M (m)$ is reducible and $w_{m + 1} = f^{m + 1} v_{m}$ is singular.

3.1step 1.1step 2.1algebra∎

Conversely, suppose $λ \notin Z_{\geq 0}$ and let $N$ be a nonzero submodule. A nonzero vector of $N$ is a finite sum of basis vectors $w_{n}$ . Since their $h$ -eigenvalues are distinct, a finite Lagrange interpolation polynomial in $h$ extracts one nonzero $w_{n} \in N$ . Each coefficient $k (λ - k + 1)$ for $1 \leq k \leq n$ is nonzero, so applying $e^{n}$ gives a nonzero multiple of $w_{0} \in N$ . Applying powers of $f$ then gives every $w_{j} \in N$ . Thus $N = M (λ)$ and $M (λ)$ is simple. Together with step 2.1 this proves the asserted classification without a determinant criterion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Mrudul Thatte, Category O: Verma's Thesis, Example 4.3 (standard reference, not scraped)