theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.derivativeDDECertificateOnSource_of_singleQhatMajorant {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d : ℝ} (hd : 0 < d) (Q : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)) : MovingDerivativeDDECertificateOnSource H d

The large source range supplied by Proposition 13.1 and the fixed compact head supplied by continuity/positivity merge into the corrected pointwise certificate. In particular, the certificate is produced here and is not an assumption of either Claim 14.6 or Case II.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_claim14_6_full_internal_at_sourceSigma {H : Section13HatLayers} {d Δ : ℝ} (hH : Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → Claim14_6_MonotoneLambdaPremise H D d (sourceSigma D d) ∧ Claim14_6_MonotoneQPremise H D d Δ (sourceSigma D d) ∧ ∀ (sign : ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ 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

All three moving clauses at the literal source endpoint. The same internally constructed scalar majorant feeds both the corrected (i),(ii) certificate and the already closed (iii) assembly.

theorem MathlibNt.SieveTheory.claim14_5_caseII_natEventual_of_internalClaim146 {Tdisc : ℕ → ℝ → ℝ → ℝ} {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {B₀ : ℕ → ℕ → ℝ} {N : ℕ} {d Δ σ K C C145 s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hN : Odd N) (hd1 : 1 < d) (hd : 7 / (1 - Δ) < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hs1 : 1 < s) (hs3 : s ≤ 3) (hC : 0 ≤ C) (hK : 0 ≤ K) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hscaleNonneg : ∀ (D : ℕ), 0 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)) (hassemble : MovingCaseIIRelativeAssembler Tdisc S H B₀ d Δ C K) (hnormalize : MovingCaseIINormalization S H B₀ d Δ σ K C C145) : Claim14_5NatEventualAt Tdisc S H N d Δ σ K s C145

Natural Case-II closure with Claims 14.6(i)--(iii) generated before the natural source parameter is introduced.

theorem MathlibNt.SieveTheory.claim14_5_natEventual_exact_case_split_with_internalClaim146_caseII {Tdisc : ℕ → ℝ → ℝ → ℝ} {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {B₀ : ℕ → ℕ → ℝ} {N : ℕ} {d Δ σ K C C145 D C1 ΘK s : ℝ} (hdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne 2 N) (hsσ : s ≤ σ) (hlarge : C1 * K ^ ΘK < Real.log D) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hd : 7 / (1 - Δ) < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 ≤ C) (hK : 0 ≤ K) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hscaleNonneg : ∀ (D : ℕ), 0 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)) (hassemble : MovingCaseIIRelativeAssembler Tdisc S H B₀ d Δ C K) (hnormalize : MovingCaseIINormalization S H B₀ d Δ σ K C C145) (hI : 2 + ↑(N % 2) ≤ s → s ≤ σ → Claim14_5NatEventualAt Tdisc S H N d Δ σ K s C145) : Claim14_5NatEventualAt Tdisc S H N d Δ σ K s C145

Exact Case-I/Case-II split with the full moving Claim 14.6 generated internally from the Section-13 source contract.