Removing finitely many conductors from a quadratic Siegel lower bound

This module isolates a quantifier bridge needed by a genuine Landau--Siegel lower bound. Strict positivity at each nonprincipal quadratic character makes all conductors below a fixed threshold harmless: finiteness of the character groups supplies one positive constant for those conductors. Consequently it is enough to prove the power lower bound uniformly for all sufficiently large conductors.

No characters or conductors are enumerated in this argument.

theorem DirichletCharacter.exists_fixed_conductor_quadratic_LFunction_one_lower (q : ℕ) [NeZero q] (η : ℝ) : ∃ (c : ℝ), 0 < c ∧ ∀ (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (LFunction χ 1).re

At one fixed nonzero conductor, positivity of quadratic nonprincipal L(1, χ) can be made uniform over all characters.

theorem DirichletCharacter.exists_below_conductor_quadratic_LFunction_one_lower (Q : ℕ) (η : ℝ) : ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), q < Q → χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (LFunction χ 1).re

All nonzero conductors below a fixed threshold have one uniform positive quadratic L(1, χ) power lower constant.

theorem DirichletCharacter.exists_quadratic_LFunction_one_lower_of_eventual (η : ℝ) (_hη : 0 < η) (hlarge : ∃ (Q : ℕ) (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), Q ≤ q → χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (LFunction χ 1).re) : ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (LFunction χ 1).re

Finite-exception bridge for the quadratic Landau--Siegel lower bound. A uniform power lower bound beyond an arbitrary fixed conductor threshold extends to every conductor. The small-conductor constant is obtained from the actual finite character groups and strict positivity, rather than from a finite scan or a supplied small-conductor predicate.

theorem DirichletCharacter.quadratic_LFunction_one_lower_of_eventual_forall_exponents (hlarge : ∀ (η : ℝ), 0 < η → ∃ (Q : ℕ) (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), Q ≤ q → χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (LFunction χ 1).re) (η : ℝ) : 0 < η → ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (LFunction χ 1).re

Quantifier-level reduction of the full Landau--Siegel lower bound: it is enough to establish each exponent uniformly beyond some conductor threshold. All finite exceptions are discharged unconditionally by the preceding theorem.