theorem MathlibNt.SieveTheory.suzukiSupportedBelow_ceil_real (S : BoundingSieve) (y : ℝ) : SwitchingPrinciple.suzukiSupportedBelow S ⌈y⌉₊ = {p ∈ S.prodPrimes.primeFactors | ↑p < y}

A natural ceiling is exactly the natural cutoff representing the strict real inequality p < y.

theorem MathlibNt.SieveTheory.caseI_endpoint_power_cube {β D y : ℝ} (hD : 0 ≤ D) (hβ : β = 2) (hy : y = D ^ (1 / (β + 1))) : y ^ 3 = D

At the κ=1 source endpoint β = 2, the real power coordinate has exactly cube D.

theorem MathlibNt.SieveTheory.section14ExtendedV_one_eq_zero_of_ceil_of_cube_le (S : BoundingSieve) {Dnat : ℕ} {y : ℝ} (hycube : y ^ 3 ≤ ↑Dnat) : section14ExtendedV S 1 Dnat ⌈y⌉₊ = 0

The exact boundary condition needed for the natural recurrence. Unlike the coarser ynat^3 ≤ Dnat, this condition is preserved by choosing ynat = ceil y: every integer p < ceil y satisfies p < y.

theorem MathlibNt.SieveTheory.section14ExtendedT_recurrence_of_ceil_of_cube_le (S : BoundingSieve) {N Dnat : ℕ} {y : ℝ} (hN2 : 2 ≤ N) (hycube : y ^ 3 ≤ ↑Dnat) : section14ExtendedT S N Dnat ⌈y⌉₊ = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈y⌉₊, S.nu p * section14ExtendedT S (N - 1) (Dnat ⌈/⌉ p) p

Exact section14ExtendedT recurrence at a ceiling cutoff. This is the natural-API form needed at the Case-II endpoint.

theorem MathlibNt.SieveTheory.section14ExtendedT_recurrence_at_caseI_endpoint (S : BoundingSieve) {N Dnat : ℕ} {β D y : ℝ} (hN2 : 2 ≤ N) (hD : D = ↑Dnat) (hD0 : 0 ≤ D) (hβ : β = 2) (hy : y = D ^ (1 / (β + 1))) : section14ExtendedT S N Dnat ⌈y⌉₊ = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈y⌉₊, S.nu p * section14ExtendedT S (N - 1) (Dnat ⌈/⌉ p) p

The Case-I endpoint y = D^(1/(β+1)), with the source value β=2, feeds the natural ceiling recurrence without the false condition ceil(y)^3 ≤ Dnat.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_eq_section14ExtendedT_at_ceil (S : BoundingSieve) (N Dnat : ℕ) (y : ℝ) (hlegal : ⌈y⌉₊ ^ N ≤ Dnat) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n Dnat ⌈y⌉₊ = section14ExtendedT S N Dnat ⌈y⌉₊

The legal-domain bridge at the natural endpoint. The power condition is kept explicit: it is not implied by a real power coordinate after taking a ceiling.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_natural_endpoint_iff_caseI_source_endpoint {S : BoundingSieve} {β s Vz endpointErr y : ℝ} {N Dnat ynat : ℕ} (hynat : ynat = ⌈y⌉₊) (hlegal : ynat ^ N ≤ Dnat) : section14ExtendedT S N Dnat ynat ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr ↔ ∑ n ∈ sourceParityIndices N, suzukiSourceV S n Dnat ynat ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr

Under the legal-domain power condition, the endpoint inequality required by Case II is exactly the corresponding source-faithful Case-I inequality. This statement has no endpoint-bound hypothesis and makes the remaining analytic obligation explicit.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseI_source_endpoint_to_caseII_natural {S : BoundingSieve} {β s Vz endpointErr y : ℝ} {N Dnat ynat : ℕ} (hynat : ynat = ⌈y⌉₊) (hlegal : ynat ^ N ≤ Dnat) (hsourceEndpoint : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n Dnat ynat ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr) : section14ExtendedT S N Dnat ynat ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr

Exact Case-I endpoint inequality consumed by the Case-II normalized assembly, transported from the source-faithful parity sum to the natural section14ExtendedT API. The real endpoint is represented by ynat = ceil y, and the source/extended identification requires the explicit legal-domain power condition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5_caseII_finite_assembly_normalized_of_caseI_source_endpoint {S : BoundingSieve} {H : Section13HatLayers} {β D d Δ K s Vz endpointErr y : ℝ} {N Dnat znat ynat : ℕ} (hH : 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) (hynat : ynat = ⌈y⌉₊) (hlegal : ynat ^ N ≤ Dnat) (hcut : section14ExtendedT S N Dnat znat = section14ExtendedT S N Dnat ynat + section14ExtendedV S 1 Dnat znat) (hsourceEndpoint : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n Dnat ynat ≤ Vz * ((β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1)) + endpointErr) (hbase : section14ExtendedV S 1 Dnat znat ≤ Vz * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s + K * (β + 1) ^ 2 / (s * Real.log D))) : section14ExtendedT S N Dnat znat ≤ Vz * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + endpointErr + Vz * (K * (β + 1) ^ 2 / (β - 1) * errorEnvelope H N D d s * Real.log D ^ (-Δ))

Case-II normalized assembly with no opaque hendpoint argument: the exact source-faithful Case-I endpoint inequality is transported through the legal bridge internally.