theorem MathlibNt.SieveTheory.suzukiSourceV_one_eq_suzukiVOne_two (S : BoundingSieve) (D z : ℕ) : suzukiSourceV S 1 D z = SwitchingPrinciple.suzukiVOne S (↑D) 2 ↑z

The source-faithful base layer is exactly Suzuki's finite V₁ object at β = 2. This identification uses the literal source carrier D ≤ p³ and no legacy extended-layer object.

theorem MathlibNt.SieveTheory.suzukiSourceV_one_le_V_mul_fOne_add_localError {S : BoundingSieve} {D z : ℕ} {s K : ℝ} (hD : 1 < ↑D) (hs : 0 < s) (hs3 : s ≤ 3) (hz : ↑z = ↑D ^ (1 / s)) (hz2 : 2 ≤ ↑z) (hK : 0 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : suzukiSourceV S 1 D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + K * 3 ^ 2 / (s * Real.log ↑D))

Source-native V₁ base bound. Unlike the older natural bridge, both sides refer directly to suzukiSourceV; no extended Section-14 object occurs.

theorem MathlibNt.SieveTheory.caseII_source_finite_assembly {S : BoundingSieve} {β s K Vz endpointErr : ℝ} {N D y z : ℕ} (hN : Odd N) (hs : 0 < s) (hsβ : s ≤ β + 1) (hyz : y ≤ z) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) (hendpoint : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr) (hbase : suzukiSourceV S 1 D z ≤ Vz * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s + K * (β + 1) ^ 2 / (s * Real.log ↑D))) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ Vz * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + endpointErr + Vz * (K * (β + 1) ^ 2 / (s * Real.log ↑D))

Pure source-native finite Case-II assembly. The exact ceiling-cube hypotheses produce Suzuki's cutoff identity internally; the two analytic inputs are already stated on the source parity sum and source V₁.

theorem MathlibNt.SieveTheory.caseII_source_finite_assembly_normalized {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {β d Δ K s Vz endpointErr : ℝ} {N D y z : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β) (hN : Odd N) (hD : Real.exp 1 ≤ ↑D) (hd : 0 ≤ d) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hs : 0 < s) (hsβ : s ≤ β + 1) (hK : 0 ≤ K) (hVz : 0 ≤ Vz) (hyz : y ≤ z) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) (hendpoint : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr) (hbase : suzukiSourceV S 1 D z ≤ Vz * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s + K * (β + 1) ^ 2 / (s * Real.log ↑D))) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ Vz * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + endpointErr + Vz * (K * (β + 1) ^ 2 / (β - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ))

Source-native Case-II assembly with the base loss normalized to the same literal error envelope as the endpoint induction error.

theorem MathlibNt.SieveTheory.caseII_total_le_concrete_finiteSourceLayer_add_errorEnvelope (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K s endpointErr : ℝ} {N D y z : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hN : Odd N) (hD : Real.exp 1 ≤ ↑D) (hd : 0 ≤ d) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (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 / (2 - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ))

Fully concrete source-native Case-II assembly at Suzuki's source parameter β = 2. It consumes the source endpoint at the exact natural cube cutoff and proves the source V₁ estimate internally from the local-product bound.