theorem MathlibNt.SieveTheory.lowerRosserSetDensitySum_eq_euler_sub_suzukiActualT_all_supported (S : BoundingSieve) {D z : ℕ} (hD1 : 1 < D) (hzD : z ≤ D) : LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z) = sourceDiscreteEuler S z - suzukiActualT S (2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1)) D z

Once the even depth contains every supported pair-depth, the lower-Rosser density is exactly the finite Euler product minus Suzuki's actual parity sum. The depth depends on the finite carrier, but the identity has no limiting or fixed-depth approximation.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_exact_bound_of_suzuki_literal_allDepth (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (D : ℕ), 2 ≤ D → ∀ (s : ℝ), 2 ≤ s → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → have z := ⌈↑D ^ (1 / s)⌉₊; have N := 2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1); sourceDiscreteEuler S z - SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)) ≤ LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z)

Direct lower-Rosser density consequence of the literal all-depth Suzuki headline. The adaptive even depth is legal because the headline's constants are uniform over every natural depth. No discrepancy or depth limit remains.