A quantifier-order strengthening of the internal Σ₁₂ contraction. The large-D threshold comes only from the full moving Claim 14.6 source assembly, so it is chosen before, and is uniform in, the depth N and coordinate s.

theorem MathlibNt.SieveTheory.eventually_sigmaTwelve_internal_contraction_sameC_uniform {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {C K d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 ≤ C) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → ∀ (N : ℕ) (s : ℝ) (z : ℕ), 2 ≤ N → 0 < s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s → 1 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 1 < ↑D → 2 ≤ ↑D ^ (1 / s) → 2 ≤ ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑D ^ (1 / s) → z = ⌈↑D ^ (1 / s)⌉₊ → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) Δ) / 2 ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) (SwitchingPrinciple.suzukiVProduct S ↑z) C K Δ N D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s ≤ sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) Δ * sigma12InheritedBudget S H N D z C K d Δ s + sigma12EndpointRemainder S H N D z C K d Δ s (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) (SwitchingPrinciple.suzukiVProduct S ↑z) C K Δ N D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s ≤ q.ρ * sigma12InheritedBudget S H N D z C K d Δ s + sigma12EndpointRemainder S H N D z C K d Δ s (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

The natural-ceiling Σ₁₂ same-constant contraction with one threshold uniform in both the induction depth N and the coordinate s.