theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.odd_layer_weighted_eq_at_beta_add_one {β s : ℝ} {n : ℕ} (hn : Odd n) (hn3 : 3 ≤ n) (hs : 0 < s) (hsβ : s ≤ β + 1) : s * SuzukiFiniteContinuousLayers.suzukiLayer 1 β n s = (β + 1) * SuzukiFiniteContinuousLayers.suzukiLayer 1 β n (β + 1)

For every odd source layer of index at least three, the weighted layer s f_n(s) is constant on Suzuki's short initial interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.finiteSourceLayer_caseII_identity {β s : ℝ} {N : ℕ} (hN : Odd N) (hs : 0 < s) (hsβ : s ≤ β + 1) : (β + 1) / s * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (β + 1) + SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s = SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s

Exact κ=1 continuous identity used in Suzuki Case II: ((β+1)/s) T_N(β+1) + T_1(s) = T_N(s) for odd N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_T4_base_error_exact {H : Section13HatLayers} {β D K s : ℝ} (hH : Section13HatContract H β) (hs : 0 < s) (hsβ : s ≤ β + 1) (hβ1 : β ≠ 1) (hlog : Real.log D ≠ 0) : K * (β + 1) ^ 2 / (s * Real.log D) = K * (β + 1) ^ 2 / (β - 1) * (s * H.T ErrorSign.plus s) / Real.log D

T4 converts the elementary base-case loss exactly into the unperturbed odd error scale. This is the only use of the Section-13 initial data in Case II.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_base_error_le_errorEnvelope {H : Section13HatLayers} {β D d Δ K s : ℝ} {N : ℕ} (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) : K * (β + 1) ^ 2 / (s * Real.log D) ≤ K * (β + 1) ^ 2 / (β - 1) * errorEnvelope H N D d s * Real.log D ^ (-Δ)

The elementary (log D)⁻¹ base loss is absorbed into the literal odd E_N(D,s)(log D)^(-Δ) normalization.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5_caseII_finite_assembly {S : BoundingSieve} {H : Section13HatLayers} {β D _d _Δ K s Vz endpointErr : ℝ} {N Dnat znat ynat : ℕ} (_hH : Section13HatContract H β) (hN : Odd N) (hs : 0 < s) (hsβ : s ≤ β + 1) (hcut : section14ExtendedT S N Dnat znat = section14ExtendedT S N Dnat ynat + section14ExtendedV S 1 Dnat znat) (hendpoint : section14ExtendedT 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 / (s * Real.log D))

Maximal source-faithful finite Case-II inequality currently expressible with production objects. hcut is precisely (14.24), and hendpoint is the already proved Case-I estimate transported from the cutoff β+1. Everything after those two interfaces—including the exact continuous parity identity and the T4/error normalization of the base term—is proved here.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5_caseII_finite_assembly_normalized {S : BoundingSieve} {H : Section13HatLayers} {β D d Δ K s Vz endpointErr : ℝ} {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) (hcut : section14ExtendedT S N Dnat znat = section14ExtendedT S N Dnat ynat + section14ExtendedV S 1 Dnat znat) (hendpoint : section14ExtendedT 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 assembly with the base loss fully normalized to the same literal E_N(D,s)(log D)^(-Δ) used by the induction error.