Reusing the actual analytic reduction with a smaller frequency cutoff

The integral, signed coefficients, full modulus interval, and six-key box are unchanged. Only the genuinely retained frequency set is made smaller.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedMaxFrequency_le_of_cutoff_le {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) (H : ℕ → ℕ → ℕ) (hH : ∀ q ∈ Finset.Ioc 0 ⌊L⌋₊, ∀ r ∈ Finset.Ioc 0 ⌊L⌋₊, H q r ≤ wUniformCutoff M Z q r) (N : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : wExtractedMaxFrequency H N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ ≤ ⌈L ^ 2 / M * Z⌉₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_key_bound_of_cutoff_le {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) (H : ℕ → ℕ → ℕ) (hH : ∀ q ∈ Finset.Ioc 0 ⌊L⌋₊, ∀ r ∈ Finset.Ioc 0 ⌊L⌋₊, H q r ≤ wUniformCutoff M Z q r) (N : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (x η R S ξ : ℝ) (hY : 1 ≤ x ^ η) : ∃ b ≤ Nat.log 2 ⌈L ^ 2 / M * Z⌉₊, ∃ y ∈ Set.Icc (1 / 2) 3, ∃ K ∈ wExtractedKeyBox (x ^ η), |wMaskedFactorExtractedTruncated M H N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ| ≤ 384 * M * ↑(Nat.log 2 ⌈L ^ 2 / M * Z⌉₊ + 1) * (x ^ η) ^ 7 * ‖wExtractedKeyExponential H N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K (M * y)‖

A smaller cutoff uses the same explicit shell count and key loss. This reuses the proved integral and grouping, without replacing a masked sum by an unweighted interval.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_floor_extracted_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 ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ m ∈ U, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have L := x ^ ((5 - 5 * ν) / 9 - ε); have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; R₀ * S₀ = L ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → signedError U (N z) (Finset.Ioc 0 ⌊L⌋₊) α (β z) c a ^ 2 ≤ (8 * ∑ m ∈ U, α m ^ 2) * wMaskedFactorExtractedTruncated M (wFloorCutoff M (x ^ η)) (N z) (Finset.Ioc 0 ⌊L⌋₊) (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) + x ^ 2 / Real.log x ^ A

The cutoff correction is physically paid in the original signed-error bound before any Fourier integral or maximum is taken. The legitimate WF factors still precede every choice of the changing residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_floor_key_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 ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ m ∈ U, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have L := x ^ ((5 - 5 * ν) / 9 - ε); have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; have J := Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊; R₀ * S₀ = L ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∃ b ≤ J, ∃ y ∈ Set.Icc (1 / 2) 3, ∃ K ∈ wExtractedKeyBox (x ^ η), signedError U (N z) (Finset.Ioc 0 ⌊L⌋₊) α (β z) c a ^ 2 ≤ (3072 * M * ∑ m ∈ U, α m ^ 2) * ↑(J + 1) * (x ^ η) ^ 7 * ‖wExtractedKeyExponential (wFloorCutoff M (x ^ η)) (N z) (Finset.Ioc 0 ⌊L⌋₊) (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) b K (M * y)‖ + x ^ 2 / Real.log x ^ A

The corrected original-error endpoint with the same explicit six-key and shell costs. The selected fiber has a genuinely bounded Fourier scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFloorKey_phase_budget {M T x Z y : ℝ} (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) (hy : y ∈ Set.Icc (1 / 2) 3) {N Q : Finset ℕ} (hN : ∀ n ∈ N, T ≤ ↑n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} (ha : |↑a| ≤ x) {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) : have v := wGCDTuple (wExtractedOriginal t.1); |↑t.2| * (|M * y| / (↑K.D * ↑v.k₁ * ↑t.1.1.2.1 * ↑t.1.1.2.2) + |↑a| / (↑v.n₁ * ↑v.k₁ * ↑t.1.1.2.1 * ↑t.1.1.2.2 * ↑K.D')) ≤ 7 * Z

The two smooth monomials on each actual floor-retained point have a uniform budget, with no loss depending on the changing residue or moduli.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFloorKey_zero_or_positive {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (M Z : ℝ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (u : ℝ) : wExtractedKeyExponential (wFloorCutoff M Z) N Q β c₁ γ ζ a P R S ξ b K u = 0 ∨ 0 < K.D ∧ 0 < K.D' ∧ ∃ t ∈ wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K, wExtractedCoefficient β c₁ γ ζ t.1 ≠ 0

Empty or cancelling selected fibers are handled before taking positive source parameters. This applies to the actual floor endpoint above.