Source-correct moving closure of Claims 14.6(i) and (ii)

The old MovingClaim14_6TailCertificate is not used: its single ρ D must simultaneously dominate a slope bound growing with the moving endpoint and be O(sourceSigma⁻²). The corrected interface records the actual pointwise DDE comparison, before monotonicity is deduced. The short T4 interval is handled at the fixed endpoint 4, so no incompatible moving-σ condition is introduced.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDerivativeDDECertificateOnSource (H : Section13HatLayers) (d : ℝ) : Prop

Source-correct pointwise input for the two moving monotonicity claims. It is a derivative/DDE comparison, not either monotonicity conclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDerivativeDDECertificateOnSource H d = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → 4 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (ε t : ℝ), ε = 0 ∨ ε = 1 → 2 + sign.epsilon < t → t < MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbationSlope D d ε t ≤ t * H.T sign.opposite (t - 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_claim14_6_i_ii_at_sourceSigma_of_derivativeDDE {H : Section13HatLayers} (hH : Section13HatContract H 2) {d Δ : ℝ} (hd1 : 1 < d) (hΔ : -1 < Δ) (hcert : MovingDerivativeDDECertificateOnSource H d) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → Claim14_6_MonotoneLambdaPremise H D d (sourceSigma D d) ∧ Claim14_6_MonotoneQPremise H D d Δ (sourceSigma D d)

The corrected source certificate closes both Claims with the required ∃ D₀, ∀ D ≥ D₀ quantifier order. The only extra threshold is elementary: it makes the perturbation slope small on the fixed T4 interval [2,4].

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_unshifted_derivativeDDE_of_cutoffMajorants {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d : ℝ} (hd : 0 < d) (majorant : (sign : ErrorSign) → CutoffCorrectedRatio.CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat) : ∃ (M : ℝ) (D₀ : ℝ), 1 < M ∧ 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ sourceSigma D d ∧ ∀ (sign : ErrorSign) (t : ℝ), M ≤ t → t ≤ sourceSigma D d → weightedHat H sign t * perturbationSlope D d 0 t ≤ t * H.T sign.opposite (t - 1)

The proved Section-13 cutoff majorant supplies the unshifted (ε=0) half of the corrected pointwise certificate through Proposition 13.1's moving ratio. The shifted half remains explicit in the corrected interface rather than being hidden in an impossible scalar ρ.