theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.derivativeDDECertificateOnSource_of_singleQhatMajorant
{H : Section13HatLayers}
(hH : Section13HatSourceContract H)
{d : ℝ}
(hd : 0 < d)
(Q : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H))
:
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.