theorem MathlibNt.SieveTheory.suzukiSourceV_one_eq_zero_of_supported_cube (S : BoundingSieve) {D y : ℕ} (hcube : ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S y, p ^ 3 < D) : suzukiSourceV S 1 D y = 0

A literal cubic carrier makes the source base layer vanish. This is the exact finite statement needed when the Case-I theorem is used at the Case-II cutoff; no global hypothesis y^N ≤ D is involved.

theorem MathlibNt.SieveTheory.caseITau_eq_beta_add_one_of_log_threshold {β D : ℝ} (hβ : 1 < β) (hD : 1 < D) (hDlarge : β * Real.log 2 ≤ (β - 1) * Real.log D) : caseITau D (β + 1) = β + 1

At s = β+1, the finite correction in caseITau is inactive under the same explicit large-D logarithmic threshold as in Case I.

theorem MathlibNt.SieveTheory.caseII_endpoint_le_concrete_finiteSourceLayer_add_qD (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) (hpower : ↑D ^ (1 / (β + 1)) = ↑y) (hyDhalf : ↑y ≤ ↑D / 2) (hβ1σ : β + 1 ≤ σ) (hD : 1 < ↑D) (hDlarge : β * Real.log 2 ≤ (β - 1) * Real.log ↑D) (hwy : ↑D ^ (1 / σ) ≤ ↑y) (hy2 : 2 ≤ ↑y) (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)) (hClaim14_6_i : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ (β + 1), SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H (↑(D ⌈/⌉ p)) d σ) (hErrorDomain : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S y) D σ (β + 1), 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) β 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 < ↑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)) : ∑ 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))))

Maximal direct instantiation of the final concrete Case-I theorem at the Case-II endpoint s=β+1, z=y (odd N).

The Case-I-only premises hbase, hcube, hdom, hcaseITau, hcaseI, hsdom, hsm1dom, hv2, and hvz are discharged here. The endpoint provider remains at s'=σ, not at the current endpoint β+1; hence the theorem does not hide the desired current-s estimate in hEndpoint.

Two genuinely arithmetic endpoint facts remain explicit: the exact real power identity D^(1/(β+1))=y required by the Case-I API, and y ≤ D/2, required by its exact min(y,D/2) cutoff contract.