theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope_shift_one_le {D d u σ : ℝ} (hlog : 0 < Real.log D) (hd : 0 ≤ d) (hu : 0 ≤ u) (huσ : u ≤ σ) : perturbationSlope D d 1 u ≤ (1 + σ * d) * (σ + 1) ^ d / Real.log D

The slope estimate needed on Suzuki's T4 interval. Unlike the high-range version, the shifted argument u = t - 1 need only be nonnegative; the base u + 1 is still at least one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_mul_eq_short_minus {H : Section13HatLayers} {β D d Δ t : ℝ} (hH : Section13HatContract H β) (ht : 1 < t) (htop : t ≤ β + 2) : qD H ErrorSign.plus D d Δ t * t = (β - 1) * perturbation D d 1 (t - 1) * (t / (t - 1)) ^ (1 + Δ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_mul_eq_at_plus_boundary {H : Section13HatLayers} {β D d Δ : ℝ} (hH : Section13HatContract H β) : qD H ErrorSign.minus D d Δ (β + 1) * (β + 1) = β * perturbation D d 1 β * ((β + 1) / β) ^ (1 + Δ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_mul_antitoneOn_short_minus {H : Section13HatLayers} {β D d Δ τ σ ρ : ℝ} (hH : Section13HatContract H β) (hd : 0 ≤ d) (_hΔ : -1 ≤ Δ) (hρ : 0 < ρ) (hlog : 0 < Real.log D) (hDlarge : (1 + σ * d) * (σ + 1) ^ d ≤ ρ * Real.log D) (hτlower : β ≤ τ) (hτupper : τ ≤ β + 2) (hτσ : τ ≤ σ) (hshort : ρ * (σ * (σ - 1)) ≤ 1 + Δ) : AntitoneOn (fun (t : ℝ) => qD H ErrorSign.plus D d Δ t * t) (Set.Ioc β τ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_ii_of_log_bound {H : Section13HatLayers} {β D d Δ σ ρ : ℝ} (hH : Section13HatContract H β) (hd : 0 ≤ d) (hΔ : -1 ≤ Δ) (hσ : ∀ (sign : ErrorSign), β + sign.epsilon ≤ σ) (hρ : 0 < ρ) (hlog : 0 < Real.log D) (hDlarge : (1 + σ * d) * (σ + 1) ^ d ≤ ρ * Real.log D) (hdelay : ∀ (sign : ErrorSign) (t : ℝ), β + sign.epsilon < t → t ≤ σ → ρ * weightedHat H sign t ≤ t * H.T sign.opposite (t - 1)) (hshort : ρ * (σ * (σ - 1)) ≤ 1 + Δ) : Claim14_6_MonotoneQPremise H D d Δ σ

Full quantitative Claim 14.6(ii). The minus outer-sign branch is split at β + 2: T4 gives the lower piece and shifted Claim 14.6(i) gives the upper piece. For the plus outer sign, the shifted high-range argument starts immediately above β + 1.