Case-I source-large coefficient and uniform Σ₁₂ interface

The coefficient cutoff and the Claim-14.6 cutoff are selected before the later Case-I constants. In particular, the Σ₁₂ theorem below has C and K inside the universal quantifier following D₀; its API contains no post-K eventual quantifier.

theorem MathlibNt.SieveTheory.exists_caseISourceOrderCoefficient_sourceLargeLog_uniform {Amax d Δ Θ : ℝ} (hAmax : 0 ≤ Amax) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hΘ : 0 < Θ) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 K D A : ℝ), C1min ≤ C1 → 2 ≤ K → 2 ≤ D → 0 ≤ A → A ≤ Amax → C1 * K ^ Θ < Real.log D → ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient A D d ≤ 1 - q.ρ

Quantitative source-large replacement for eventually_caseISourceOrderCoefficient_le_sameC_gap. The witness C1min is selected before C1,K,D,A.

theorem MathlibNt.SieveTheory.caseISigmaZero_ratio_le_commonScale {A C C145 : ℝ} (hA : 0 < A) (hC : 0 < C) (hscale : A * C145 ≤ C) : C145 / C ≤ 1 / A

Under the common scale C ≥ A*C145, the direct Σ₀ coefficient is bounded before C145 and C are chosen.

theorem MathlibNt.SieveTheory.caseI_endpointCoefficient_le_commonScale {A C C145 K L R : ℝ} (hA : 0 < A) (hC3 : 3 ≤ C) (hscale : A * C145 ≤ C) (hL : 0 ≤ L) (hR : 0 ≤ R) : C145 / C + 6 * L * R / (C * Real.exp √K) + 12 * R ≤ 1 / A + 2 * L * R + 12 * R

The three endpoint constants have a fixed upper bound under the common scale C ≥ max 3 (A*C145). This is the Amax supplied to the quantitative source-order theorem above.

theorem MathlibNt.SieveTheory.exists_sigmaTwelve_internal_contraction_binderUniform_in_S {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (S : BoundingSieve) (C K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 0 ≤ C → ∀ (D N : ℕ) (s : ℝ) (z : ℕ), D₀ ≤ ↑D → 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)) → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p → ↑p < ↑D ^ (1 / s) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑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 Claim-14.6 cutoff selected before the varying sieve S, then before C, K, the depth N, and the coordinate s. The threshold is genuinely source-uniform: it is the Claim-14.6 cutoff, which depends only on H, d, and Δ.

theorem MathlibNt.SieveTheory.exists_sigmaTwelve_internal_contraction_binderUniform {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (C K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 0 ≤ C → ∀ (D N : ℕ) (s : ℝ) (z : ℕ), D₀ ≤ ↑D → 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)) → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p → ↑p < ↑D ^ (1 / s) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑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)

Compatibility specialization of the threshold-uniform-in-S contraction.