theorem MathlibNt.SieveTheory.finiteSourceLayer_one_eq_zero_of_three_le {s : ℝ} (hs3 : 3 ≤ s) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s = 0

Above the initial strip, the depth-one continuous source layer vanishes.

theorem MathlibNt.SieveTheory.suzukiActualT_one_natCeil_eq_zero_of_three_lt (S : BoundingSieve) {D : ℕ} {s : ℝ} (hD : 1 ≤ D) (hs3 : 3 < s) : suzukiActualT S 1 D ⌈↑D ^ (1 / s)⌉₊ = 0

At a power cutoff with exponent strictly above three, the actual depth-one source is empty: every natural below the cutoff has cube strictly below D.

theorem MathlibNt.SieveTheory.lemma14_4_base_one_full_uniform {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ Lemma144UniformNatCeilAt S H C K d Δ 1 Dmin

The complete depth-one Lemma 14.4 base with one cutoff before every coordinate. The low strip uses the source-native rounded base estimate and a uniform absorption threshold; above 3, both the actual source and the finite continuous source layer vanish identically.