theorem MathlibNt.SieveTheory.caseII_total_le_concrete_finiteSourceLayer_add_rawBase (S : BoundingSieve) {K s endpointErr : ℝ} {N D y z : ℕ} (hN : Odd N) (hD : Real.exp 1 ≤ ↑D) (hs : 0 < s) (hs3 : s ≤ 3) (hK : 0 ≤ K) (hyz : y ≤ z) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) (hz : ↑z = ↑D ^ (1 / s)) (hz2 : 2 ≤ ↑z) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hendpoint : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (3 / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) + endpointErr) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + endpointErr + SwitchingPrinciple.suzukiVProduct S ↑z * (K * 3 ^ 2 / (s * Real.log ↑D))

Sharp source-native Case-II assembly at β = 2.

Unlike caseII_total_le_concrete_finiteSourceLayer_add_errorEnvelope, this uses the unnormalised source assembly and therefore retains the base-layer loss at its native 1 / (s * log D) scale.

theorem MathlibNt.SieveTheory.caseII_total_le_from_caseI_endpoint_explicit_rawBase (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 / (s * Real.log ↑D))

Full production endpoint transport followed by the sharp source-native Case-II assembly. Every term of caseIIEndpointErr is retained (including the Euler-product ratio excess), while the source V₁ base loss remains 9 K / (s log D) rather than being normalised to a bare 9 K multiple of the error envelope. No legacy extended-layer object occurs.