theorem MathlibNt.SieveTheory.lowerRosser_depthFour_terminal_forces_source_cutoffs {D p₀ p₁ p₂ q : ℕ} (h10 : p₁ < p₀) (h21 : p₂ < p₁) (hq2 : q < p₂) (hterminal : D ≤ p₀ * p₁ * p₂ * q ^ 3) : D ≤ p₀ ^ 6 ∧ D ≤ p₀ * p₁ ^ 5 ∧ D ≤ p₀ * p₁ * p₂ ^ 4

The three lower cutoffs appearing in Suzuki's depth-four recursion are forced by the terminal lower-Rosser boundary crossing. This is the first nontrivial layer after depth two: no source cutoff is silently discarded.

theorem MathlibNt.SieveTheory.suzuki_depthFour_cutoffs_iff_lowerRosser_cutoffs {D p₀ p₁ p₂ q : ℕ} (h10 : p₁ < p₀) (h21 : p₂ < p₁) (hq2 : q < p₂) : D ≤ p₀ ^ 6 ∧ D ≤ p₀ * p₁ ^ 5 ∧ p₀ * p₁ ^ 3 < D ∧ D ≤ p₀ * p₁ * p₂ ^ 4 ∧ D ≤ p₀ * p₁ * p₂ * q ^ 3 ↔ p₀ * p₁ ^ 3 < D ∧ D ≤ p₀ * p₁ * p₂ * q ^ 3

After clearing the exact natural ceiling quotients, Suzuki's depth-four recursive carrier is exactly the lower-Rosser carrier: the only independent interior condition is the first even-prefix test p₀*p₁^3 < D, and the final condition is the odd boundary crossing.