Total control of the quadratic Siegel convolution discrepancy

The floor sum is split at m. On d < m, the floor error is at most one and |Re χ(d)| ≤ 1, so the complete short contribution costs at most m. On d ≥ m, the existing Pólya--Vinogradov/Abel estimate controls the floor-weighted tail. The final theorem inserts this honest total estimate back into the square-lower-bound/Pólya--Vinogradov bridge.

This closes the discrepancy-control layer. It does not by itself prove a large-conductor Siegel lower bound: optimizing this one-fold square estimate leaves an error on the scale forced by sqrt q (1 + log q). A genuine higher-convolution or power-amplification producer is still required before one can derive L(1,χ) ≫_η q⁻η.

theorem DirichletCharacter.abs_natDiv_cast_sub_div_le_one (X d : ℕ) (hd : 1 ≤ d) : |↑(X / d) - ↑X / ↑d| ≤ 1

A real quotient differs from its natural-number floor by at most one.

theorem DirichletCharacter.abs_quadratic_shortFloorError_le {q : ℕ} (χ : DirichletCharacter ℂ q) (X m : ℕ) : |∑ d ∈ Finset.Ico 1 m, (↑(X / d) * (χ ↑d).re - ↑X * ((χ ↑d).re / ↑d))| ≤ ↑m

The entire short floor-error segment costs at most the cutoff m.

theorem DirichletCharacter.IsPrimitive.abs_quadraticSiegelConvolutionDiscrepancy_le {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hq : 1 < q) {m X : ℕ} (hm : 1 ≤ m) (hmX : m ≤ X) : |χ.quadraticSiegelConvolutionDiscrepancy X m| ≤ ↑m + 8 * √↑q * (1 + Real.log ↑q) * ↑(X / m)

Total discrepancy bound: short floor error plus the oscillatory long tail.

theorem DirichletCharacter.IsPrimitive.sqrt_sub_totalDiscrepancyError_sub_polyaVinogradovError_le {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hquad : χ ^ 2 = 1) (hnonprincipal : χ ≠ 1) (hq : 1 < q) {m X : ℕ} (hm : 1 ≤ m) (hmX : m ≤ X) : ↑X.sqrt - (↑m + 8 * √↑q * (1 + Real.log ↑q) * ↑(X / m)) - ↑X * (8 * √↑q * (1 + Real.log ↑q) / ↑m) ≤ ↑X * (LFunction χ 1).re

The square lower bound with the total discrepancy estimate substituted. This is the strongest unconditional output of the present one-fold route.