theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_log_rpow_decay_threshold (Δ A σ : ℝ) (_hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hA : 0 ≤ A) (hσ : 1 < σ) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → A * Real.log D ^ (Δ - 1) ≤ (1 - Δ) / (8 * σ)

For fixed A, a positive power saving in log D is eventually absorbed by any fixed positive relative margin. The threshold is explicit (an exponential of a real power), so no uninstantiated "large D" hypothesis remains.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_one_div_log_relative_envelope (Δ A σ : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hA : 0 ≤ A) (hσ : 1 < σ) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → A / Real.log D ≤ (1 - Δ) / (8 * σ) * Real.log D ^ (-Δ)

Source-legal endpoint form: A / log D is factored as the relative coefficient A * (log D)^(Δ-1) times the source scale (log D)^(-Δ).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_log_rpow_decay_loglog_threshold (Δ A σ : ℝ) (_hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hA : 0 ≤ A) (hσ : 1 < σ) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → A * Real.log D ^ (Δ - 1) ≤ (1 - Δ) / (8 * σ * Real.log (Real.log D))

A source-style shrinking relative bracket: the fixed coefficient is ultimately O(1 / (σ * log log D)), with an explicit exponential threshold.