theorem AnalyticNumberTheory.LargeSieve.fourFactor_siegel_noZero_or_witness (η : ℝ) (hη : 0 < η) : ∃ (δ : ℝ), 0 < δ ∧ δ ≤ 1 / 8 ∧ 48 * δ ≤ η ∧ ((∃ (ξ : PrimitiveQuadraticDatum), ∃ β ∈ Set.Ioo (1 - δ) 1, have this := ⋯; DirichletCharacter.LFunction ξ.character ↑β = 0) ∨ ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re)

Classical ineffective dichotomy. The zero witness need not have minimal conductor. The width pays a Q³ error after an eighth-power cutoff (24δ≤η/2). This is not yet the raw lower bound: the real-zero branch remains explicit.