Moving-source closure audit for Claims 14.6(i) and (ii)

The fixed-σ theorem has quantifiers ∀ σ, ∃ D₀(σ), ∀ D ≥ D₀(σ) and therefore cannot be specialized diagonally to σ = sourceSigma D d. The results below state and prove the strongest source-faithful uniform reductions available from the production API.

For (i), the exact derivative bracket is exposed. For (ii), the residual is a uniform moving-tail/DDE margin ρ D, including the short-interval inequality; this is exactly what claim14_6_ii_of_log_bound consumes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_i_of_explicit_derivative_domination {H : Section13HatLayers} {β D d σ : ℝ} (hH : Section13HatContract H β) (hlog : 0 < Real.log D) (hdom : ∀ (sign : ErrorSign) (ε t : ℝ), ε = 0 ∨ ε = 1 → β + sign.epsilon < t → t < σ → weightedHat H sign t * perturbationSlope D d ε t ≤ t * H.T sign.opposite (t - 1)) : Claim14_6_MonotoneLambdaPremise H D d σ

Exact pointwise derivative domination sufficient for Claim 14.6(i) on one interval. Unlike the fixed-σ compactness proof, this statement is suitable for a moving upper endpoint: no threshold depending on that endpoint is chosen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_claim14_6_i_at_sourceSigma_of_derivative_domination {H : Section13HatLayers} {β d : ℝ} (hH : Section13HatContract H β) (hd1 : 1 < d) (hdom : ∃ (Da : ℝ), 1 < Da ∧ ∀ (D : ℝ), Da ≤ D → ∀ (sign : ErrorSign) (ε t : ℝ), ε = 0 ∨ ε = 1 → β + sign.epsilon < t → t < sourceSigma D d → weightedHat H sign t * perturbationSlope D d ε t ≤ t * H.T sign.opposite (t - 1)) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 3 ≤ sourceSigma D d ∧ Claim14_6_MonotoneLambdaPremise H D d (sourceSigma D d)

Uniform moving-source closure of Claim 14.6(i) from its explicit derivative condition. sourceSigma growth is used to put both signs' left endpoints below the moving endpoint.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingClaim14_6TailCertificate (H : Section13HatLayers) (β d Δ : ℝ) : Prop

WITHDRAWN / source-incompatible for moving sourceSigma. The second and fourth fields force asymptotically incompatible lower and upper bounds on ρ D (see CLAIM146_I_II_SOURCE_AUDIT.md). Retained only so older conditional lemmas continue to elaborate; do not use in the production chain.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingClaim14_6TailCertificate H β d Δ = ∃ (D0 : ℝ), 1 < D0 ∧ ∃ (ρ : ℝ → ℝ), ∀ (D : ℝ), D0 ≤ D → 0 < ρ D ∧ (1 + MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d * d) * (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d + 1) ^ d ≤ ρ D * Real.log D ∧ (∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (t : ℝ), β + sign.epsilon < t → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → ρ D * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t ≤ t * H.T sign.opposite (t - 1)) ∧ ρ D * (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d * (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d - 1)) ≤ 1 + Δ

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

Moving-source Claims 14.6(i)/(ii) close uniformly from the exact tail/DDE certificate above. This theorem is source-faithful: all dependence on the moving endpoint remains inside one ∀ D ≥ D0 statement.