Closed quadratic zero-free ingredients

The endpoint optimization is intentionally not asserted here. These public lemmas close the vertical fundamental theorem, the low-height two-segment argument once its sharp derivative budgets have been instantiated, and the high-height (3,4,1) contradiction while consuming the actual principal Euler-correction and pole-plus-log zeta bounds.

theorem AnalyticNumberTheory.LargeSieve.integral_verticalDeriv_LFunction_eq_sub {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (t : ℝ) (hderivContinuous : Continuous (deriv fun (v : ℝ) => DirichletCharacter.LFunction χ (1 + ↑v * Complex.I))) : ∫ (u : ℝ) in 0..t, deriv (fun (v : ℝ) => DirichletCharacter.LFunction χ (1 + ↑v * Complex.I)) u = DirichletCharacter.LFunction χ (1 + ↑t * Complex.I) - DirichletCharacter.LFunction χ 1

Genuine vertical fundamental theorem for a nonprincipal Dirichlet L-function. The derivative here is the real derivative of the actual vertical restriction, so the statement contains no assumed path identity.

theorem AnalyticNumberTheory.LargeSieve.norm_LFunction_sub_le_sixtyfour_mul_conductorHeightLogSq {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {σ₁ σ₂ t : ℝ} (hσ₁half : 1 / 2 ≤ σ₁) (hσ₁lower : 1 - 1 / Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t) ≤ σ₁) (hσ₁σ₂ : σ₁ ≤ σ₂) (hσ₂upper : σ₂ ≤ 2) : ‖DirichletCharacter.LFunction χ (↑σ₂ + ↑t * Complex.I) - DirichletCharacter.LFunction χ (↑σ₁ + ↑t * Complex.I)‖ ≤ 64 * (1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t)) ^ 2 * (σ₂ - σ₁)

Integrating the conductor-height derivative estimate along a horizontal segment gives a logarithmic, rather than polynomial-in-the-conductor, budget.

noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalPowerZeroFreeH (q : ℕ) (t : ℝ) : ℝ

Common conductor-height and zeta-pole scale used in the conditional quadratic zero-free headline.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalPowerZeroFreeH q t = 1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t) + if _ht : t = 0 then 0 else 1 + Real.log (|2 * t| + 2) + 1 / |2 * t|

theorem AnalyticNumberTheory.LargeSieve.norm_LFunction_vertical_sub_le_sixtyfour_mul_conductorHeightLogSq {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (t : ℝ) : ‖DirichletCharacter.LFunction χ (1 + ↑t * Complex.I) - DirichletCharacter.LFunction χ 1‖ ≤ 64 * (1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t)) ^ 2 * |t|

Integrating the global conductor-log derivative bound along the genuine vertical segment gives a linear-in-|t| budget at re s = 1.

theorem AnalyticNumberTheory.LargeSieve.LFunction_ne_zero_lowHeight_of_twoSegmentBudgets {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) {β t Bh Bv : ℝ} (hhorizontal : ‖DirichletCharacter.LFunction χ (1 + ↑t * Complex.I) - DirichletCharacter.LFunction χ (↑β + ↑t * Complex.I)‖ ≤ Bh) (hvertical : ‖DirichletCharacter.LFunction χ (1 + ↑t * Complex.I) - DirichletCharacter.LFunction χ 1‖ ≤ Bv) (hbudget : Bh + Bv < (DirichletCharacter.LFunction χ 1).re) : DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0

Low-height two-segment exclusion. The endpoint value is identified with its positive real part using quadraticity. hhorizontal and hvertical are the two sharp derivative-integral budgets, and the preceding theorem supplies the required vertical fundamental theorem when establishing hvertical.

theorem AnalyticNumberTheory.LargeSieve.norm_quadraticSquare_LFunction_le_principalPolePlusLog {q : ℕ} [NeZero q] (Z : ℝ) (hzeta : ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) {x t : ℝ} (hx : 0 < x) (hx1 : x ≤ 1) (ht : t ≠ 0) : ‖DirichletCharacter.LFunction (χ ^ 2) (1 + ↑x + Complex.I * (2 * ↑t))‖ ≤ (1 + Real.log ↑q) * (Z * (1 + Real.log (|2 * t| + 2) + 1 / |2 * t|))

Actual principal-square estimate used in the high-height branch. This directly consumes both accepted analytic inputs; it is not an abstract source predicate.

theorem AnalyticNumberTheory.LargeSieve.LFunction_ne_zero_highHeight_of_valueProduct {q : ℕ} [NeZero q] (Z : ℝ) (hZ : 0 < Z) (hzeta : ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (_hχ : χ ≠ 1) {β t x D : ℝ} (hx : 0 < x) (hx1 : x ≤ 1) (ht : t ≠ 0) (htriv : ‖DirichletCharacter.LFunctionTrivChar q (1 + ↑x)‖ ≤ 2 / x) (hright : ‖DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑t)‖ ≤ D * x) (hpay : 8 * (1 + Real.log ↑q) * (Z * (1 + Real.log (|2 * t| + 2) + 1 / |2 * t|)) * (D * x) ^ 4 < x ^ 3) : DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0

High-height (3,4,1) contradiction. The actual principal-square bound is invoked in the proof. htriv and hright are precisely the elementary principal-pole and Taylor estimates to be discharged by the surrounding power-width arithmetic.

theorem AnalyticNumberTheory.LargeSieve.one_le_dirichletLQuadraticConditionalPowerZeroFreeH (q : ℕ) [NeZero q] (t : ℝ) : 1 ≤ dirichletLQuadraticConditionalPowerZeroFreeH q t

The combined conductor-height/pole scale is at least one.

theorem AnalyticNumberTheory.LargeSieve.one_add_log_conductorHeightCutoff_le_quadraticH (q : ℕ) [NeZero q] (t : ℝ) : 1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t) ≤ dirichletLQuadraticConditionalPowerZeroFreeH q t

The conductor logarithm is dominated by the common scale.

theorem AnalyticNumberTheory.LargeSieve.one_add_log_twoHeight_add_inv_le_quadraticH (q : ℕ) [NeZero q] {t : ℝ} (ht : t ≠ 0) : 1 + Real.log (|2 * t| + 2) + 1 / |2 * t| ≤ dirichletLQuadraticConditionalPowerZeroFreeH q t

For nonzero height, the pole-plus-log factor is also dominated by the common scale.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletL_quadratic_conditional_powerZeroFree (c η : ℝ) (hc : 0 < c) (hη : 0 < η) : ∃ (A : ℝ), 0 < A ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q) (β t : ℝ), χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → β ∈ Set.Ico (1 - A * ↑q ^ (-2 * η) / dirichletLQuadraticConditionalPowerZeroFreeH q t ^ 12) 1 → DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0

A genuine conditional quadratic headline. A Siegel-type lower bound at one, with its premise left explicit, gives a single power-width zero-free region at every height. The low branch uses both the horizontal and the accepted vertical derivative budgets; the complementary branch uses the (3,4,1) value-product argument.