theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_derivativeDDE_largeRange_of_section13HatSourceContract {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d : ℝ} (hd : 0 < d) (Q : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)) : ∃ (M : ℝ) (D₀ : ℝ), 1 < M ∧ 4 ≤ M ∧ 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ sourceSigma D d ∧ ∀ (sign : ErrorSign) (ε t : ℝ), ε = 0 ∨ ε = 1 → M ≤ t → t ≤ sourceSigma D d → weightedHat H sign t * perturbationSlope D d ε t ≤ t * H.T sign.opposite (t - 1)

A single Qhat cutoff majorant and Proposition 13.1's delayed/current ratio absorb the logarithmic derivatives for both ε = 0 and ε = 1, uniformly on the moving source range. The proof splits at (log D)^(1/d) and keeps the source upper bound in both branches.