The actual signed distribution error after zero-mode payment

At the source normalization x = 4 M T, the full zero-mode difference and both U/V errors are paid. Only the original signed nonzero W mode is retained. This is a reduction, not a bound for that oscillatory remainder.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_nonzeroMode_c2 {ι : Type u_1} {κ k ℓ j : ℕ} (hk : 1 ≤ k) (hℓ : 1 ≤ ℓ) (hj : 1 ≤ j) (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (i : ι), 1 ≤ T i) (hN : ∀ (i : ι), ∀ n ∈ N i, T i ≤ ↑n ∧ ↑n ≤ 2 * T i) (hβ : ∀ (i : ι), ∀ n ∈ N i, |β i n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (i : ι) (M L : ℝ), 1 ≤ M → 1 ≤ L → 4 * M * T i = x → x ^ ε ≤ T i → T i ≤ x ^ (1 / 10) → L ≤ x ^ (5 / 9) → ∀ (S Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau ℓ) m)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), signedError S (N i) Q α (β i) c a ^ 2 ≤ (∑ m ∈ S, α m ^ 2) * smoothWNonzeroMode M (N i) Q (β i) c a + x ^ 2 / Real.log x ^ A

Uniform reduction of the actual signed bilinear distribution error at the full dyadic C.2 scales. The given SW family is at the lower beta scale; its doubled-scale transport is proved, not assumed. The W term stays signed.