LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

K-type eigenvalues of A(nu): recurrence, closed form and nonvanishing

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $ε \in {0, 1}$ , let $ν \in C$ with $Re ν > 0$ , and let $c_{r} (ν)$ be the eigenvalue of $A (ν)$ on the $K$ -type $f_{r}$ for each $r \equiv ε (m o d 2)$ in The standard intertwining operator A(nu). Then, for every such $r$ , $(r + 1 + ν) c_{r + 2} (ν) = (r + 1 - ν) c_{r} (ν), c_{- r} (ν) = (- 1)^{r} c_{r} (ν) .$ When $r + 1 + ν \neq 0$ , the first identity is equivalently $c_{r + 2} (ν) = c_{r} (ν) \frac{r + 1 - ν}{r + 1 + ν};$ at a zero denominator the cross-multiplied identity is the meaning of the recurrence. The scalar eigenvalues have the closed form $c_{r} (ν) = (- i)^{r} \sqrt{π} Γ (ν / 2) Γ ((ν + 1) / 2) \frac{1}{Γ ((ν + r + 1) / 2)} \frac{1}{Γ ((ν - r + 1) / 2)},$ where reciprocal Gamma is understood as its entire continuation, so this formula is valid for $Re ν > 0$ and its right side gives the meromorphic continuation of each scalar eigenvalue. Define the two base scalars $b_{0} (ν) = \int_{R} (1 + u^{2})^{- (1 + ν) / 2} d u, b_{1} (ν) = \int_{R} (u - i) (1 + u^{2})^{- (2 + ν) / 2} d u .$ Then $b_{0} = \sqrt{π} Γ (ν / 2) / Γ ((ν + 1) / 2)$ and $b_{1} = - i \sqrt{π} Γ ((ν + 1) / 2) / Γ ((ν + 2) / 2)$ . For $ε = 0$ , $c_{0} = b_{0}$ is the base eigenvalue and $b_{1}$ is only a formal odd scalar; for $ε = 1$ , $c_{1} = b_{1}$ is the base eigenvalue and $b_{0}$ is only a formal even scalar.

For $m \in W_{ε}$ , $m \geq 1$ , the exceptional zero sets are exact: at $ν = m$ , $c_{r} (m) = 0$ exactly for allowed $r$ with $∣ r ∣ \geq m + 1$ ; at $ν = - m$ , $c_{r} (- m) = 0$ exactly for allowed $r$ with $∣ r ∣ \leq m - 1$ . In particular $c_{m - 1} (m) \neq 0$ and $c_{m + 1} (- m)$ is finite and nonzero.

Facts & Assumptions

Given: AC, $ε \in {0, 1}$ , $Re ν > 0$ , and the smooth compact-picture principal series.

[F1]

For $Re ν > 0$ , the defining integral for $A (ν)$ is absolutely convergent, smooth, covariant for $I_{ε, - ν}$ , right- $G$ intertwining, and diagonal on the allowed $K$ -types. These initial-half-plane claims are verified in steps 1.1–4.1 of The standard intertwining operator A(nu); this proof uses only those claims. The formal even scalar and its continuation needed when $ε = 1$ are established below. The separate meromorphic continuation of the full operator family in that Definition is not assumed here.

[F2]

The compact-picture action has $K$ -types $C f_{r}$ with $f_{r} (k_{θ}) = e^{i r θ}$ and $r \equiv ε (m o d 2)$ (The compact picture of the SL2(R) principal series, K-type decomposition of the SL2(R) principal series). The exceptional lattice is $W_{0} = 2 Z + 1$ and $W_{1} = 2 Z$ (The normalized principal series I(epsilon, nu)).

[F3]

The complex-linear derived action satisfies $L_{E_{\pm}} f_{r} = (1 + ν \pm r) f_{r \pm 2} / 2$ and preserves smooth vectors (Derived action and raising/lowering formulas in the compact picture).

[F4]

For $Re p, Re q > 0$ , the Beta and Gamma integrals satisfy $B (p, q) = Γ (p) Γ (q) / Γ (p + q)$ (Euler's Beta function on the right half-planes, Euler's Gamma function on the right half-plane, The Beta-Gamma identity), and $Γ (1 / 2) = \sqrt{π}$ (The value of Gamma at one half).

[F5]

Gamma has meromorphic continuation with simple poles of nonzero residue at the nonpositive integers, no zeros, and reciprocal Gamma is entire with simple zeros exactly there. Its functional equation holds meromorphically (Meromorphic continuation of Gamma, Gamma has no zeros).

[F6]

If $T : U \to V$ is a $C^{1}$ diffeomorphism of open Euclidean sets and $h \in L^{1} (V)$ , then $\int_{V} h = \int_{U} (h \circ T) ∣ \det D T ∣$ (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F7]

$L (R)$ is the Lebesgue sigma-algebra, and a real or complex function is in $L^{1}$ when it is measurable and its absolute value has finite integral (Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , Integrable real and complex functions, and their integrals).

[F8]

Measurable restrictions of nonnegative functions are measurable, dominated nonnegative functions are integrable when the majorant is, and the integral over a measurable set is the integral of the indicator restriction (Integral over a measurable subset, Closure properties of measurable functions used by the integral, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F9]

A nonnegative integrable function has integral zero over a null set, and every singleton in $R$ is null by the degenerate interval case (A nonnegative integral over a null set vanishes, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F10]

The Lebesgue integral is complex-linear on $L^{1}$ (The Lebesgue integral is linear on $L^{1} (μ)$ ).

[A1]

The item assumes full AC. It implies ${A C}_{ω}$ through The Axiom of Countable Choice ( ${A C}_{ω}$ ), which supplies the countable-choice hypothesis in [F6] and the singleton-null supplier in [F7]. The algebraic and reflection calculations make no further choices (The Axiom of Choice).

Proof

technique · evaluate the integral on each $K$-type, differentiate its intertwining identity, and determine all scalars from one base index in each parity

1.1F1F2F7algebra

Put $R (u) = \sqrt{1 + u^{2}}$ and $q_{r} (u) = (u - i)^{r} R (u)^{- 1 - ν - r}$ . At $g = I$ , the bottom row of $w n_{u}$ is $(1, u)$ , so the compact coordinate satisfies $e^{i θ_{u}} = (u - i) / R (u)$ . Thus the defining integral gives $c_{r} (ν) = \int_{R} q_{r} (u) d u$ . Also $b_{0} = \int_{R} q_{0}$ and $b_{1} = \int_{R} q_{1} (u) d u$ . For every integer $r$ , $∣ q_{r} (u) ∣ = R (u)^{- 1 - Re ν}$ ; this equals the absolute value of the defining integrand for any allowed mode, so it is integrable by [F1]. It also shows both formal base integrands are integrable when their parity is not allowed.

1.2F1F2F3algebra

Differentiate the right- $G$ intertwining identity in [F1] along real Lie-algebra directions and extend complex-linearly as in [F3]. Applying $A (ν) L_{E_{+}}^{ν} = L_{E_{+}}^{- ν} A (ν)$ to $f_{r}$ gives $(r + 1 + ν) c_{r + 2} (ν) = (r + 1 - ν) c_{r} (ν)$ . This cross-multiplied identity holds even when $r + 1 + ν = 0$ ; division gives the ratio form only when that denominator is nonzero.

1.3F1F4F6F7F8F9F10A1algebra

The even function $q_{0}$ is in $L^{1} (R)$ . For measurable $E$ , write $\int_{E} q_{0} = \int_{R} q_{0} χ_{E}$ ; split real and imaginary parts into positive and negative parts, use [F8] for measurability of their restrictions, and use $∣ q_{0} χ_{E} ∣ \leq ∣ q_{0} ∣$ and [F7, F8] for integrability. The singleton ${0}$ is null by the degenerate interval case of [F9]; its complex integral is zero by applying the nonnegative null-integral result in [F9] to the four restricted parts and recombining by [F10]. The three indicators of $(- \infty, 0)$ , ${0}$ , and $(0, \infty)$ sum to $1$ , so [F10] splits the full integral into these subset integrals. Reflection $u \mapsto - u$ in [F6] equates the two open half-line integrals, giving $b_{0} = 2 \int_{0}^{\infty} q_{0} (u) d u$ . The inverse change of variables for $t = u^{2} / (1 + u^{2})$ is $u = \sqrt{t / (1 - t)}$ with derivative $1 / (2 \sqrt{t} (1 - t)^{3 / 2})$ . Applying [F6] to this inverse diffeomorphism and the $L^{1}$ function $q_{0}$ gives $b_{0} = B (1 / 2, ν / 2)$ ; these Beta parameters have positive real parts because $Re ν > 0$ . By [F4], this equals $\sqrt{π} Γ (ν / 2) / Γ ((ν + 1) / 2)$ .

2.1F1F4F6F7F8F9F10step 1.1step 1.3algebra

Put $h_{1} (u) = (1 + u^{2})^{- 1 - ν / 2}$ . Both $h_{1}$ and $u h_{1}$ are in $L^{1}$ : pointwise $∣ h_{1} (u) ∣ \leq ∣ (u - i) h_{1} (u) ∣$ and $∣ u h_{1} (u) ∣ \leq ∣ (u - i) h_{1} (u) ∣$ , and the latter is the absolutely integrable formal base integrand by step 1.1. Reflection in [F6] sends $u h_{1} (u)$ to its negative, so its full integral is zero. The same indicator splitting, reflection and null-singleton argument as in step 1.3 give $\int_{R} h_{1} = 2 \int_{0}^{\infty} h_{1}$ . The inverse substitution from step 1.3 now gives $\int_{R} h_{1} = B (1 / 2, (ν + 1) / 2)$ ; these Beta parameters have positive real parts because $Re ν > 0$ . By linearity and [F4], $b_{1} = \int_{R} (u - i) h_{1} (u) d u = - i \sqrt{π} Γ ((ν + 1) / 2) / Γ ((ν + 2) / 2)$ . Thus $c_{0} = b_{0}$ when $ε = 0$ and $c_{1} = b_{1}$ when $ε = 1$ ; the other scalar is only a formal base integral.

2.2F6step 1.1algebra

The density formula gives $q_{- r} (u) = (- 1)^{r} q_{r} (- u)$ for every integer $r$ . Since both sides are integrable by step 1.1, the $C^{1}$ reflection $u \mapsto - u$ in [F6] yields $c_{- r} (ν) = (- 1)^{r} c_{r} (ν)$ directly, with no division by a recurrence coefficient.

3.1F4F5step 1.2step 1.3step 2.1step 2.2

Define ${\tilde{c}}_{r} (ν)$ by the Gamma formula in the Statement and set $x = (ν + r + 1) / 2$ , $y = (ν - r + 1) / 2$ . The Gamma functional equation gives ${\tilde{c}}_{r + 2} = - (y - 1) x^{- 1} {\tilde{c}}_{r} = \frac{r + 1 - ν}{r + 1 + ν} {\tilde{c}}_{r}$ wherever this ratio is defined, so $(r + 1 + ν) {\tilde{c}}_{r + 2} = (r + 1 - ν) {\tilde{c}}_{r}$ holds meromorphically, including at zero denominators. Swapping the denominator factors and using $(- i)^{- 2 r} = (- 1)^{r}$ gives ${\tilde{c}}_{- r} = (- 1)^{r} {\tilde{c}}_{r}$ . The substitutions in steps 1.3 and 2.1 give ${\tilde{c}}_{0} = b_{0} = c_{0}$ for even parity and ${\tilde{c}}_{1} = b_{1} = c_{1}$ for odd parity. For $r \geq 0$ , $r + 1 + ν \neq 0$ on $Re ν > 0$ , so the recurrence determines every nonnegative allowed index from that base; step 2.2 determines the negative indices. Hence $c_{r} = {\tilde{c}}_{r}$ on the initial half-plane, and the Gamma expression supplies the meromorphic continuation of each scalar without asserting convergence of the original integral outside that half-plane. At $ν = 0$ , for even $r$ the denominator arguments are half-integers, so the numerator pole remains; for odd $r$ , exactly one denominator argument is a nonpositive integer, whose reciprocal zero cancels the numerator pole and leaves a finite nonzero value.

4.1F5step 3.1algebra∎

Let $m \in W_{ε}$ be positive. Then $m$ and every allowed $r$ have opposite parity, so all four denominator arguments at $ν = \pm m$ are integers. At $ν = m$ , both arguments are positive for $∣ r ∣ \leq m - 1$ , making the Gamma quotient finite and nonzero; for $∣ r ∣ \geq m + 1$ , exactly one argument is nonpositive, so its reciprocal-Gamma factor vanishes and the numerator is finite. At $ν = - m$ , exactly one numerator Gamma factor has a simple pole and the other is finite and nonzero. If $∣ r ∣ \leq m - 1$ , both denominator arguments are nonpositive integers, so their two simple reciprocal-Gamma zeros leave a zero after multiplication by the single numerator pole. If $∣ r ∣ \geq m + 1$ , exactly one denominator argument is a nonpositive integer and the other is positive; its simple reciprocal-Gamma zero cancels the numerator pole and leaves a finite nonzero value. In particular, the denominator arguments at $r = m - 1, ν = m$ are $m, 1$ , and at $r = m + 1, ν = - m$ they are $1, - m$ , proving the two stated boundary values. These cases prove both directions of the exact zero-set assertions.

Remarks

Kerr's formulas (2.5)–(2.6) use the same compact-picture ladder normalization and give the same derived-action coefficients. His Exercise 2.8 asks for the intertwiner properties and K-type computation without supplying a solution; the integral eigenvalues and their continuation are derived above. Kerr's Weyl matrix is $- w$ relative to the $w$ fixed in The standard intertwining operator A(nu), so its integral eigenvalues differ by $(- 1)^{ε}$ in parity $ε$ .

Etingof's §9.1 formulas (4)–(5) use an abstractly normalized $({s l}_{2}, K)$ basis, and §9.2 uses a right- $P$ -covariant model with left $G$ -action. In that model $F (g b) = ∣ t (b) ∣^{s - 1} σ_{ε} (t (b)) F (g)$ , while inversion of the present left- $P$ model gives exponent $- 1 - ν$ and hence $s = - ν$ . This is a convention and ladder check; it does not supply the integral eigenvalue constants proved here.

Depends on

Used by

Cited to discharge well-definedness by The standard intertwining operator A(nu).

Dependency tree · two levels

115 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)