Paying source-fixed pointwise thresholds

This is the common no-eventual bridge used by the strict Case-I moving producer. A cutoff selected from the source data before K is absorbed into the separator C1 * K ^ Θ < log D; no cutoff is selected after K.

theorem MathlibNt.SieveTheory.exists_sourceLargeLog_fixedThreshold {Θ : ℝ} (hΘ : 0 < Θ) (D0 : ℝ) (hD0 : 0 < D0) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 K D : ℝ), C1min ≤ C1 → 2 ≤ K → 0 < D → C1 * K ^ Θ < Real.log D → D0 < D

A positive fixed real cutoff can be paid by an earlier source-separator constant. The conclusion is strict, matching the strict source separator.

theorem MathlibNt.SieveTheory.exists_sourceLargeLog_fixedThreshold_of_source {d Δ Θ : ℝ} (hsrc : SuzukiClaim145SourceParameters d Δ Θ) (D0 : ℝ) (hD0 : 0 < D0) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 K D : ℝ), C1min ≤ C1 → 2 ≤ K → 0 < D → C1 * K ^ Θ < Real.log D → D0 < D

Source-packet specialization. This is the form consumed by strict Case I; its only exponent premise is the literal source packet.