theorem AnalyticNumberTheory.LargeSieve.fourFactor_fixed_zero_residue_lower (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) {β : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hz : have this := ⋯; DirichletCharacter.LFunction x.character ↑β = 0) : (1 - β) / (2 * ((5000 * ↑(x.modulus * y.modulus) ^ 3) ^ 8) ^ (1 - β)) ≤ (FourFactorLogInduction_residue x y).re

A genuine fixed zero gives a lower bound for the same actual residue whose upper bound costs three logarithms.

theorem AnalyticNumberTheory.LargeSieve.fourFactor_log_cube_absorption {Q η : ℝ} (hQ : 1 ≤ Q) (hη : 0 < η) : (1 + Real.log Q) ^ 3 ≤ (1 + 6 / η) ^ 3 * Q ^ (η / 2)

Uniform elementary log absorption, without any varying cutoff.

theorem AnalyticNumberTheory.LargeSieve.fourFactor_denominator_bound {Q η d : ℝ} (hQ : 1 ≤ Q) (hη : 0 < η) (hdη : 24 * d ≤ η / 2) : ((5000 * Q ^ 3) ^ 8) ^ d * (1 + Real.log Q) ^ 3 ≤ 5000 ^ (8 * d) * (1 + 6 / η) ^ 3 * Q ^ η

The actual eighth-power cutoff costs exactly 24d in the level. The remaining half exponent absorbs all three logarithms.

theorem AnalyticNumberTheory.LargeSieve.fourFactor_fixed_zero_value_lower (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) {β η : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hη : 0 < η) (hdη : 24 * (1 - β) ≤ η / 2) (hz : have this := ⋯; DirichletCharacter.LFunction x.character ↑β = 0) : (1 - β) / (64 * 5000 ^ (8 * (1 - β)) * (1 + 6 / η) ^ 3 * x.value) * ↑(x.modulus * y.modulus) ^ (-η) ≤ y.value

Fixed-zero extraction, uniform over every distinct primitive quadratic datum. All constants depend only on the fixed datum, fixed zero and exponent.

theorem AnalyticNumberTheory.LargeSieve.fourFactor_raw_lower_of_fixed_zero (x : PrimitiveQuadraticDatum) {β η : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hη : 0 < η) (hdη : 24 * (1 - β) ≤ η / 2) (hz : have this := ⋯; DirichletCharacter.LFunction x.character ↑β = 0) : ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re

The genuine zero branch gives the raw bound after the already proved finite-conductor bridge. The cutoff and constant precede q and χ.

theorem AnalyticNumberTheory.LargeSieve.fourFactor_rawLandauSiegelLowerBound : RawLandauSiegelLowerBound

Unconditional raw Landau--Siegel theorem for every positive exponent. The only analytic sources are the actual small-value/real-zero dichotomy, the actual real-zero residue lower bound, and the log-cubed induction upper bound.

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

Requested headline specialization; no lower-bound source is a hypothesis.