theorem MathlibNt.SieveTheory.caseII_sameCAt_to_literal_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {M D : ℕ} {d Δ C K s : ℝ} (h : Lemma144CaseIISameCAt S H M D d Δ C K s) : suzukiActualT S M D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H M (↑D) d s * Real.log ↑D ^ (-Δ))

The same-constant Case-II bound implies the literal actual recurrence bound.

theorem MathlibNt.SieveTheory.exists_lemma144_caseII_odd_sameC_sourceLargeLog_uniform_moving_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) (hDmin : 2 ≤ Dmin) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (S : BoundingSieve) (C1 C K : ℝ) (N D : ℕ) (s : ℝ), C1min ≤ C1 → 3 ≤ C → 2 ≤ K → 2 ≤ D → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → C1 * K ^ Θ < Real.log ↑D → 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

Source-large Case-II closure with the cutoff chosen before the varying bounding sieve, C1, the same error constant C, K, the odd depth, D, and s. The proof uses the actual moving predecessor IH and the exact-ratio rounded transport packet; no sieve- or fixed-K eventual cutoff occurs.

theorem MathlibNt.SieveTheory.exists_lemma144_caseII_odd_sameC_sourceLargeLog_uniform_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) (hDmin : 2 ≤ Dmin) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 C K : ℝ) (N D : ℕ) (s : ℝ), C1min ≤ C1 → 3 ≤ C → 2 ≤ K → 2 ≤ D → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → C1 * K ^ Θ < Real.log ↑D → 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

Compatibility wrapper for the original fixed-sieve moving Case-II API.