Case I: source-large-log uniform cutoff

The qualitative (14.23) scalar estimate was previously instantiated at fixed K, so its eventual threshold could still depend on K. The source has already chosen C1 before K and enters Case I only after C1 * K^Theta < log D. We spend the power 2 / Theta to absorb the exact K^2 coefficient and apply the source-scalar estimate with the strengthened exponent Delta + 2 / Theta. Thus the cutoff below is chosen before K, every depth and coordinate, and the later Claim-14.5 constant.

theorem MathlibNt.SieveTheory.exists_caseI1423_sourceScalar_sourceLargeLog_uniform {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΘ : 0 < Θ) (hmargin : Δ + 2 / Θ < 1) (hd : 7 / (1 - (Δ + 2 / Θ)) < d) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 K D : ℝ), C1min ≤ C1 → 2 ≤ K → 2 ≤ D → C1 * K ^ Θ < Real.log D → K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ^ 3 * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) * Real.log (Real.log D) / Real.log D ^ (1 - Δ) ≤ 1

Quantitative replacement for the fixed-K eventuality hidden in the old endpoint API. The hypotheses are precisely the strict exponent margin needed when the K^2 in (14.23) is paid by log D > C1*K^Theta.