Removing the large supported beta factor from the original C.2 error

The original signed error is now restricted to low-omega beta pairs with d, δ, and d₁ small. This is an exact subdivision of the previous tuple domain followed by the same-mask payment, not monotonicity of a signed sum. The two supported modulus factors and the IV.3 estimate remain separate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_eq_support_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 ∧ ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁ ≤ Y) + wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => P t ∧ Y < ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁

Partition the actual truncated sum inside any preceding mask by d₁.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_lowOmega_twoGCD_support_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 ^ η) ∧ ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁ ≤ x ^ η) + x ^ 2 / Real.log x ^ A

The original error reduced to three small canonical coordinates. The SW constants belong to the original beta family and are uniform in its index and the changing residue. All fixed divisor orders may be zero.