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) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ B0 + 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).