LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 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.

Derived action and raising/lowering formulas in the compact picture

Statement

Assume the Axiom of Choice (The Axiom of Choice). Use the compact-picture conventions of Iwasawa and minimal-parabolic data for SL2(R) and K-type decomposition of the SL2(R) principal series: $k_{θ} = (\begin{array}{cc} \cos θ & \sin θ \\ - \sin θ & \cos θ \end{array})$ and $f_{n} (k_{θ}) = e^{i n θ}$ . Put $J = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array}), H = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}), S = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), W = - i J, E_{+} = \frac{1}{2} (H + i S), E_{-} = \frac{1}{2} (H - i S) .$ Thus $J, H, S$ are real Lie-algebra elements, $k_{θ} = \exp (θ J)$ , and $W, E_{+}, E_{-}$ are the explicitly normalized basis of ${s l}_{2} (C)$ with $[W, E_{\pm}] = \pm 2 E_{\pm}$ and $[E_{+}, E_{-}] = W$ . For a smooth compact-picture vector define $L_{X} f = \frac{d}{d t} ∣_{t = 0} Π_{ν} (\exp (t X)) f (X \in {s l}_{2} (R)),$ and extend this map complex-linearly to ${s l}_{2} (C)$ ; in particular $L_{W} = - i L_{J}$ and $L_{E_{\pm}} = (L_{H} \pm i L_{S}) / 2$ . No action of the real group on $\exp (t X)$ for nonreal $X$ is asserted.

These operators preserve smooth vectors and the $K$ -finite vectors of $I_{ε, ν}$ , satisfy $[L_{W}, L_{E_{\pm}}] = \pm 2 L_{E_{\pm}}, [L_{E_{+}}, L_{E_{-}}] = L_{W},$ and act on the $K$ -type basis by $L_{W} f_{n} = n f_{n}, L_{E_{\pm}} f_{n} = \frac{1 + ν \pm n}{2} f_{n \pm 2} .$ Consequently $L_{E_{-}} f_{n} = 0$ exactly when $ν = n - 1$ , and $L_{E_{+}} f_{n} = 0$ exactly when $ν = - (n + 1)$ .

Facts & Assumptions

Given: AC, $ε \in {0, 1}$ , $ν \in C$ , and a smooth vector in the compact picture of $I_{ε, ν}$ .

[F1]

Restriction to $K$ identifies the induced model with parity- $ε$ smooth functions and gives the cocycle action for right translation (The compact picture of the SL2(R) principal series).

[F2]

The Iwasawa theorem gives unique smooth KAN and NAK coordinates; the relation $a_{t} n_{x} = n_{e^{t} x} a_{t}$ converts the latter by a smooth coordinate change into unique smooth ANK coordinates (Iwasawa decomposition and Haar integration formula for SL2(R), Iwasawa and minimal-parabolic data for SL2(R)).

[F3]

The covariance factor in that action is $∣ α ∣^{1 + ν}$ , with the normalized half-modular character applied exactly once (The normalized principal series I(epsilon, nu)).

[F4]

The $K$ -finite vectors are the finite sums of $f_{n} (k_{θ}) = e^{i n θ}$ with $n \equiv ε (m o d 2)$ (K-type decomposition of the SL2(R) principal series).

[F5]

The bracket on the traceless matrix Lie algebra is the matrix commutator (The special linear Lie algebra sl_2); direct multiplication of the displayed matrices gives $[W, E_{\pm}] = \pm 2 E_{\pm}$ and $[E_{+}, E_{-}] = W$ .

[F6]

Real one-parameter subgroups are exponentials with initial velocity $X$ ; the real product and chain rules apply to the smooth matrix coordinates (One-parameter subgroup of a Lie group, One-parameter subgroups are exactly exponentials, Exponential map of a Lie group, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[F7]

For positive $r$ , the scalar factor $r^{1 + ν}$ means $\exp ((1 + ν) \log r)$ ; the complex exponential has derivative itself, so its derivative along a real smooth curve follows by applying the real chain rule to real and imaginary parts (The complex exponential is entire and its complex derivative is itself, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[F9]

The real logarithm is differentiable on $(0, \infty)$ with derivative $1 / r$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F8]

The circle matrices satisfy $k_{θ} k_{ϕ} = k_{θ + ϕ}$ , and $\frac{d}{d θ} k_{θ} ∣_{θ = 0} = J$ , by the sine/cosine addition and derivative formulas (The addition formulas for sine and cosine, The derivatives of sine and cosine are cosine and minus sine).

[A1]

AC supplies the normalized Haar inputs of the compact-picture and K-type suppliers; it implies AC $_{ω}$ for the Fourier and one-parameter-subgroup/exponential suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ )). No vector is selected when defining $L_{X}$ (The Axiom of Choice, Iwasawa and minimal-parabolic data for SL2(R)).

Proof

technique · differentiate the actual right-translation cocycle along real matrix directions

1.1F1F2F6F8A1algebra

By [F8], $θ \mapsto k_{θ}$ is a one-parameter subgroup with initial velocity $J$ ; uniqueness in [F6] gives $k_{θ} = \exp (θ J)$ . Fix $θ$ and $X \in {J, H, S}$ , and write $k_{θ} \exp (t X) = a_{u (t)} n_{x (t)} k_{ϕ (t)}$ in the unique smooth $A N K$ coordinates near $t = 0$ , with $u (0) = x (0) = 0$ and $ϕ (0) = θ$ . If the bottom row is $v (t)$ , then $v (t) = e^{- u (t) / 2} (- \sin ϕ (t), \cos ϕ (t))$ , so $∣ α ∣ = ∥ v ∥^{- 1}$ , $(\log ∣ α ∣)^{'} = - v \cdot v^{'} / ∥ v ∥^{2}$ , and $ϕ^{'} = \det (v, v^{'}) / ∥ v ∥^{2}$ . By [F6], $\frac{d}{d t} \exp (t X) ∣_{t = 0} = X$ , hence $v (0) = (- \sin θ, \cos θ)$ and $v^{'} (0) = (- \sin θ, \cos θ) X$ . For $X = H$ , this gives $v \cdot v^{'} = - \cos 2 θ$ and $\det (v, v^{'}) = \sin 2 θ$ ; for $X = S$ , it gives $v \cdot v^{'} = - \sin 2 θ$ and $\det (v, v^{'}) = - \cos 2 θ$ ; for $X = J$ , it gives $v \cdot v^{'} = 0$ and $\det (v, v^{'}) = 1$ . Thus the pairs $((\log ∣ α ∣)^{'}, ϕ^{'})$ for $J, H, S$ are respectively $(0, 1)$ , $(\cos 2 θ, \sin 2 θ)$ , and $(\sin 2 θ, - \cos 2 θ)$ . The positive diagonal fixes the local $M$ factor as $I$ .

2.1F1F3F6F7F9step 1.1

Differentiating the compact-picture factor $∣ α ∣^{1 + ν} f (k_{ϕ})$ using step 1.1 gives $L_{J} = \partial_{θ}$ , $L_{H} = (1 + ν) \cos 2 θ + \sin 2 θ \partial_{θ}$ , and $L_{S} = (1 + ν) \sin 2 θ - \cos 2 θ \partial_{θ}$ . Indeed, [F7] and [F9] give $\frac{d}{d t} ∣ α ∣^{1 + ν} = (1 + ν) ∣ α ∣^{1 + ν} (\log ∣ α ∣)^{'}$ ; at $t = 0$ the factor is $1$ . The compact-coordinate derivative contributes $ϕ^{'} (0) \partial_{θ}$ .

3.1F4step 2.1algebra

Complex-linear extension gives $L_{W} = - i D$ and $L_{E_{\pm}} = \frac{1}{2} e^{\pm 2 i θ} ((1 + ν) \mp i D)$ , where $D = \partial_{θ}$ . Applying these to $f_{n} = e^{i n θ}$ yields $L_{W} f_{n} = n f_{n}$ and $L_{E_{\pm}} f_{n} = \frac{1 + ν \pm n}{2} f_{n \pm 2}$ ; the coefficients preserve the parity lattice and shift each Fourier mode by one allowed $K$ -type.

4.1F4F5step 3.1algebra∎

The displayed operators are differential operators with smooth periodic coefficients, so they preserve smooth vectors, and step 3.1 shows they preserve finite Fourier sums. Using $[D, e^{\pm 2 i θ}] = \pm 2 i e^{\pm 2 i θ}$ gives $[L_{W}, L_{E_{\pm}}] = \pm 2 L_{E_{\pm}}$ . Writing $a = 1 + ν$ and $P_{\pm} = L_{E_{\pm}}$ , the product rule gives $P_{+} P_{-} = \frac{1}{4} ((a - 2 - i D) (a + i D)) = \frac{1}{4} (a (a - 2) + D^{2} - 2 i D)$ and $P_{-} P_{+} = \frac{1}{4} ((a - 2 + i D) (a - i D)) = \frac{1}{4} (a (a - 2) + D^{2} + 2 i D)$ , hence $[L_{E_{+}}, L_{E_{-}}] = - i D = L_{W}$ on every smooth vector. Finally, the coefficient of $f_{n - 2}$ in $L_{E_{-}} f_{n}$ vanishes iff $1 + ν - n = 0$ , i.e. $ν = n - 1$ , and the coefficient of $f_{n + 2}$ in $L_{E_{+}} f_{n}$ vanishes iff $1 + ν + n = 0$ , i.e. $ν = - (n + 1)$ .

Remarks

Kerr's formulas (2.5)–(2.6) use the same matrices $W, E_{\pm}$ and parameter normalization as this item, so the ladder coefficients and vanishing loci match directly. Kerr leaves the coordinate derivation as an exercise; this item supplies it from the bottom row of $k_{θ} \exp (t X)$ . Kowalski's Lemma 7.4.9, printed pp. 298–299, computes one real derived direction and leaves the other two to the reader; the local calculation above verifies all three. Etingof's formulas (4)–(5) use abstract $e, f, h$ and a separately normalized weight basis on $P^{\pm} (s)$ . In the convention $h = W$ , $e = E_{+}$ , $f = E_{-}$ , the local ladder coefficients give $f e f_{n} = (ν^{2} - (n + 1)^{2}) f_{n} / 4$ , so $f e + (h + 1)^{2} / 4$ acts by $ν^{2} / 4$ . This matches Etingof's Casimir scalar $s^{2} / 4$ when $s = \pm ν$ ; it is a central-character check, not a coefficient-by-coefficient identification. The displayed formulas above are derived locally.

Depends on

Used by

Dependency tree · two levels

87 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

Matt Kerr, Notes on the Representation Theory of SL2(R) (CBMS workshop writeup) (standard reference, not scraped)
Pavel Etingof, Representations of Lie Groups (MIT 18.757 lecture notes, Fall 2023) (standard reference, not scraped)
Emmanuel Kowalski, An Introduction to the Representation Theory of Groups (AMS GSM 155; author's PDF) (standard reference, not scraped)