Original signed distribution error, with no unproved analytic energy input. The genuine family-uniform coprime Siegel--Walfisz premise is explicit.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_wellFactorable_signedError_sq_c2 {ι : Type u_1} {κ k i j : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (U : Finset ℕ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → signedError U (N z) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊) α (β z) c a ^ 2 ≤ 2 * x ^ 2 / Real.log x ^ A

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_wellFactorable_signedError_c2 {ι : Type u_1} {κ k i j : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (U : Finset ℕ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError U (N z) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊) α (β z) c a| ≤ x / Real.log x ^ A

C.2 on its original full modulus interval and residue-uniform domain.