noncomputable def MathlibNt.SieveTheory.lowerSuzukiDiscreteKernel (S : BoundingSieve) (D z k q : ℕ) : ℝ

The odd stored-chain mass which remains after Suzuki's terminal prime q is externalized. Pair depth k means stored length 2*k+1; after restoring q, the full source index is therefore 2*k+2. The strict filter is essential: q is not one of the stored primes.

Equations

• MathlibNt.SieveTheory.lowerSuzukiDiscreteKernel S D z k q = MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsFixedPairDepth0Density (⇑S.nu) D q ({p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z | q < p}) k

noncomputable def MathlibNt.SieveTheory.lowerSuzukiNormalizedLayer (S : BoundingSieve) (D w z k : ℕ) : ℝ

The finite normalized lower layer corresponding to Suzuki's V_{2k+2}(D,z)/V(z). The terminal prime is external: its contribution is the Suzuki atom ν(q) V(q)/V(z), while the odd chain behind it is the kernel.

Equations

• MathlibNt.SieveTheory.lowerSuzukiNormalizedLayer S D w z k = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeSumNat S w z (MathlibNt.SieveTheory.lowerSuzukiDiscreteKernel S D z k)

theorem MathlibNt.SieveTheory.lowerSuzukiDiscreteKernel_sourceIndex (S : BoundingSieve) (D z k q : ℕ) : lowerSuzukiDiscreteKernel S D z k q = ∑ l ∈ LinearSieve.lowerRosserBoundaryChainsAtSourceIndex D q ({p ∈ SwitchingPrinciple.suzukiSupportedBelow S z | q < p}) (2 * k + 2), (List.map (⇑S.nu) l).prod

The source index attached to pair depth k is exactly 2*k+2.

theorem MathlibNt.SieveTheory.lowerSuzukiNormalizedLayer_eq_primeSum (S : BoundingSieve) (D w z k : ℕ) : lowerSuzukiNormalizedLayer S D w z k = ∑ q ∈ SwitchingPrinciple.suzukiSupportedBelow S z with w ≤ q, S.nu q * SwitchingPrinciple.suzukiSuffixRatio S z q * lowerSuzukiDiscreteKernel S D z k q

Exact terminal-prime externalization. This is Suzuki's finite prime sum, not merely an upper bound or an asymptotic identification.

theorem MathlibNt.SieveTheory.lowerSuzuki_terminalFactor (S : BoundingSieve) {z q : ℕ} (hq : q ∈ SwitchingPrinciple.suzukiSupportedBelow S z) : S.nu q * SwitchingPrinciple.suzukiSuffixRatio S z q = S.nu q / (1 - S.nu q) * SwitchingPrinciple.suzukiSuffixRatio S z (q + 1)

Pointwise form of terminal externalization: the terminal q is removed from the stored odd chain and contributes its odds factor; the remaining Euler ratio starts strictly after q.

theorem MathlibNt.SieveTheory.lowerSuzukiNormalizedLayer_terminalExternalized (S : BoundingSieve) (D w z k : ℕ) : lowerSuzukiNormalizedLayer S D w z k = ∑ q ∈ SwitchingPrinciple.suzukiSupportedBelow S z with w ≤ q, S.nu q / (1 - S.nu q) * SwitchingPrinciple.suzukiSuffixRatio S z (q + 1) * lowerSuzukiDiscreteKernel S D z k q

The normalized layer with terminal q visibly externalized.

theorem MathlibNt.SieveTheory.lowerSuzukiDiscreteKernel_succ (S : BoundingSieve) {D z q : ℕ} (hq : q ∈ SwitchingPrinciple.suzukiSupportedBelow S z) (k : ℕ) : lowerSuzukiDiscreteKernel S D z (k + 1) q = ∑ p₀ ∈ SwitchingPrinciple.suzukiSupportedBelow S z with q < p₀, ∑ p₁ ∈ {p ∈ SwitchingPrinciple.suzukiSupportedBelow S z | q < p} with p₁ < p₀ ∧ p₀ * p₁ ^ 3 < D, S.nu p₀ * S.nu p₁ * lowerSuzukiDiscreteKernel S (D ⌈/⌉ (p₀ * p₁)) p₁ k q

Exact one-pair recurrence for the discrete kernel. No analytic assumption is used. Notice that the residual cutoff is p₁, not z; this is the finite carrier refinement hidden by continuous notation.

theorem MathlibNt.SieveTheory.lowerSuzukiNormalizedLayer_eq_lemmaEightSixPrimeSum (S : BoundingSieve) (Dreal : ℝ) (D w z k : ℕ) (H : ℝ → ℝ) (hH : ∀ q ∈ {q ∈ SwitchingPrinciple.suzukiSupportedBelow S z | w ≤ q}, H (Real.log Dreal / Real.log ↑q) = lowerSuzukiDiscreteKernel S D z k q) : lowerSuzukiNormalizedLayer S D w z k = SwitchingPrinciple.suzukiLemmaEightSixPrimeSum S Dreal (↑w) (↑z) H

Bridge to the already proved real-cutoff Suzuki Lemma 8.6 prime sum. The sole compatibility premise says that the real test function interpolates the finite Rosser kernel at supported prime coordinates.

theorem MathlibNt.SieveTheory.lowerSuzukiNormalizedLayer_le (S : BoundingSieve) (Dreal : ℝ) (D w z k : ℕ) {s σ K : ℝ} {H : ℝ → ℝ} (hD : 1 < Dreal) (hw2 : 2 ≤ ↑w) (hs : 0 < s) (hsσ : s ≤ σ) (hz : ↑z = Dreal ^ (1 / s)) (hw : ↑w = Dreal ^ (1 / σ)) (hHcont : Continuous H) (hH0 : ∀ t ∈ Set.Icc s σ, 0 ≤ H t) (hHt : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc s σ)) (hK : 0 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hinterp : ∀ q ∈ {q ∈ SwitchingPrinciple.suzukiSupportedBelow S z | w ≤ q}, H (Real.log Dreal / Real.log ↑q) = lowerSuzukiDiscreteKernel S D z k q) : lowerSuzukiNormalizedLayer S D w z k ≤ (1 / s * ∫ (t : ℝ) in s..σ, H t) + 2 * K * H s / Real.log ↑w

Direct application of the proved dimension-one Suzuki lemma to the exact finite lower layer. All hypotheses are inherited from that lemma, except for the explicit interpolation condition identifying H with the discrete Rosser kernel on the finite prime carrier.