High-omega preprocessing at the original C.2 entry

The high-omega part of the original beta is cleaned before its progression estimate; its divisor part, including m*n=a, is paid separately. Only then is dispersion reapplied to the low-omega SW family. The resulting signed W has an explicit restriction on both beta indices, with the same original modulus coefficients and the same constructed frequency cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_lowOmega_comm (β : ℕ → ℝ) (a : ℤ) (ξ : ℝ) : betaClean (betaLowOmega β ξ) a = betaLowOmega (betaClean β a) ξ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_highOmega_comm (β : ℕ → ℝ) (a : ℤ) (ξ : ℝ) : betaClean (betaHighOmega β ξ) a = betaHighOmega (betaClean β a) ξ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily.betaLowOmega_clean {ι : Type u_1} {κ k : ℕ} {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), N z ⊆ Finset.Ioc 0 ⌊2 * T z⌋₊) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : BetaCoprimeSWFamily (κ + 1 + 1) (fun (z : BetaCleanIndex (fun (w : BetaLowOmegaIndex T) => T w.index) ε) => T z.index.index) (fun (z : BetaCleanIndex (fun (w : BetaLowOmegaIndex T) => T w.index) ε) => N z.index.index) fun (z : BetaCleanIndex (fun (w : BetaLowOmegaIndex T) => T w.index) ε) => LiLiuPrereqFouvry.betaClean (LiLiuPrereqFouvry.betaLowOmega (β z.index.index) (highOmegaCutoff z.index.scale)) z.residue

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_original_signedError_log_payment (i k j A : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → 4 * M * T = x → 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| ≤ x → |signedError S N Q α (betaHighOmega β (highOmegaCutoff x)) c a| ≤ x / Real.log x ^ A ∧ |signedError S N Q α β c a - signedError S N Q α (betaLowOmega β (highOmegaCutoff x)) c a| ≤ x / Real.log x ^ A

Original beta needs neither a nondivisibility condition nor a high-omega vanishing condition. Every changing datum follows the common threshold.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_betaLowOmega (M ξ : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : wMaskedTruncated M H N Q (betaLowOmega β ξ) c a P = wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => P t ∧ ↑t.2.1.primeFactors.card ≤ ξ ∧ ↑t.2.2.primeFactors.card ≤ ξ

A genuine restriction of the tuple domain, retaining all compatibility and Fourier factors. This identity does not assert any WF closure.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_lowOmega_firstGCD_truncated_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 < ε) (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M L : ℝ), 1 ≤ M → 1 ≤ L → 4 * M * T z = x → x ^ ε ≤ T z → T z ≤ 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 i) m)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → signedError S (N z) Q α (β z) c a ^ 2 ≤ ((4 * ∑ m ∈ S, α m ^ 2) * wMaskedTruncated M (wUniformCutoff M (x ^ η)) (N z) Q (betaClean (β z) a) c a fun (t : WOriginalTuple) => ↑(t.2.1.gcd t.2.2) ≤ x ^ η ∧ ↑t.2.1.primeFactors.card ≤ highOmegaCutoff x ∧ ↑t.2.2.primeFactors.card ≤ highOmegaCutoff x) + x ^ 2 / Real.log x ^ A

Original signed C.2 error after high-omega deletion, divisor deletion, zero-mode cancellation, full-tail payment, and the first gcd exclusion. The coefficient four is explicit; the retained W is still signed.