Lemma 14.4, Case I: unconditional same-constant successor

This is the final assembly against the source interfaces. The recurrence and IH are the actual finite ones; Σ₀ is first identified with the single source endpoint, Σ₁₁ is the internal Lemma-8.7 estimate, Σ₁₂ uses the natural ceiling, and Σ₂ vanishes in the genuine κ = 1 Case-I range.

The only upstream name intentionally isolated by this file is caseI1423_sigmaZero_realEndpoint_sourceBound. It is the expected real endpoint source estimate for the explicit Claim-14.5 remainder, not a bound on Σ₀, a mainSum estimate, or an absorption hypothesis. Once that producer is present, the theorem below has no Sigma-bound, mainSum, or absorption premise.

theorem MathlibNt.SieveTheory.lemma14_4_caseI_successor_sameC_eventually (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N Dmin : ℕ} {C C145 K d Δ s : ℝ} (hN : 2 ≤ N) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) (hspred : s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hs : 2 ≤ s) (hsLower : 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 < C) (hC145 : 0 < C145) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; 4 ≤ D → 1 < σ → s ≤ σ → 2 ≤ ↑D ^ (1 / s) → 2 ≤ ↑D ^ (1 / σ) → ↑D ^ (1 / σ) ≤ ↑D ^ (1 / s) → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s → (Odd N → z ^ 3 ≤ D) → (∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, Nat.Prime p) → SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (SwitchingPrinciple.suzukiSupportedBelow S z) D Dmin σ s → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → 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 → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → suzukiActualT S N D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + sigma12InheritedBudget S H N D z C K d Δ s

Eventual Case-I successor with literally the same constant C in the induction hypothesis, inherited budget, and conclusion.