Lemma 14.4, Case I: uniform-in-s 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 real endpoint, Σ₀ transport, and Σ₁₂ contraction estimates are consumed through their production uniform source interfaces, not as bounds on a Sigma term, a mainSum estimate, or an absorption hypothesis.

theorem MathlibNt.SieveTheory.lemma14_4_caseI_successor_sameC_uniform_strict (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {C C145 K d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 < C) (hC145 : 0 < C145) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), 2 ≤ N → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → 2 ≤ s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s → 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 → (∀ 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

Uniform Case-I successor with literally the same C: one cutoff precedes N,s, and every geometry/IH premise follows those binders.