theorem MathlibNt.SieveTheory.sourceParityIndices_eq_actualParityCarrier (n : ℕ) : sourceParityIndices n = suzukiActualParityCarrier n

The source parity indices coincide with the actual recurrence carrier.

theorem MathlibNt.SieveTheory.caseII_raw_inherited_gt_two {D p : ℕ} (hp : 2 ≤ p) (hD : 1 < D) (hupper : ↑p < ↑D ^ (1 / 3)) : 2 < SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p

A prime below the cubic cutoff has inherited logarithmic coordinate above two.

theorem MathlibNt.SieveTheory.eventually_lemma144_caseII_odd_rawRoundedFinal (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 → SwitchingPrinciple.SuzukiLemma144Equation1410.GlobalDepthLemma144InductionHypothesis (suzukiActualT S) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) 2 C K Δ (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.