theorem MathlibNt.SieveTheory.claim145_caseA_highS_sourceLarge_eventually {C1 Θ : ℝ} (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) : ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (D : ℕ) (s : ℝ), 2 ≤ D → 2 ≤ s → √K / Real.log K ≤ s → Real.log ↑D ≤ C1 * K ^ Θ → Real.exp 1 * suzukiSourceL (↑D) K ≤ s - 2

Uniform high-coordinate threshold ensuring that the ambient Lemma-14.3 source parameter lies in the decreasing floor-tail regime. This stronger ambient form is exactly what the scalar absorption theorem consumes; the natural-ceiling source is then smaller by suzukiSourceL_natCeil_rpow_le.