noncomputable def MathlibNt.SieveTheory.caseIIEndpointSigma11 (K : ℝ) (N : ℕ) (D σ : ℝ) : ℝ

The explicit Σ₁₁ endpoint loss left by the Case-I estimate at the cubic endpoint β+1=3.

Equations

• MathlibNt.SieveTheory.caseIIEndpointSigma11 K N D σ = 6 * K ^ 2 * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2 / Real.log (D ^ (1 / σ)) * (3 / 3)

noncomputable def MathlibNt.SieveTheory.caseIIEndpointQD (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (D d Δ σ C K : ℝ) : ℝ

The complete transported q_D contribution left by the Case-I estimate at β+1=3.

Equations

• MathlibNt.SieveTheory.caseIIEndpointQD H N D d Δ σ C K = C * Real.exp √K * Real.log D ^ (-Δ) * ((1 / 3 * ∫ (t : ℝ) in 3..σ, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ t) + 6 * K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ 3 / Real.log (D ^ (1 / σ)) * (3 / 3))

noncomputable def MathlibNt.SieveTheory.caseIIEndpointErr (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D y z : ℕ) (d Δ σ C K B0 s : ℝ) : ℝ

The named, fully explicit endpoint error used by source-native Case II. Besides the transported B₀, Σ₁₁, and q_D terms, it displays separately the excess from the dimension-one product ratio: (3/s) * (K/log y) * finiteSourceLayer ....

Equations

• MathlibNt.SieveTheory.caseIIEndpointErr S H N D y z d Δ σ C K B0 s = B0 + MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (3 / s * (K / Real.log ↑y) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 3 / s * (1 + K / Real.log ↑y) * MathlibNt.SieveTheory.caseIIEndpointSigma11 K N (↑D) σ + 3 / s * (1 + K / Real.log ↑y) * MathlibNt.SieveTheory.caseIIEndpointQD H N (↑D) d Δ σ C K)

theorem MathlibNt.SieveTheory.caseII_finiteSourceLayer_three_nonneg {N : ℕ} (hN : Odd N) : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3

At odd depth, the endpoint value of the finite source layer is nonnegative on its exact parity domain.

theorem MathlibNt.SieveTheory.caseIIEndpointSigma11_nonneg {N D : ℕ} {K σ : ℝ} (hN : Odd N) (hw2 : 2 ≤ ↑D ^ (1 / σ)) : 0 ≤ caseIIEndpointSigma11 K N (↑D) σ

The explicit Σ₁₁ endpoint loss is nonnegative in the Case-II range.

theorem MathlibNt.SieveTheory.caseIIEndpointQD_nonneg {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {N D : ℕ} {d Δ σ C K : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hD : 1 < ↑D) (h3σ : 3 ≤ σ) (hw2 : 2 ≤ ↑D ^ (1 / σ)) (hC : 0 ≤ C) : 0 ≤ caseIIEndpointQD H N (↑D) d Δ σ C K

The transported q_D endpoint contribution is nonnegative under the Section-13 positivity contract and the Case-II endpoint hypotheses.

theorem MathlibNt.SieveTheory.suzukiVProduct_le_dimensionOne_ratio (S : BoundingSieve) {K : ℝ} {y z : ℕ} (hy2 : 2 ≤ ↑y) (hyz : y ≤ z) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : SwitchingPrinciple.suzukiVProduct S ↑y ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (Real.log ↑z / Real.log ↑y) * (1 + K / Real.log ↑y)

The genuine dimension-one finite Euler-product transport from y to z. No independent product-ratio hypothesis is used.

theorem MathlibNt.SieveTheory.caseII_log_ratio_of_power_identities {D y z s : ℝ} (hD : Real.exp 1 ≤ D) (hs : 0 < s) (hy : y = D ^ (1 / 3)) (hz : z = D ^ (1 / s)) : Real.log z / Real.log y = 3 / s

The Case-II logarithmic ratio follows from the two exact power coordinates.

theorem MathlibNt.SieveTheory.caseII_endpoint_transport_explicit (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D y z : ℕ} {d Δ σ C K B0 s : ℝ} (_hs : 0 < s) (hlogRatio : Real.log ↑z / Real.log ↑y = 3 / s) (hVratio : SwitchingPrinciple.suzukiVProduct S ↑y ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (Real.log ↑z / Real.log ↑y) * (1 + K / Real.log ↑y)) (hF : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hSigma11 : 0 ≤ caseIIEndpointSigma11 K N (↑D) σ) (hQD : 0 ≤ caseIIEndpointQD H N (↑D) d Δ σ C K) (hcaseI : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y ≤ B0 + SwitchingPrinciple.suzukiVProduct S ↑y * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + caseIIEndpointSigma11 K N (↑D) σ) + SwitchingPrinciple.suzukiVProduct S ↑y * caseIIEndpointQD H N (↑D) d Δ σ C K) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (3 / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) + caseIIEndpointErr S H N D y z d Δ σ C K B0 s

Algebraic endpoint transport. The Case-I main layer is split into the required (3/s) term and the explicit ratio excess; every other Case-I term is placed in caseIIEndpointErr.

theorem MathlibNt.SieveTheory.caseII_total_le_from_caseI_endpoint_explicit (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) (hpower : ↑D ^ (1 / 3) = ↑y) (hyDhalf : ↑y ≤ ↑D / 2) (h3σ : 3 ≤ σ) (hD : Real.exp 1 ≤ ↑D) (hDlarge : 2 * Real.log 2 ≤ Real.log ↑D) (hwy : ↑D ^ (1 / σ) ≤ ↑y) (hy2 : 2 ≤ ↑y) (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)) (hClaim14_6_i : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ 3, SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H (↑(D ⌈/⌉ p)) d σ) (hErrorDomain : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ 3, 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 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) (hd : 0 ≤ d) (hCeilFull : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑y → 2 ≤ p ∧ 2 * p ≤ D) (hT : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑y → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hClaim14_13 : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑y → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) (hs : 0 < s) (hs3 : s ≤ 3) (hyz : y ≤ z) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) (hz : ↑z = ↑D ^ (1 / s)) (hz2 : 2 ≤ ↑z) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + caseIIEndpointErr S H N D y z d Δ σ C K B0 s + SwitchingPrinciple.suzukiVProduct S ↑z * (K * 3 ^ 2 / (2 - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ))

Final source-native Case-II converter. It invokes the concrete Case-I endpoint theorem at y, proves the V(y)/V(z) transport from the genuine local-product hypothesis, discharges all three endpoint nonnegativity facts from the parity domain and Section-13 positivity contract, and feeds the resulting named caseIIEndpointErr directly to the source-native Case-II assembly. In particular, there is no arbitrary hendpoint, hF, hSigma11, or hQD premise.