ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

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.

Lowest K-types of the first holomorphic discrete series

Statement

Assume the Axiom of Choice (The Axiom of Choice). In the holomorphic model $D_{2}^{-} = (π_{2}, H_{2}^{+})$ of Holomorphic and antiholomorphic discrete-series models, put $f_{2, j} (z) = (z - i)^{j} (z + i)^{- 2 - j}$ . The extremal vector $f_{2, 0} (z) = (z + i)^{- 2}$ has norm squared $π / 4$ , so $(2 / \sqrt{π}) f_{2, 0}$ has unit norm; it is annihilated by $L_{E_{+}}$ and has K-character $e^{- 2 i θ}$ . The vectors $f_{2, j}$ , $j \geq 0$ , form the complete multiplicity-one K-type chain with characters $e^{- i (2 + 2 j) θ}$ ; their ladder coefficients are $L_{E_{+}} f_{2, 0} = 0$ , $L_{E_{+}} f_{2, j} = - j f_{2, j - 1}$ for $j \geq 1$ , and $L_{E_{-}} f_{2, j} = (2 + j) f_{2, j + 1}$ for $j \geq 0$ .

Facts & Assumptions

Given: AC and the weighted holomorphic discrete-series model at $n = 2$ .

[F1]

In the model, $f_{n, j} (z) = (z - i)^{j} (z + i)^{- n - j}$ and $π_{n} (k_{θ}) f_{n, j} = e^{- i (n + 2 j) θ} f_{n, j}$ ; the derived actions are $L_{E_{+}} f_{n, 0} = 0$ , $L_{E_{+}} f_{n, j} = - j f_{n, j - 1}$ for $j \geq 1$ , and $L_{E_{-}} f_{n, j} = (n + j) f_{n, j + 1}$ for $j \geq 0$ (Holomorphic and antiholomorphic discrete-series models, Smooth and K-finite vectors for SL2(R), and the (g,K)-module).

[F2]

The weighted holomorphic space is a Hilbert space whose displayed vectors are a complete orthogonal K-type basis (The weighted discrete-series space is a Hilbert space with K-type basis).

[F3]

$D_{n}^{-}$ is an irreducible strongly continuous unitary representation for every $n \geq 2$ (Irreducibility and K-types of the discrete series).

[F4]

Tonelli's theorem interchanges the iterated integrals of a nonnegative measurable function on the product of the two sigma-finite Lebesgue spaces (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[A1]

AC is inherited through the model, Hilbert-space, and representation suppliers (The Axiom of Choice).

Proof

technique · direct

Given: The definitions and hypotheses in the Statement.

1.1F1F4algebraA1

Since $y^{2 - 2} = 1$ and $∣ z + i ∣^{2} = x^{2} + (y + 1)^{2}$ for $z = x + i y$ , [F4] gives $∥ f_{2, 0} ∥_{2}^{2} = \int_{0}^{\infty} \int_{- \infty}^{\infty} (x^{2} + (y + 1)^{2})^{- 2} d x d y$ . For $a > 0$ , the substitution $x = a \tan t$ yields $\int_{- \infty}^{\infty} (x^{2} + a^{2})^{- 2} d x = a^{- 3} \int_{- π / 2}^{π / 2} \cos^{2} t d t = π / (2 a^{3})$ . Taking $a = y + 1$ therefore gives $∥ f_{2, 0} ∥_{2}^{2} = (π / 2) \int_{0}^{\infty} (y + 1)^{- 3} d y = π / 4$ , and $∥ (2 / \sqrt{π}) f_{2, 0} ∥_{2} = 1$ .

2.1F1F2F3algebra∎

Setting $n = 2$ in [F1] gives $f_{2, j} (z) = (z - i)^{j} (z + i)^{- 2 - j}$ , K-character $e^{- i (2 + 2 j) θ}$ , and $L_{E_{+}} f_{2, 0} = 0$ , $L_{E_{+}} f_{2, j} = - j f_{2, j - 1}$ for $j \geq 1$ , and $L_{E_{-}} f_{2, j} = (2 + j) f_{2, j + 1}$ for $j \geq 0$ . Thus every step from $f_{2, j}$ to $f_{2, j + 1}$ and every return step for $j > 0$ has nonzero coefficient. By [F2], these lines give the full multiplicity-one K-type decomposition of $D_{2}^{-}$ , and [F3] gives its irreducibility.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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

Emmanuel Kowalski, An Introduction to the Representation Theory of Groups (AMS GSM 155; author's PDF) (standard reference, not scraped)
Matt Kerr, Notes on the Representation Theory of SL2(R) (NSF/CBMS workshop writeup) (standard reference, not scraped)