def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEAsymptoticCertificateOnSource (H : Section13HatLayers) (sign : ErrorSign) (d M : ℝ) : Prop

The minimal missing Proposition 13.1 input. It is pointwise and upstream of integration: on each of the two source ranges it says that the perturbation slope is absorbed by the delayed/current DDE ratio.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEAsymptoticCertificateOnSource H sign d M = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ (∀ (t : ℝ), M ≤ t → t ≤ Real.log D ^ (1 / d) → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope D d 0 t ≤ t * H.T sign.opposite (t - 1) * (t ^ d / Real.log D / (1 + t ^ d / Real.log D))) ∧ ∀ (t : ℝ), Real.log D ^ (1 / d) < t → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope D d 0 t ≤ t * H.T sign.opposite (t - 1) * (t ^ d / Real.log D / (1 + t ^ d / Real.log D))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_movingSigma_large_s_differential_tail_onSource {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d Δ t₀ : ℝ} (ht₀ : 2 < t₀) (hΔ : Δ < 1) (hcert : MovingDDEAsymptoticCertificateOnSource H sign d (t₀ + 2)) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → t₀ + 2 ≤ sourceSigma D d ∧ ∀ (s : ℝ), t₀ + 2 ≤ s → s ≤ sourceSigma D d → ∫ (t : ℝ) in s..sourceSigma D d, qD H sign.opposite D d Δ t ≤ (1 - 1 / sourceSigma D d) ^ (1 - Δ) * lambda H sign D d 0 s

The large-s moving tail from pp. 90--91. The split point is fixed as M=t₀+2; the conclusion is derived by differential domination and FTC, never assumed as a premise.

Source-range-corrected moving DDE certificate

Both source inputs and both certificate branches are quantified only up to sourceSigma D d. No global-in-t extension is used.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.movingDDEAsymptoticCertificateOnSource_of_proposition131_ratioOnSource {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d M : ℝ} (hratio : SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource H sign d M) : MovingDDEAsymptoticCertificateOnSource H sign d M

The source delayed/current ratio proves the moving differential certificate by splitting at (log D)^(1/d) exactly as on pp. 90--91.