noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (D d : ℝ) : ℝ

Suzuki's source cutoff from Claim 14.5 (p.82): σ(D) = (log D)^(1/d) log(log(27D)).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d = Real.log D ^ (1 / d) * Real.log (Real.log (27 * D))

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

In the source range 0 < Δ < 1, the hypothesis d > 7 / (1 - Δ) leaves a genuine exponent gap.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_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 * Real.log D ^ (Δ - 1) ≤ (1 - Δ) / (16 * sourceSigma D d)

A source-faithful positive-Δ endpoint decay theorem. For every fixed nonnegative coefficient A, the exact source cutoff sourceSigma D d is absorbed eventually. The threshold is built only from exp, max, and real powers; no D-dependent inequality is left among the premises.