theorem MathlibNt.SieveTheory.lowerRosserBoundaryAccum_supportedBelow_eq_sum_unnormalizedLayers (S : BoundingSieve) (D z : ℕ) : LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ (suzukiSupportedBelowList S z) = ∑ k ∈ Finset.range ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1), lowerSuzukiUnnormalizedLayer S D z k

The canonical lower-Rosser accumulator is exactly the finite sum of every unnormalized Suzuki pair-depth layer. There is no analytic or truncation premise: card + 1 is a complete finite-support cutoff.

theorem MathlibNt.SieveTheory.sourceDiscreteEuler_mul_suzukiSuffixRatio (S : BoundingSieve) {z q : ℕ} (hq : q ∈ SwitchingPrinciple.suzukiSupportedBelow S z) : sourceDiscreteEuler S z * SwitchingPrinciple.suzukiSuffixRatio S z q = sourceDiscreteEuler S q

The exact terminal-factor identity. Multiplication by the full Euler product converts the normalized suffix ratio into the Euler product strictly below the terminal prime.

theorem MathlibNt.SieveTheory.lowerSuzukiUnnormalizedLayer_eq_euler_mul_normalizedLayer (S : BoundingSieve) (D z k : ℕ) : lowerSuzukiUnnormalizedLayer S D z k = sourceDiscreteEuler S z * lowerSuzukiNormalizedLayer S D 0 z k

Exact normalization of each pair-depth layer. The coefficient is the full finite Euler product sourceDiscreteEuler S z; no suffix ratio is substituted for the accumulator's terminal factor.

theorem MathlibNt.SieveTheory.lowerRosserBoundaryAccum_supportedBelow_eq_euler_mul_sum_normalizedLayers (S : BoundingSieve) (D z : ℕ) : LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ (suzukiSupportedBelowList S z) = sourceDiscreteEuler S z * ∑ k ∈ Finset.range ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1), lowerSuzukiNormalizedLayer S D 0 z k

Hence the canonical accumulator is the full Euler product times the finite sum of normalized lower Suzuki layers.

theorem MathlibNt.SieveTheory.suzukiSourceV_even_eq_euler_mul_normalizedLayer (S : BoundingSieve) (D z k : ℕ) (hzD : z ≤ D) : suzukiSourceV S (2 * (k + 1)) D z = sourceDiscreteEuler S z * lowerSuzukiNormalizedLayer S D 0 z k

At every legal source level, each actual even Suzuki source layer is the Euler product times its normalized lower-boundary layer.

theorem MathlibNt.SieveTheory.suzukiActualT_even_eq_euler_mul_sum_normalizedLayers (S : BoundingSieve) (D z m : ℕ) (hzD : z ≤ D) : suzukiActualT S (2 * m) D z = sourceDiscreteEuler S z * ∑ k ∈ Finset.range m, lowerSuzukiNormalizedLayer S D 0 z k

Exact finite normalization identity for Suzuki's actual even parity sum.

theorem MathlibNt.SieveTheory.suzukiActualT_all_supported_depths_eq_lowerRosserBoundaryAccum (S : BoundingSieve) (D z : ℕ) (hzD : z ≤ D) : suzukiActualT S (2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1)) D z = LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ (suzukiSupportedBelowList S z)

Once all finite supported depths are included, the actual Suzuki parity sum is literally the canonical lower-Rosser accumulator.