theorem MathlibNt.SieveTheory.caseI_total_le_concrete_finiteSourceLayer_add_qD (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D z : ℕ} {β σ s C C1 K ΘK Δ d B0 : ℝ} (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) (hcaseITau : 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) (hnu : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, 0 ≤ S.nu p) (hC : 0 ≤ C) (hlog : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, 0 ≤ Real.log ↑(D ⌈/⌉ p)) (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)) (hClaim14_6_i : ∀ 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) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) β C K Δ N D σ s) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hsm1dom : s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hD : 1 < ↑D) (hz2 : 2 ≤ ↑z) (hv2 : 2 ≤ ↑D ^ (1 / s)) (hw2 : 2 ≤ ↑D ^ (1 / σ)) (hwv : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / s)) (hvz : ↑D ^ (1 / s) ≤ ↑z) (hErrorThreshold : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hClaim14_6_ii : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H (↑D) d Δ σ) (hΔ : 0 ≤ Δ) (hCeilFull : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) (hT : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hClaim14_13 : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ B0 + (SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (s - 1) / Real.log (↑D ^ (1 / σ)) * (s / s)) + C * Real.exp √K * SwitchingPrinciple.suzukiVProduct S ↑z * Real.log ↑D ^ (-Δ) * ((1 / s * ∫ (t : ℝ) in s..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t) + 6 * K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ s / Real.log (↑D ^ (1 / σ)) * (s / s)))

Final concrete finite Case-I assembly. The total source inequality is specialized to Suzuki's Euler product, while the exact carrier equality moves the full-support sigmaTwelve estimate onto the supported carrier required by the recurrence assembly.