theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.source_two_exponent_gap_pos {Δ d : ℝ} (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : 0 < 1 - Δ - 2 / d

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_sq_positive_delta_decay_threshold (Δ d A : ℝ) (_hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hA : 0 ≤ A) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → A * sourceSigma D d * Real.log D ^ (Δ - 1) ≤ (1 - Δ) / (32 * sourceSigma D d)

An explicit threshold absorbing the quadratic source-cutoff growth into (log D)^(Δ-1). In particular, the coefficient may itself be linear in sourceSigma D d; no D-dependent premise remains.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_sq_one_div_log_decay_threshold (Δ d A : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hA : 0 ≤ A) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → A * sourceSigma D d / Real.log D ≤ (1 - Δ) / (32 * sourceSigma D d)

The same explicit threshold also absorbs the 1 / log D endpoint scale.