def MathlibNt.SieveTheory.Lemma144CaseIIFinalSide (N : ℕ) (s : ℝ) : Prop

The Case-II side used by the finite-depth partition: odd depth and the closed low strip. At even depth this side is empty.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIFinalSide N s = (Odd N ∧ s ≤ 3)

theorem MathlibNt.SieveTheory.eventually_lemma144_caseII_odd_sameC_final (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin N : ℕ} {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) (hN : Odd N) (hN3 : 3 ≤ N) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (s : ℝ), 1 < s → s ≤ 3 → Lemma144GlobalDepthAt S H C K d Δ (N - 1) Dmin → Lemma144CaseIISameCAt S H N D d Δ C K s

Direct odd Case-II same-C closure with the genuine global predecessor IH. The raw rounded estimate and Claim-14.5 endpoint normalization are combined at one eventual cutoff; no IH-free raw-producer abstraction is used.

theorem MathlibNt.SieveTheory.lemma14_4_caseII_final_finiteDepth_interface (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) (N Dmin : ℕ) : 1 ≤ N → 2 ≤ Dmin → Lemma144GlobalDepthAt S H C K d Δ N Dmin → ∃ (DII : ℕ), Dmin ≤ DII ∧ Lemma144UniformNatCeilRestrictedAt S H C K d Δ (N + 1) DII (Lemma144CaseIIFinalSide (N + 1))

Exact hcaseII packet expected by lemma14_4_full_finiteDepth_final. For a successor depth, the Case-II side is impossible when the successor is even; when it is odd, N+1 ≥ 3 and the direct global-IH theorem applies.

theorem MathlibNt.SieveTheory.lemma14_4_caseII_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 N Dmin : ℕ) : 1 ≤ N → N < depth → 2 ≤ Dmin → Lemma144GlobalDepthAt S H C K d Δ N Dmin → ∃ (DII : ℕ), Dmin ≤ DII ∧ Lemma144UniformNatCeilRestrictedAt S H C K d Δ (N + 1) DII (Lemma144CaseIIFinalSide (N + 1))

The same packet with the unused finite-depth bound binders, ready to pass literally as hcaseII to lemma14_4_full_finiteDepth_final.