The original C.2 error with both gcd restrictions

The low-omega, first-small-beta-gcd tuple domain is partitioned by the common modulus. Its large part is paid using its own original sum, zero mode and tail. The retained signed sum has the same coefficients, phases and frequency cutoff. The three remaining support-factor exclusions and IV.3 are not asserted here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_eq_delta_small_add_large (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : wMaskedTruncated M H N Q β c a P = (wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => P t ∧ ↑(t.1.1.gcd t.1.2) ≤ Y) + wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => P t ∧ Y < ↑(t.1.1.gcd t.1.2)

An exact partition inside any existing arithmetic mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_lowOmega_twoGCD_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) ∧ ↑(t.1.1.gcd t.1.2) ≤ x ^ η) + x ^ 2 / Real.log x ^ A

The original signed error, with no nondivisibility premise on beta, reduced to low-omega tuples with both beta gcd and modulus gcd small. All orders may be zero; the SW constants still precede the changing family index, scales and residue. No closure of WF weights under masks is used.