theorem MathlibNt.SieveTheory.roundedBaseOne_cube_carrier_iff (D p : ℕ) : D ≤ p ^ 3 ↔ ↑D ^ (1 / 3) ≤ ↑p

The integral cubic source condition is the real cubic-root lower cutoff.

theorem MathlibNt.SieveTheory.roundedBaseOne_V_mul_localRatio_eq_sourceEuler (S : BoundingSieve) {p : ℕ} {x : ℝ} (hpx : ↑p < x) : SwitchingPrinciple.suzukiVProduct S x * SwitchingPrinciple.suzukiLocalRatio S (↑p) x = sourceDiscreteEuler S p

The strict Euler suffix identity needed to identify the source summands with the summands in the real-cutoff Suzuki V₁.

theorem MathlibNt.SieveTheory.roundedBaseOne_sourceV_one_eq_realVOne (S : BoundingSieve) {D z : ℕ} {x : ℝ} (hz : z = ⌈x⌉₊) : suzukiSourceV S 1 D z = SwitchingPrinciple.suzukiVOne S (↑D) 2 x

Exact strict-carrier bridge from source V₁ at a natural ceiling to Suzuki's unnormalized real-cutoff V₁.

theorem MathlibNt.SieveTheory.roundedBaseOne_V_natCeil_eq_real (S : BoundingSieve) {x : ℝ} {z : ℕ} (hz : z = ⌈x⌉₊) : SwitchingPrinciple.suzukiVProduct S ↑z = SwitchingPrinciple.suzukiVProduct S x

Strict real cutoffs are unchanged by replacing the cutoff by its natural ceiling, even though the cast ceiling is generally not the real cutoff.

theorem MathlibNt.SieveTheory.suzukiSourceV_one_le_V_natCeil_mul_fOne_add_localError {S : BoundingSieve} {D z : ℕ} {s K : ℝ} (hz : z = ⌈↑D ^ (1 / s)⌉₊) (hD : 1 < ↑D) (hs : 0 < s) (hs3 : s ≤ 3) (hroot2 : 2 ≤ ↑D ^ (1 / s)) (hK : 0 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : suzukiSourceV S 1 D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + 9 * K / (s * Real.log ↑D))

Sharp source-native base-one estimate at z = ceil(D^(1/s)). All cutoff transport is by equality of strict finite carriers; no cast-ceiling/root equality and no cutoff error are used.