Case-II raw rounded transport without the outer-endpoint Claim 14.6(i) interface

The three variants below replace the overstrong quotient Claim-14.6(i) premise on the outer source interval by the only consequence used by the rounded assembly: coordinate-wise transport of the quotient error envelope.

theorem MathlibNt.SieveTheory.caseII_endpoint_le_concrete_finiteSourceLayer_add_qD_natCeil_of_errorTransport (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D y : ℕ} {β σ C C1 K ΘK Δ d B0 : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β) (hN : Odd N) (hN2 : 2 ≤ N) (hycube : ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S y, p ^ 3 < D) (hyceil : y = ⌈↑D ^ (1 / (β + 1))⌉₊) (_hyDhalf : ↑y ≤ ↑D / 2) (hβ1σ : β + 1 ≤ σ) (hD : 1 < ↑D) (hDlarge : β * Real.log 2 ≤ (β - 1) * Real.log ↑D) (hwy : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / (β + 1))) (hy2 : 2 ≤ ↑y) (hroot2 : 2 ≤ ↑D ^ (1 / (β + 1))) (hw2 : 2 ≤ ↑D ^ (1 / σ)) (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 y) D σ (β + 1), 0 ≤ S.nu p) (hC : 0 ≤ C) (hlog : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ (β + 1), 0 ≤ Real.log ↑(D ⌈/⌉ p)) (hSourceDomain : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ (β + 1), SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hErrorTransport : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ (β + 1), 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) β C K Δ N D σ (β + 1)) (hErrorThreshold : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ β + 1) (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 / (β + 1)) → 2 ≤ p ∧ 2 * p ≤ D) (hT : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / (β + 1)) → 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 / (β + 1)) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y ≤ B0 + (SwitchingPrinciple.suzukiVProduct S ↑y * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1) + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) β / Real.log (↑D ^ (1 / σ)) * ((β + 1) / (β + 1))) + C * Real.exp √K * SwitchingPrinciple.suzukiVProduct S ↑y * Real.log ↑D ^ (-Δ) * ((1 / (β + 1) * ∫ (t : ℝ) in β + 1..σ, 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 Δ (β + 1) / Real.log (↑D ^ (1 / σ)) * ((β + 1) / (β + 1))))

theorem MathlibNt.SieveTheory.caseII_total_le_from_caseI_endpoint_explicit_rawBase_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 ≤ Δ) (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)) (hs : 0 < 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)) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + caseIIRoundedTransportErr S H N (↑D) (↑D ^ (1 / 3)) (↑D ^ (1 / s)) d Δ σ C K B0 s + SwitchingPrinciple.suzukiVProduct S ↑z * (9 * K / (s * Real.log ↑D))

Double-rounded sharp Case-II endpoint transport.

The natural cutoffs are y = ceil(D^(1/3)) and z = ceil(D^(1/s)). Dimension-one transport and the logarithmic ratio are carried out only at the exact real roots. The two Euler products are then returned exactly to their natural-ceiling cutoffs; no equality between a cast natural cutoff and a real root is assumed.

theorem MathlibNt.SieveTheory.caseII_total_le_doubleRounded_direct_concrete_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 : 1 ≤ 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 ^ (-Δ) * caseIIConcreteRoundedRelativeBracket N (↑D) d Δ σ C K)

Direct double-rounded concrete relative Case-II theorem.

The Case-I induction/source packet is consumed by the sharp natural-ceiling endpoint theorem. The resulting transport remainder is absorbed by the fixed positive-Δ packet, and the packet is then contracted to the concrete relative coefficient. In particular, the public interface exposes neither a raw endpoint inequality nor an abstract endpoint-error premise.