Suzuki (14.9) with the strict natural-ceiling carrier

The odd-depth recurrence needs only the source condition p^3 < D for the actual summation indices p < z. It does not need the generally false natural-ceiling surrogate z^3 ≤ D.

theorem MathlibNt.SieveTheory.suzukiSourceV_one_eq_zero_of_cube_lt_below (S : BoundingSieve) {D z : ℕ} (hCube : ∀ p < z, p ^ 3 < D) : suzukiSourceV S 1 D z = 0

The depth-one source layer vanishes when every natural below the strict cutoff satisfies the cubic source bound.

theorem MathlibNt.SieveTheory.suzukiSourceV_succ_eq_unrestricted_strict (S : BoundingSieve) {n D z : ℕ} (hn : 0 < n) (hOddCarrier : Odd (n + 1) → ∀ p < z, p ^ 3 < D) : suzukiSourceV S (n + 1) D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

The exact successor recurrence after erasing the lower source cutoff. At odd depth its upper cutoff is automatic from the strict carrier condition on the indices actually present in the sum.

theorem MathlibNt.SieveTheory.suzukiActualT_caseI_recurrence_strict (S : BoundingSieve) {N D z : ℕ} (hN : 2 ≤ N) (hOddCarrier : Odd N → ∀ p < z, p ^ 3 < D) : suzukiActualT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiActualT S (N - 1) (D ⌈/⌉ p) p

Case I's actual finite recurrence under the source-faithful odd condition. The strict inequality is required only for indices p < z.

theorem MathlibNt.SieveTheory.suzuki_equation14_9_strict (S : BoundingSieve) {N D z : ℕ} (hN : 2 ≤ N) (hOddCarrier : Odd N → ∀ p < z, p ^ 3 < D) {a b : ℝ} (hab : a ≤ b) : suzukiActualT S N D z = suzukiSigmaZero S N D z a + suzukiSigmaOne S N D z a b + suzukiSigmaTwo S N D z b

Equation (14.9) with the exact strict odd carrier hypothesis.

theorem MathlibNt.SieveTheory.cube_lt_of_lt_natCeil_rpow {D z p : ℕ} {s : ℝ} (hD : 0 < D) (hs : 3 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) (hpz : p < z) : p ^ 3 < D

A natural ceiling of D^(1/s) with s ≥ 3 supplies exactly the strict cubic carrier needed by the odd recurrence.

theorem MathlibNt.SieveTheory.suzukiActualT_caseI_recurrence_natCeil (S : BoundingSieve) {N D z : ℕ} {s : ℝ} (hN : 2 ≤ N) (hD : 0 < D) (hs : 3 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : suzukiActualT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiActualT S (N - 1) (D ⌈/⌉ p) p

Natural-ceiling specialization of the actual recurrence.

theorem MathlibNt.SieveTheory.suzuki_equation14_9_natCeil (S : BoundingSieve) {N D z : ℕ} {s : ℝ} (hN : 2 ≤ N) (hD : 0 < D) (hs : 3 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) {a b : ℝ} (hab : a ≤ b) : suzukiActualT S N D z = suzukiSigmaZero S N D z a + suzukiSigmaOne S N D z a b + suzukiSigmaTwo S N D z b

Natural-ceiling specialization of Suzuki's decomposition (14.9).