theorem
MathlibNt.SieveTheory.caseI_total_le_sigma0_add_sigma11_add_sigma12
(S : BoundingSieve)
(V : ℕ → ℝ)
(H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers)
{N D z : ℕ}
{β σ s C C1 K ΘK Δ d Vz B0 Bmid : ℝ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β)
(hN2 : 2 ≤ N)
(hbase : Odd N → suzukiSourceV S 1 D z = 0)
(hcube : ∀ n ∈ sourceParityIndices N, 2 ≤ n → Odd n → ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D)
(hdom : CaseIThreeRangeDomain D z σ s)
(hτ : caseITau (↑D) s = s)
(hz : ↑D ^ (1 / s) = ↑z)
(hcaseI : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI β N s σ)
(hEndpoint :
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime β (↑D) σ C1 K ΘK σ →
∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / σ)⌉₊,
S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p ≤ B0)
(hVz : Vz ≠ 0)
(hnu :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
0 ≤ S.nu p)
(hV :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
0 ≤ V p)
(hC : 0 ≤ C)
(hlog :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
0 ≤ Real.log ↑(D ⌈/⌉ p))
(hCeil :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
2 ≤ p ∧ 2 * p ≤ D)
(hSourceDomain :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1))
(hClaim :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H (↑(D ⌈/⌉ p)) d σ)
(hErrorDomain :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ Set.Icc (H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)).epsilon) σ ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ Set.Icc (H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)).epsilon) σ)
(hIH :
SwitchingPrinciple.SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract
(SwitchingPrinciple.suzukiSupportedBelow S z)
(fun (n D' p : ℕ) => ∑ m ∈ sourceParityIndices n, suzukiSourceV S m D' p) V
(fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) β C K Δ N D σ s)
(hMiddle87 :
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven (SwitchingPrinciple.suzukiSupportedBelow S z) (⇑S.nu) V Vz β
N D σ s + SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve (SwitchingPrinciple.suzukiSupportedBelow S z) (⇑S.nu) V
(fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) Vz C K Δ N D σ
s ≤ Bmid)
:
Production source-correct Case-I assembly of Σ₀ + Σ₁₁ + Σ₁₂ for the
Section-13 error envelope.
The source recurrence is supplied directly by
suzukiSourceParitySum_recurrence_caseI_two_ranges; the Σ₀ estimate is
transported directly from the explicit Claim-14.5 endpoint provider at s'=σ.
The recursive input is the literal natural-ceiling induction hypothesis and is
transported only through the proved ceiling bridge. The source-layer comparison
is derived from Proposition 9.3 using the explicit parity-domain hypotheses,
and the error comparison from recursive Claim 14.6(i).