theorem
MathlibNt.SieveTheory.caseII_total_le_doubleRounded_direct_sourceLarge_relative_natCeil_of_errorTransport
(S : BoundingSieve)
(H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers)
{N D y z : ℕ}
{σ C C1 K ΘK Δ d B0 s : ℝ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2)
(hN : Odd N)
(hN2 : 2 ≤ N)
(hycube : ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S y, p ^ 3 < D)
(hyceil : y = ⌈↑D ^ (1 / 3)⌉₊)
(hyDhalf : ↑y ≤ ↑D / 2)
(h3σ : 3 ≤ σ)
(hD : Real.exp 1 ≤ ↑D)
(hDlarge : 2 * Real.log 2 ≤ Real.log ↑D)
(hwy : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / 3))
(hy2 : 2 ≤ ↑y)
(hyr2 : 2 ≤ ↑D ^ (1 / 3))
(hw2 : 2 ≤ ↑D ^ (1 / σ))
(hEndpoint :
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime 2 (↑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 y) D σ 3,
0 ≤ S.nu p)
(hC : 0 ≤ C)
(hlog :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ 3,
0 ≤ Real.log ↑(D ⌈/⌉ p))
(hSourceDomain :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ 3,
SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1))
(hErrorTransport :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ 3,
SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d
(SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d
(SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p))
(hIH :
SwitchingPrinciple.SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract
(SwitchingPrinciple.suzukiSupportedBelow S y)
(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) 2 C K Δ N D σ 3)
(hErrorThreshold : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ 3)
(hK : 2 ≤ K)
(hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K)
(hClaim14_6_ii : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H (↑D) d Δ σ)
(hΔ0 : 0 < Δ)
(hΔ1 : Δ < 1)
(hCeilFull : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / 3) → 2 ≤ p ∧ 2 * p ≤ D)
(hT :
∀ p ∈ S.prodPrimes.primeFactors,
↑D ^ (1 / σ) ≤ ↑p →
↑p < ↑D ^ (1 / 3) →
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 / 3) →
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p)
(↑D / ↑p))
(hs1 : 1 < s)
(hs3 : s ≤ 3)
(hyrzr : ↑D ^ (1 / 3) ≤ ↑D ^ (1 / s))
(hyz : y ≤ z)
(hyLower : (y - 1) ^ 3 < D)
(hyUpper : D ≤ y ^ 3)
(hzceil : z = ⌈↑D ^ (1 / s)⌉₊)
(hzr2 : 2 ≤ ↑D ^ (1 / s))
(hsmall : 3 ^ d ≤ Real.log ↑D)
(hE : 1 / 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s)
(hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ))
(hClaim14_6_iii :
∫ (t : ℝ) in 3..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H
(SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N)
(↑D) d 0 3)
(hLambdaCubic :
SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N)
(↑D) d 0 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation (↑D) d 0 3 * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N)
(↑D) d 0 s)
(hP : 3 ≤ C * Real.exp √K)
(_hPE : 1 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s)
:
∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ B0 + SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ) * caseIIConcreteRoundedRelativeBracketSourceLarge N (↑D) d Δ σ K)
Direct double-rounded Case-II assembly into the exact-ratio source-large relative bracket. This is the K-uniform consumer of the rounded transport packet; no abstract endpoint-error premise is exposed.