theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.rpow_contraction_gap {Δ σ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hσ : 1 < σ) : (1 - Δ) / σ ≤ 1 - (1 - 1 / σ) ^ (1 - Δ)

The real-power source bracket loses at least its linear tangent gap. This is the weighted AM--GM (equivalently, concavity/Bernoulli) inequality.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma_gt_one_of_large {D d : ℝ} (hd : 0 < d) (hD : Real.exp (Real.exp 1) ≤ D) : 1 < sourceSigma D d

For every positive source exponent parameter, Suzuki's exact cutoff is strictly larger than one beyond the explicit threshold exp (exp 1).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_gt_one_threshold {Δ d : ℝ} (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 1 < sourceSigma D d

Eventual σ(D) > 1 in the source parameter range, with an explicit threshold and no size-dependent premise.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_contraction_gap_threshold (Δ d : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → (1 - Δ) / sourceSigma D d ≤ 1 - (1 - 1 / sourceSigma D d) ^ (1 - Δ)

At Suzuki's exact source cutoff, the source bracket contraction gap is at least (1-Δ)/sourceSigma D d for all sufficiently large D.