Clean beta at the original C.2 entry and in the first gcd exclusion

The original error is reduced to the genuine nonzero W mode of the constructed clean sequence. Its SW input is proved for the enlarged changing-residue family. The first large-gcd exclusion is then applied with upper beta endpoint 2*T, not T. No claim is made for the other four exclusions or the IV.3 remainder.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_clean_nonzeroMode_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 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 ≤ (2 * ∑ m ∈ S, α m ^ 2) * smoothWNonzeroMode M (N z) Q (betaClean (β z) a) c a + x ^ 2 / Real.log x ^ A

The original, uncleaned signed error after honest divisor deletion and zero-mode payment. All orders, including the SW order, may be zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_wMaskedTruncated_largeGCD_dyadic (i k j : ℕ) (A : ℝ) {η : ℝ} (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → 4 * M * T = x → 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| ≤ x → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → x ^ η < ↑(t.2.1.gcd t.2.2)) → |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q (betaClean β a) c a P| ≤ 12 * M * T ^ 2 * x ^ (-η / 8) ∧ (∑ m ∈ S, α m ^ 2) * |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q (betaClean β a) c a P| ≤ x ^ 2 / Real.log x ^ A

Physical application of the accepted first-gcd estimate to betaClean. The factor 12 is 3 * (2*T)^2 / T^2; the beta endpoint is not confused with its lower dyadic scale. No beta nondivisibility assumption remains.