Third Harmonic Extraction

This module focuses on the Fourier domain analysis of the weighted sieve sums, specifically expanding the hit counts into frequencies and isolating the main terms and the key third harmonic contribution.

noncomputable def KrafftSieve.wHat (n : ℕ) (W : ZMod (q n) → ℝ) (h : ZMod (q n)) : ℂ

Define $\hat{W}(h)$ (Fourier Transform of the Weight): Define $\hat{W}(h)$ as the Discrete Fourier Transform of the weight function $W(x)$ over $\mathbb{Z}/q\mathbb{Z}$: $$ \hat{W}(h) = \frac{1}{q} \sum_{x=0}^{q-1} W(x) e^{-2\pi i h x / q} $$

Equations

• KrafftSieve.wHat n W h = 1 / ↑(KrafftSieve.q n) * ∑ x : ZMod (KrafftSieve.q n), ↑(W x) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑(h.val * x.val) / ↑(KrafftSieve.q n))

noncomputable def KrafftSieve.gHat (n : ℕ) (i : Fin (w n)) (h : ZMod (q n)) : ℂ

Define $\hat{g}_i(h)$ (Fourier Transform of the Local Hit): Define $\hat{g}_i(h)$ as the Discrete Fourier Transform of the local hit function $g_i(x)$: $$ \hat{g}_i(h) = \frac{1}{q} \sum_{x=0}^{q-1} g_i(x) e^{-2\pi i h x / q} $$

Equations

• KrafftSieve.gHat n i h = 1 / ↑(KrafftSieve.q n) * ∑ x : ZMod (KrafftSieve.q n), ↑(KrafftSieve.g n i x) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑(h.val * x.val) / ↑(KrafftSieve.q n))

theorem KrafftSieve.sum_W_eq_S1 (n : ℕ) (hn : n ≥ 1) (W : ZMod (q n) → ℝ) (h_supp : ∀ (x : ZMod (q n)), x.val ∉ evalInterval n → W x = 0) : ∑ x : ZMod (q n), W x = sum1 n W

Given the compact support of $W$ in $\mathcal{A}_n$, the sum of $W(x)$ over $\mathbb{Z}/q\mathbb{Z}$ is equal to $sum1(n, W)$.

theorem KrafftSieve.compact_support_equivalence (n : ℕ) (hn : n ≥ 1) (W : ZMod (q n) → ℝ) (h_supp : ∀ (x : ZMod (q n)), x.val ∉ evalInterval n → W x = 0) : sum1 n W = ↑(q n) * (wHat n W 0).re

Compact Support Equivalence

Assume the weight function is strictly supported inside the interval: $\forall x \notin \mathcal{A}_n, W(x) = 0$. Prove that the interval sum $sum1(n, W)$ is equivalent to the full space sum, which yields the zero-frequency Fourier coefficient: $$ sum1(n, W) = \sum_{x \in \mathbb{Z}/q\mathbb{Z}} W(x) = q \hat{W}(0) $$

theorem KrafftSieve.plancherel_theorem_custom (n : ℕ) (f g : ZMod (q n) → ℂ) : ∑ x : ZMod (q n), f x * (starRingEnd ℂ) (g x) = ↑(q n) * ∑ h : ZMod (q n), (1 / ↑(q n) * ∑ x : ZMod (q n), f x * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑(h.val * x.val) / ↑(q n))) * (starRingEnd ℂ) (1 / ↑(q n) * ∑ x : ZMod (q n), g x * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑(h.val * x.val) / ↑(q n)))

Plancherel's Theorem for the custom Fourier transform definition: $$ \sum_{x} f(x) \overline{g(x)} = q \sum_{h} \hat{f}(h) \overline{\hat{g}(h)} $$

theorem KrafftSieve.plancherel_hit_expansion (n : ℕ) (hn : n ≥ 1) (W : ZMod (q n) → ℝ) (h_supp : ∀ (x : ZMod (q n)), x.val ∉ evalInterval n → W x = 0) : ↑(sum2 n W) = ↑(q n) * ∑ i : Fin (w n), ∑ h : ZMod (q n), wHat n W h * (starRingEnd ℂ) (gHat n i h)

The Plancherel Hit Expansion Using the compact support of $W(x)$ and admitting Plancherel's theorem for the inner product of $W(x)$ and $g_i(x)$, expand the weighted hit count $sum2(n)$ into the Fourier domain: $$ sum2(n) = q \sum_{i=1}^w \sum_{h=0}^{q-1} \hat{W}(h) \overline{\hat{g}_i(h)} $$

theorem KrafftSieve.dirac_comb_nonzero (n : ℕ) (i : Fin (w n)) (k : Fin (p n i)) : gHat n i ↑(↑k * (q n / p n i)) = ↑2 / ↑↑(p n i) * ↑(Real.cos (2 * Real.pi * ↑↑k * ↑(krafftResidue n i) / ↑(p n i)))

theorem KrafftSieve.dirac_comb_zero (n : ℕ) (i : Fin (w n)) (h : ZMod (q n)) (h_not_multiple : ∀ (k : Fin (p n i)), h ≠ ↑(↑k * (q n / p n i))) : gHat n i h = 0

theorem KrafftSieve.resonant_sieve_equation (n : ℕ) (hn : n ≥ 1) (W : ZMod (q n) → ℝ) (h_supp : ∀ (x : ZMod (q n)), x.val ∉ evalInterval n → W x = 0) : ↑(sum2 n W) = ↑(sum1 n W) * ∑ i : Fin (w n), ↑2 / ↑↑(p n i) + ↑(q n) * ∑ i : Fin (w n), ∑ k ∈ (Finset.range (p n i)).erase 0, wHat n W ↑(k * (q n / p n i)) * (↑2 / ↑↑(p n i) * ↑(Real.cos (2 * Real.pi * ↑k * ↑(krafftResidue n i) / ↑(p n i))))

theorem KrafftSieve.exact_krafft_cosine (n : ℕ) (i : Fin (w n)) : Real.cos (2 * Real.pi * 3 * ↑(krafftResidue n i) / ↑(p n i)) = -Real.cos (Real.pi / ↑(p n i))

The Exact Krafft Cosine

Using the definition $r^K_i = \lfloor(p_i+1)/6\rfloor$, admit that for all primes $p_i \ge 5$, the cosine at the third harmonic evaluates exactly to the negative cosine of a microscopic angle: $$ \cos\left( \frac{2\pi \cdot 3 \cdot r^K_i}{p_i} \right) = -\cos\left( \frac{\pi}{p_i} \right) $$

theorem KrafftSieve.third_harmonic_extraction (n : ℕ) (hn : n ≥ 1) (W : ZMod (q n) → ℝ) (h_supp : ∀ (x : ZMod (q n)), x.val ∉ evalInterval n → W x = 0) (h_spectral : ∀ (i : Fin (w n)), ∀ k ∈ (Finset.range (p n i)).erase 0, k ≠ 3 → wHat n W ↑(k * (q n / p n i)) = 0) : ↑(sum2 n W) = ↑(sum1 n W) * ∑ i : Fin (w n), ↑2 / ↑↑(p n i) - ↑(q n) * ∑ i : Fin (w n), wHat n W ↑(3 * (q n / p n i)) * (↑2 / ↑↑(p n i) * ↑(Real.cos (Real.pi / ↑(p n i))))

The Third Harmonic Extraction

Admit that for a strategically chosen weight function $W(x)$ where $\hat{W}(h)$ is concentrated strictly at $h=0$ and the third harmonics $h = 3q/p_i$, the Resonant Sieve Equation simplifies to: $$ sum2(n, W) = sum1(n, W) \sum_{i=1}^w \frac{2}{p_i} - q \sum_{i=1}^w \hat{W}\left(3 \frac{q}{p_i}\right) \frac{2}{p_i} \cos\left( \frac{\pi}{p_i} \right) $$

noncomputable def KrafftSieve.hSpec (n : ℕ) : ℝ

Sum of reciprocals of primes in the sieve window

Equations

• KrafftSieve.hSpec n = ∑ p ∈ KrafftSieve.primeWindow n, 1 / ↑p

noncomputable def KrafftSieve.mainTerm (n : ℕ) : ℝ

The main term of the sieve: 2H(n)

Equations

• KrafftSieve.mainTerm n = 2 * KrafftSieve.hSpec n

noncomputable def KrafftSieve.resonanceStrength (p : ℕ) : ℝ

The resonance strength for a single prime p: cos(π/p)

Equations

• KrafftSieve.resonanceStrength p = Real.cos (Real.pi / ↑p)

noncomputable def KrafftSieve.resonanceCapacity (n : ℕ) : ℝ

The total resonance capacity: Σ (2/p)·cos(π/p)

Equations

• KrafftSieve.resonanceCapacity n = ∑ p ∈ KrafftSieve.primeWindow n, 2 / ↑p * KrafftSieve.resonanceStrength p

theorem KrafftSieve.resonance_lt_mainTerm (n : ℕ) (hn : primeWindow n ≠ ∅) : resonanceCapacity n < mainTerm n

The Harmonic Deficit (Parity Barrier Collision) The resonance capacity of any purely one-dimensional 3rd harmonic weight system is strictly overpowered by the sieve aggregate main density. This formalizes the collision with the Sieve Parity limit.