theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.log_scales {u : ℝ} {q : ℕ} (hu : 2 ≤ u) (hq : 1 < q) (hqu : ↑q ≤ u ^ 100) : 1 ≤ dirichletLQuadraticConditionalCentralH q (u ^ 2 + 1) ∧ dirichletLQuadraticConditionalCentralH q (u ^ 2 + 1) ≤ 105 * (1 + Real.log u) ∧ Real.log (2 * (u ^ 2 + 1) + 2) ≤ 4 * Real.log u

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.log_power_absorb (C : ℝ) (n : ℕ) {r : ℝ} (hr : 0 < r) : ∀ᶠ (u : ℝ) in Filter.atTop, C * (1 + Real.log u) ^ n ≤ u ^ r

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.fixedH_bound {u c η : ℝ} {q : ℕ} (hu : 2 ≤ u) (hc : 0 < c) (hη : 0 ≤ η) (hq : 1 < q) (hqu : ↑q ≤ u ^ 100) : 0 < dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q (u ^ 2 + 1)) (u ^ 2 + 1) ∧ dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q (u ^ 2 + 1)) (u ^ 2 + 1) ≤ (1000 + 3000000 / c) * ↑q ^ η * (1 + Real.log u) ^ 2

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.nonquadratic_width_eventually : ∀ᶠ (u : ℝ) in Filter.atTop, ∀ (q : ℕ), 1 < q → ↑q ≤ u ^ 100 → 2 / √u ≤ 1 / (274877906944 * (1 + Real.log ↑(dirichletLNonquadraticConductorLogCutoff q (u ^ 2 + 1))) ^ 9)

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.quadratic_denominator_bound {u c η : ℝ} {q : ℕ} (hu : 2 ≤ u) (hc : 0 < c) (hη : 0 ≤ η) (hq : 1 < q) (hqu : ↑q ≤ u ^ 100) : ↑q ^ (2 * η) * dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q (u ^ 2 + 1)) (u ^ 2 + 1) ^ 12 ≤ (1000 + 3000000 / c) ^ 12 * ↑q ^ (14 * η) * (1 + Real.log u) ^ 24

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.quadratic_width_eventually_real (c A : ℝ) (hc : 0 < c) (hA : 0 < A) : ∀ᶠ (u : ℝ) in Filter.atTop, ∀ (q : ℕ), 1 < q → ↑q ≤ u ^ 100 → 2 / √u ≤ dirichletLQuadraticConditionalCrossZeroWidth A c (1 / 10000) q (u ^ 2 + 1)

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.quadraticCrossZeroWidth_eventually (c A : ℝ) (hc : 0 < c) (hA : 0 < A) : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (q : ℕ), 1 < q → ↑q ≤ Real.log ↑x ^ 100 → 2 / √(Real.log ↑x) ≤ dirichletLQuadraticConditionalCrossZeroWidth A c (1 / 10000) q (Real.log ↑x ^ 2 + 1)

The threshold precedes the modulus, and η is fixed once and for all.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.rectangle_mem {a T : ℝ} {s : ℂ} (ha : a ≤ s.re) (hb : s.re ≤ 2) (ht : |s.im| ≤ T) : s ∈ (↑a - Complex.I * ↑T).Rectangle (2 + Complex.I * ↑T)

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.nonquadratic_rectangle_eventually_real : ∀ᶠ (u : ℝ) in Filter.atTop, ∀ (q : ℕ) (hq : 1 < q), have this := ⋯; ↑q ≤ u ^ 100 → ∀ (χ : DirichletCharacter ℂ q), χ ^ 2 ≠ 1 → ∀ (s : ℂ), 1 - 2 / √u ≤ s.re → s.re ≤ 2 → |s.im| ≤ u ^ 2 + 1 → DirichletCharacter.LFunction χ s ≠ 0

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.nonquadratic_rectangle_eventually : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (q : ℕ) (hq : 1 < q), have this := ⋯; ↑q ≤ Real.log ↑x ^ 100 → ∀ (χ : DirichletCharacter ℂ q), χ ^ 2 ≠ 1 → ∀ (s : ℂ), 1 - 2 / √(Real.log ↑x) ≤ s.re → s.re ≤ 2 → |s.im| ≤ Real.log ↑x ^ 2 + 1 → DirichletCharacter.LFunction χ s ≠ 0

No Siegel premise is needed in the nonquadratic branch.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteZeroFreeProducer.finiteRectangle_of_fixedSiegel (c : ℝ) (hc : 0 < c) : ∃ (X₀ : ℕ), ∀ x ≥ X₀, ∀ (q : ℕ) (hq : 1 < q), have this := ⋯; ↑q ≤ Real.log ↑x ^ 100 → ∀ (χ : DirichletCharacter ℂ q), χ.IsPrimitive → (χ ^ 2 = 1 → c * ↑q ^ (-(1 / 10000)) ≤ (DirichletCharacter.LFunction χ 1).re) → ∀ (s : ℂ), 1 - 2 / √(Real.log ↑x) ≤ s.re → s.re ≤ 2 → |s.im| ≤ Real.log ↑x ^ 2 + 1 → DirichletCharacter.LFunction χ s ≠ 0

Finite Eq21 nonvanishing, conditional only on the displayed raw quadratic L(1) lower bound with one fixed c and η=1/10000. The threshold is chosen before x, q, the character and every rectangle point. No all-height assertion and no assertion that the Siegel lower bound has been proved is made.