Conditional Landau--Siegel to low Siegel--Walfisz adapter

This module deliberately does not claim that the raw Landau--Siegel lower bound alone has already been connected to a quadratic pointwise prime-number theorem. The existing quadratic theorem supplies a power-width zero-free region, but the quadratic rectangle/logarithmic-derivative estimates, Perron contour bounds, smoothing removal, and scalar error payment have not yet been assembled in the production graph.

Accordingly, the theorem below leaves that exact analytic implication as the explicit argument hquadraticZeroFreeToPointwise. The Landau--Siegel premise itself is written with its raw quantifiers and is not packaged as a Source. The conclusion is the genuine prefix-maximal low source only after this additional premise is supplied.

theorem AnalyticNumberTheory.LargeSieve.nonprincipalPrimitivePsiSiegelWalfiszSource_of_landauSiegelLowerBound {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) (hLandauSiegel : ∀ (η : ℝ), 0 < η → ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re) (hquadraticZeroFreeToPointwise : ∀ (C D : ℕ) (η A : ℝ), 0 < η → 0 < A → (∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → ∀ (β t : ℝ), β ∈ Set.Ico (1 - A * ↑q ^ (-2 * η) / dirichletLQuadraticConditionalPowerZeroFreeH q t ^ 12) 1 → DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0) → ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → ∀ (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → ∀ y ≤ N, ‖lambdaCharacterPrefix y q χ‖ ≤ K * ↑N / Real.log ↑N ^ D) : NonprincipalPrimitivePsiSiegelWalfiszSource

Honest conditional adapter from a raw, uniform Landau--Siegel lower bound at 1 to the actual nonprincipal primitive low Siegel--Walfisz source.

The second premise exposes the remaining quadratic analytic assembly: it must turn the concrete power-width zero-free region into a pointwise bound for every prefix. This is intentionally stronger and more explicit than merely assuming holomorphy, since the current production graph has no quadratic counterpart of its nonquadratic contour/error-assembly chain.