theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedQuadraticConditionalErrorAssembly (c η : ℝ) (hc : 0 < c) (hη : 0 < η) {ν : ℝ → ℝ} (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) : ∃ A > 0, ∃ K > 0, ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {T ε X : ℝ}, χ ^ 2 = 1 → χ ≠ 1 → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 0 < ε → ε < 1 → 1 ≤ X → have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; have d := dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T; have b := dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T; ‖χ.twistedSmoothedPsi ν ε X‖ ≤ K * (T * Q * X ^ a / ε + Q * X ^ b / (ε * (1 + T ^ 2)) + X ^ b * (1 + d⁻¹ ^ 2) / (ε * T))

Raw quadratic Siegel data select a single contour scale and give the full smoothed Perron error. The three displayed terms pay respectively the left edge, both horizontal edges, and both right-line tails.

theorem AnalyticNumberTheory.LargeSieve.exists_quadraticConditionalExactPrefix_of_four_payments (c η : ℝ) (hc : 0 < c) (hη : 0 < η) {ν : ℝ → ℝ} (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) : ∃ A > 0, ∃ K > 0, ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {T ε X R : ℝ}, χ ^ 2 = 1 → χ ≠ 1 → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 0 < ε → ε < 1 → 3 < X → 2 < X * ε → 0 ≤ R → have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; have d := dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T; have b := dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T; T * Q * X ^ a / ε ≤ R → Q * X ^ b / (ε * (1 + T ^ 2)) ≤ R → X ^ b * (1 + d⁻¹ ^ 2) / (ε * T) ≤ R → ε * X * Real.log X ≤ R → ‖lambdaCharacterPrefix ⌊X⌋₊ q χ‖ ≤ K * R

The strongest exact-prefix consumer at the contour level: once each of the three contour terms and the smoothing-removal term is paid by a common R, the genuine prefix through ⌊X⌋₊ is O(R). No nonquadratic theorem is used.