Quantitative logarithmic derivative in the quadratic central band

This file turns the raw lower bound at s = 1 into an explicit lower bound throughout the central band used by the cross-zero rectangle. In particular, the denominator in L'/L is paid quantitatively; zero-freeness or compactness alone is never used as a substitute for a uniform lower bound.

The resulting bound retains the honest factor q^η / c forced by the supplied raw Siegel lower bound c q⁻η ≤ L(1,χ). Removing that power requires a stronger (polylogarithmic) lower input, not a topological argument.

theorem AnalyticNumberTheory.LargeSieve.norm_LFunction_ge_half_siegel_on_quadraticConditionalCentralBand {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A c η T β t : ℝ} (hA : 0 < A) (hAc : A ≤ c / 256) (hAhalf : A ≤ 1 / 2) (hc : 0 < c) (hη : 0 < η) (hT : 0 < T) (hSiegel : c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re) (hβ : 1 - dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ β) (hβone : β ≤ 1) (ht : |t| ≤ dirichletLQuadraticConditionalCentralHeight c η q T) : c * ↑q ^ (-η) / 2 ≤ ‖DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t)‖

Quantitative central-band lower bound. It is obtained by transporting the raw lower bound at 1 along one vertical and one horizontal segment.

theorem AnalyticNumberTheory.LargeSieve.norm_logDerivative_le_on_quadraticConditionalCentralBand {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A c η T β t : ℝ} (hA : 0 < A) (hAc : A ≤ c / 256) (hAhalf : A ≤ 1 / 2) (hc : 0 < c) (hη : 0 < η) (hT : 0 < T) (hSiegel : c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re) (hβ : 1 - dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ β) (hβone : β ≤ 1) (ht : |t| ≤ dirichletLQuadraticConditionalCentralHeight c η q T) : ‖deriv (DirichletCharacter.LFunction χ) (↑β + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t)‖ ≤ 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η))

Explicit L'/L bound on the central band. The only inverse lower-bound factor is the visible 2 / (c q⁻η).