theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_eventually_signedError_bound (i k j : ℕ) {Cscale δ : ℝ} (hC : 1 ≤ Cscale) (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → L ≤ x → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ Cscale * x → |signedError S N Q α (betaDivisorPart β a) c a| ≤ 4 * (M + L) * x ^ (3 * δ)

Actual divisor deletion, including equality progressions, at a fixed shift multiple.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_divisorPart_power_saving (i k j : ℕ) {Cscale ε : ℝ} (hC : 1 ≤ Cscale) (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → x ^ ε ≤ T → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ Cscale * x → |signedError S N Q α (betaDivisorPart β a) c a| ≤ x ^ (1 - min ε (4 / 9) / 2)

Power saving uniform in the complete changing input. In particular, the residue may vary throughout 0 < |a| ≤ x, including equality progressions.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_signedError_log_payment (i k j A : ℕ) {Cscale ε : ℝ} (hC : 1 ≤ Cscale) (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → x = 4 * M * T → x ^ ε ≤ T → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ Cscale * x → |signedError S N Q α (betaDivisorPart β a) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α β c a - signedError S N Q α (betaClean β a) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α β c a| ≤ |signedError S N Q α (betaClean β a) c a| + x / Real.log x ^ A

The genuine C.2 preprocessing payment, not an assumed error estimate. For fixed orders (including zero), saving order, and positive epsilon, one threshold works simultaneously for all scales, supports, signed sequences and nonzero residues in the full permitted range. The original-to-clean difference and the triangle transfer are part of the same uniform conclusion.