Suzuki Lemma 14.3 at the natural-ceiling cutoff

For z = ⌈D^(1/s)⌉₊, the strict condition p < z is transported exactly to p < D^(1/s). This makes every source carrier through layer ⌊s-2⌋₊ empty, without the generally false surrogate inequality z^M ≤ D.

theorem MathlibNt.SieveTheory.suzukiSourceLowerCarrier_rpow_eq_empty (S : BoundingSieve) {n D : ℕ} {s : ℝ} (hD : 1 < D) (hs : 0 < s) (hns : ↑n + 2 ≤ s) : {p ∈ suzukiSupportedBelowPowerReal S (↑D ^ (1 / s)) | D ≤ p ^ (n + 2)} = ∅

The lower-cutoff carrier is literally empty at the real power cutoff. This is the strict-carrier replacement for a ceiling-power inequality.

theorem MathlibNt.SieveTheory.suzukiSourceOuterCarrier_rpow_eq_empty (S : BoundingSieve) {n D : ℕ} {s : ℝ} (hD : 1 < D) (hs : 0 < s) (hns : ↑n + 2 ≤ s) : suzukiSourceOuterCarrierPowerReal n D (↑D ^ (1 / s)) S.prodPrimes.primeFactors = ∅

Consequently the complete source outer carrier is empty. The proof uses its exact strict real-cutoff presentation, not finite-support exhaustion.

theorem MathlibNt.SieveTheory.suzukiSourceV_eq_zero_below_natCeil_rpow (S : BoundingSieve) {n D z : ℕ} {s : ℝ} (hD : 1 < D) (hs : 2 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) (hn : n ≤ ⌊s - 2⌋₊) : suzukiSourceV S n D z = 0

Actual source layers through ⌊s-2⌋₊ vanish for the natural-ceiling choice z = ⌈D^(1/s)⌉₊.

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

Lemma 14.3 with both former abstract inputs discharged: support comes from strict natural-ceiling carrier equality and the pointwise majorant is the proved Lemma 14.1 factorial bound. The right side is independent of N.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_natCeil_uniform_tsum (S : BoundingSieve) {N D z : ℕ} {s : ℝ} (hD : 1 < D) (hs : 2 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : suzukiActualT S N D z ≤ ∑' (n : ℕ), if ⌊s - 2⌋₊ + 1 ≤ n then (∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p) ^ n / ↑n.factorial else 0

Explicit tsum form of the same N-uniform conclusion.