Rankin half-plane audit for the quadratic Siegel amplifier

This file independently carries the genuine high-convolution coefficients into the absolute-convergence half-plane. It proves summability and the exact factorization

L((ζ * χ)^(r+1), σ) = (ζ(σ) L(σ,χ))^(r+1),

then combines coefficient nonnegativity with the existing perfect-power lower bound. The resulting finite Rankin inequality and its elementary zeta-majorant form contain no analytic source premise.

They also expose the obstruction to closing Landau--Siegel by this route alone. At even exponent e = r+1, perfect-power support contributes only M / (M^e)^σ. Thus σ = 1 + 1/log X does not preserve the finite summatory lower M after Rankin weighting: it pays the full factor X^σ. The infinite perfect-power subseries improves this only to a constant when r is fixed, while division by the zeta pole still leaves an L(σ,χ) lower of order σ-1. A derivative/Pólya--Vinogradov transfer of size (σ-1) * polylog(q) can therefore swamp that lower. Consequently this file deliberately proves the exact Rankin output, not a false eventual q^{-η} endpoint; closure needs a stronger weighted lower or relative control not present in the standard direct Rankin estimate.

theorem DirichletCharacter.rankin_pow_succ_summable {q : ℕ} (χ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) (r : ℕ) : LSeriesSummable (fun (n : ℕ) => (χ.zetaMul ^ (r + 1)) n) s

theorem DirichletCharacter.rankin_pow_succ_factorization {q : ℕ} (χ : DirichletCharacter ℂ q) [NeZero q] {s : ℂ} (hs : 1 < s.re) (r : ℕ) : LSeries (fun (n : ℕ) => (χ.zetaMul ^ (r + 1)) n) s = (riemannZeta s * LFunction χ s) ^ (r + 1)

theorem DirichletCharacter.rankin_term_re_eq {q : ℕ} (χ : DirichletCharacter ℂ q) (r : ℕ) {σ : ℝ} {n : ℕ} (hn : n ≠ 0) : (LSeries.term (fun (k : ℕ) => (χ.zetaMul ^ (r + 1)) k) (↑σ) n).re = (χ.quadraticSiegelPowerCoefficient (r + 1) n).re / ↑n ^ σ

theorem DirichletCharacter.rankin_term_re_nonneg {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (r : ℕ) {σ : ℝ} (n : ℕ) : 0 ≤ (LSeries.term (fun (k : ℕ) => (χ.zetaMul ^ (r + 1)) k) (↑σ) n).re

theorem DirichletCharacter.rankin_perfectPower_lower {q : ℕ} (χ : DirichletCharacter ℂ q) [NeZero q] (hquad : χ ^ 2 = 1) (r : ℕ) {e M : ℕ} (hepos : 0 < e) (heven : ∃ (t : ℕ), e = 2 * t) (hM : 1 ≤ M) {σ : ℝ} (hσ : 1 < σ) : ↑M / ↑(M ^ e) ^ σ ≤ (LSeries (fun (n : ℕ) => (χ.zetaMul ^ (r + 1)) n) ↑σ).re

Finite Rankin lower bound obtained from perfect-power support.

theorem DirichletCharacter.rankin_perfectPower_le_zeta_mul_LFunction_pow {q : ℕ} (χ : DirichletCharacter ℂ q) [NeZero q] (hquad : χ ^ 2 = 1) (r : ℕ) {e M : ℕ} (hepos : 0 < e) (heven : ∃ (t : ℕ), e = 2 * t) (hM : 1 ≤ M) {σ : ℝ} (hσ : 1 < σ) : ↑M / ↑(M ^ e) ^ σ ≤ ‖riemannZeta ↑σ‖ ^ (r + 1) * ‖LFunction χ ↑σ‖ ^ (r + 1)

The exact Rankin product inequality. This is the strongest direct output of perfect-power support and absolute convergence before choosing parameters.

theorem DirichletCharacter.rankin_perfectPower_le_zetaMajorant_mul_LFunction_pow {q : ℕ} (χ : DirichletCharacter ℂ q) [NeZero q] (hquad : χ ^ 2 = 1) (r : ℕ) {e M : ℕ} (hepos : 0 < e) (heven : ∃ (t : ℕ), e = 2 * t) (hM : 1 ≤ M) {σ : ℝ} (hσ : 1 < σ) : ↑M / ↑(M ^ e) ^ σ ≤ (1 + 1 / (σ - 1)) ^ (r + 1) * ‖LFunction χ ↑σ‖ ^ (r + 1)

After the elementary zeta majorant, the weighted perfect-power lower has only the displayed strength. At e = r+1 its numerator is overwhelmed by M^((r+1)σ); this records the quantitative Rankin barrier rather than hiding it behind a source predicate.