Quantitative six-key grouping of the actual extracted exponential sum

The five canonical gcd coordinates and the extraction divisor Δ give an explicit finite box. The complementary divisor Δ' is determined on each fiber. All original masks, cutoffs, signed coefficients, and both frequency signs remain in the actual fiber sums. The triangle inequality is used only between these fibers, not between their oscillatory summands.

This supplies the finite-key cost underlying Fouvry (1987), p. 627, (3.12). It is not an IV.3 cancellation estimate or a completion of C.2.

@[reducible, inline]

abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedKey : Type

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedKey = ((ℕ × ℕ × ℕ × ℕ × ℕ) × ℕ)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKey (z : WExtractedTuple) : WExtractedKey

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKey z = ((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z)).key, z.1.1.1)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyBox (Y : ℝ) : Finset WExtractedKey

A full rectangular box, not the image of the actual carrier.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyBox Y = (Finset.range (⌊Y⌋₊ + 1) ×ˢ Finset.range (⌊Y⌋₊ + 1) ×ˢ Finset.range (⌊Y⌋₊ + 1) ×ˢ Finset.range (⌊Y⌋₊ + 1) ×ˢ Finset.range (⌊Y⌋₊ + 1)) ×ˢ Finset.range (⌊Y ^ 2⌋₊ + 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wExtractedKeyBox_iff {Y : ℝ} {K : WExtractedKey} : K ∈ wExtractedKeyBox Y ↔ K.1.1 ≤ ⌊Y⌋₊ ∧ K.1.2.1 ≤ ⌊Y⌋₊ ∧ K.1.2.2.1 ≤ ⌊Y⌋₊ ∧ K.1.2.2.2.1 ≤ ⌊Y⌋₊ ∧ K.1.2.2.2.2 ≤ ⌊Y⌋₊ ∧ K.2 ≤ ⌊Y ^ 2⌋₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyBox_nonempty (Y : ℝ) : (wExtractedKeyBox Y).Nonempty

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyBox_card (Y : ℝ) : (wExtractedKeyBox Y).card = (⌊Y⌋₊ + 1) ^ 5 * (⌊Y ^ 2⌋₊ + 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyBox_card_le {Y : ℝ} (hY : 1 ≤ Y) : ↑(wExtractedKeyBox Y).card ≤ 128 * Y ^ 7

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtracted_extraction_spec {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a P R S ξ) : 0 < z.1.1.1 ∧ 0 < z.1.1.2 ∧ z.1.1.1 * z.1.1.2 = (wGCDTuple (wExtractedOriginal z)).δ * (wGCDTuple (wExtractedOriginal z)).δ₂ ∧ P (wExtractedOriginal z)

The actual extraction equation and strict positivity, without replacing Δ' by a new independent coordinate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKey_mem_box {N Q : Finset ℕ} {a : ℤ} {x η R S ξ : ℝ} {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a (c2FiveSmallMask x η) R S ξ) : wExtractedKey z ∈ wExtractedKeyBox (x ^ η)

Membership of the full six-key box follows from the actual mask and the extraction equation; Δ ≤ δ*δ₂ ≤ Y² uses Δ' > 0.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) : Finset (WExtractedTuple × ℤ)

The carrier remains a filter of the original extracted frequency block.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber H N Q a P R S ξ b K = {t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.frequencyBlock (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencies H N Q a P R S ξ) Prod.snd b | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKey t.1 = K}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wExtractedKeyFiber_iff {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K ↔ t ∈ frequencyBlock (wExtractedFrequencies H N Q a P R S ξ) Prod.snd b ∧ wExtractedKey t.1 = K

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_spec {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : (wGCDTuple (wExtractedOriginal t.1)).key = K.1 ∧ t.1.1.1.1 = K.2 ∧ 0 < K.2 ∧ 0 < t.1.1.1.2 ∧ t.1.1.1.2 = K.1.2.2.1 * K.1.2.2.2.2 / K.2

Fixed canonical source data on a fiber, including the determined complementary extraction divisor.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyExponential (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (u : ℝ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyExponential H N Q β c₁ γ ζ a P R S ξ b K u = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFourierExponentialSum (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber H N Q a P R S ξ b K) (fun (t : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple × ℤ) => MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient β c₁ γ ζ t.1) a (fun (t : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple × ℤ) => (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).1.1) (fun (t : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple × ℤ) => (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).1.2) (fun (t : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple × ℤ) => (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).2.1) (fun (t : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple × ℤ) => (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).2.2) Prod.snd u

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedBlockExponential_eq_sum_keys (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (x η R S ξ : ℝ) (b : ℕ) (u : ℝ) : wExtractedBlockExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b u = ∑ K ∈ wExtractedKeyBox (x ^ η), wExtractedKeyExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K u

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedBlockExponential_le_keyMax (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (x η R S ξ : ℝ) (b : ℕ) (u : ℝ) : ∃ K ∈ wExtractedKeyBox (x ^ η), (∀ K' ∈ wExtractedKeyBox (x ^ η), ‖wExtractedKeyExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K' u‖ ≤ ‖wExtractedKeyExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K u‖) ∧ ‖wExtractedBlockExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b u‖ ≤ ↑(wExtractedKeyBox (x ^ η)).card * ‖wExtractedKeyExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K u‖

A key attaining the maximum of the actual fiber sums, with the exact rectangular-box cardinality as loss. Empty source carriers cause no problem.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedBlockExponential_le_keyMax_power (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (x η R S ξ : ℝ) (b : ℕ) (u : ℝ) (hY : 1 ≤ x ^ η) : ∃ K ∈ wExtractedKeyBox (x ^ η), ‖wExtractedBlockExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b u‖ ≤ 128 * (x ^ η) ^ 7 * ‖wExtractedKeyExponential H N Q β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K u‖

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_fullLevel_key_bound {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) (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 (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ| ≤ 384 * M * ↑(Nat.log 2 ⌈L ^ 2 / M * Z⌉₊ + 1) * (x ^ η) ^ 7 * ‖wExtractedKeyExponential (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a (c2FiveSmallMask x η) R S ξ b K (M * y)‖

The actual full-level extracted W is bounded by one actual six-key fiber. The logarithmic shell cost and polynomial key cost are explicit.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_fullLevel_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 (wUniformCutoff 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 original signed-error endpoint with quantitative six-key cost. WF factors are still chosen before a; no new SW hypothesis, arbitrary fiber bound, or cancellation claim is introduced.