theorem MathlibNt.SieveTheory.exists_lemma14_4_literal_allDepth_with_lowStrip_extension (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (N : ℕ), 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

Literal all-depth, cutoff-two Suzuki bound under the printed source parameters, with the omitted source-small odd strip supplied by the separately named low-strip extension. All constants precede K, depth, D, and s.