theorem MathlibNt.SieveTheory.eventually_lemma144_caseII_odd_rawRoundedFinal_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {d Δ C K : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC3 : 3 ≤ C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), Odd N → 3 ≤ N → 1 < s → s ≤ 3 → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (N - 1) Dmin → have z := ⌈↑D ^ (1 / s)⌉₊; ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ caseIIOddClaim145Endpoint S d N D + SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ) * caseIIConcreteRoundedRelativeBracket N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) C K)

The genuine large-parameter raw rounded Case-II producer. Its cutoff is chosen before D, N, and s; the only recursive input left at a particular N is the global depth-N-1 induction hypothesis.

theorem MathlibNt.SieveTheory.eventually_lemma144_caseII_odd_sameC_final_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {d Δ C K C145 : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hC3 : 3 ≤ C) (hK : 2 ≤ K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), Odd N → 3 ≤ N → 1 < s → s ≤ 3 → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (N - 1) Dmin → Lemma144CaseIISameCAt S H N D d Δ C K s

Odd Case-II same-C closure with one large-parameter cutoff chosen before the odd depth N. The raw moving-IH producer and the quantitative rounded-bracket gap are both uniform in N; the closed cubic endpoint from the raw producer is preserved unchanged.

theorem MathlibNt.SieveTheory.lemma14_4_caseII_moving_final_hcaseII (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C K d Δ C145 : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hC3 : 3 ≤ C) (hK : 2 ≤ K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (depth : ℕ) : Lemma144MovingDomainCaseIIHCase S H C K d Δ depth

Exact moving-domain Case-II packet for the finite-depth assembler. Its natural cutoff is chosen before the successor depth is inspected.