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

The unnormalised upper-Rosser boundary layer at pair depth k. The distinguished terminal prime is external to the stored even chain, so this is the odd Suzuki source layer 2*k+1. Its terminal factor is the Euler product strictly below q, not an inverse suffix product.

Equations

• MathlibNt.SieveTheory.upperSuzukiUnnormalizedLayer S D z k = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, S.nu q * MathlibNt.SieveTheory.sourceDiscreteEuler S q * MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (⇑S.nu) D q ({p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z | q < p}) k

theorem MathlibNt.SieveTheory.suzukiSourceV_odd_eq_upperSuzukiUnnormalizedLayer (S : BoundingSieve) (D z k : ℕ) (hD : 1 < D) : suzukiSourceV S (2 * k + 1) D z = upperSuzukiUnnormalizedLayer S D z k

Exact arbitrary-depth odd-layer bridge. Pair depth k in the production upper boundary has 2*k stored primes plus the external terminal prime, hence it is Suzuki source depth 2*k+1. The only base-domain hypothesis is 1 < D, needed because the empty stored chain must still be active.

theorem MathlibNt.SieveTheory.suzukiActualT_odd_eq_sum_upperSuzukiUnnormalizedLayers (S : BoundingSieve) (D z m : ℕ) (hD : 1 < D) : suzukiActualT S (2 * m + 1) D z = ∑ k ∈ Finset.range (m + 1), upperSuzukiUnnormalizedLayer S D z k

The actual odd Suzuki parity aggregate is the finite sum of the first m production upper-boundary pair layers.