The original signed error reduced to the clean first-small-gcd truncation

The only retained oscillatory term has the actual original tuple domain, the actual constructed cutoff, and the mask gcd(n₁,n₂) ≤ x ^ η. The full truncation tail and the complementary first-large-gcd contribution are paid after multiplication by alpha-squared. This is only the first gcd exclusion: it is neither WGCDData.Small (all five gcds) nor IV.3.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode_eq_firstGCD_small_add_large (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : truncatedWNonzeroMode M H N Q β c a = (wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => ↑(t.2.1.gcd t.2.2) ≤ Y) + wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => Y < ↑(t.2.1.gcd t.2.2)

Exact partition of the actual truncated tuple sum by the first gcd. No coefficients, compatibility conditions, supports, or phases are changed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWNonzeroMode_eq_firstGCD_small_add_large_add_tail (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : smoothWNonzeroMode M N Q β c a = ((wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => ↑(t.2.1.gcd t.2.2) ≤ Y) + wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => Y < ↑(t.2.1.gcd t.2.2)) + wMaskedTail M H N Q β c a fun (x : WOriginalTuple) => True

Full signed decomposition, retaining the unmasked tail rather than silently dropping frequencies on either side of the first-gcd partition.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_clean_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 ≤ ((2 * ∑ 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 ^ η) + x ^ 2 / Real.log x ^ A

The original, uncleaned signed error has only the signed, clean, first-small-gcd truncated sum left. All discarded pieces are uniformly logarithmically paid at the same constructed cutoff. All orders may be zero.