Claim 14.5, Case A, high-s: actual closure

This file closes the source-small-D, high-coordinate branch directly for the actual discrete quantity. The final statement is uniform in the natural depth N, in every natural D ≥ 2 satisfying log D ≤ C₁ K^Θ, and in every real s ≥ √K / log K. No residual scalar comparison premise remains.

theorem MathlibNt.SieveTheory.claim145_caseA_highS_sourceL_le_logK {D K C1 Θ : ℝ} (hD : 2 ≤ D) (hK : 3 ≤ K) (hlogK1 : 1 ≤ Real.log K) (hC1 : 0 < C1) (_hΘ : 0 ≤ Θ) (hsmall : Real.log D ≤ C1 * K ^ Θ) : suzukiSourceL D K ≤ (Θ + 2 + |Real.log C1| + |Real.log (Real.log 2)|) * Real.log K

theorem MathlibNt.SieveTheory.claim145_caseA_highS_sourceSigma_le_Kbound {D K C1 Θ d : ℝ} (hD : 2 ≤ D) (hK : 3 ≤ K) (hlogK1 : 1 ≤ Real.log K) (hC1 : 0 < C1) (_hΘ : 0 ≤ Θ) (hd : 0 < d) (hsmall : Real.log D ≤ C1 * K ^ Θ) : SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ≤ C1 ^ (1 / d) * (Θ + |Real.log C1| + |Real.log (Real.log 2)| + |Real.log (Real.log 27 / Real.log 2 + 1)|) * K ^ (Θ / d) * Real.log K

theorem MathlibNt.SieveTheory.claim145_caseA_highS_log_gain_of_growth_with_constant {D K s d C1 Θ A : ℝ} (hD : 1 < D) (hK : 1 < K) (hs : 1 < s) (_hC1 : 0 < C1) (hchain : Real.log D ≤ C1 * 16 ^ Θ * s ^ (2 * Θ) * Real.log s ^ (2 * Θ)) (hgrowth : Real.exp A * C1 * 16 ^ Θ * Real.log s ^ (2 * Θ) * (Real.log (3 * K) * Real.log (3 * s) ^ 2) ≤ s ^ (d - 2 * Θ)) : s * (Real.log (Real.log (3 * K)) + 2 * Real.log (Real.log (3 * s)) + A) ≤ s * Real.log (1 + s ^ d / Real.log D)

theorem MathlibNt.SieveTheory.claim145_caseA_highS_log_gain_with_constant_eventually {d C1 Θ A : ℝ} (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hgap : 0 < d - 2 * Θ) : ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (D s : ℝ), 2 ≤ D → 4 ≤ s → √K / Real.log K ≤ s → Real.log K ≤ 4 * Real.log s → Real.log D ≤ C1 * K ^ Θ → s * (Real.log (Real.log (3 * K)) + 2 * Real.log (Real.log (3 * s)) + A) ≤ s * Real.log (1 + s ^ d / Real.log D)

theorem MathlibNt.SieveTheory.claim145_caseA_highS_exp_le_profile {D K s d C : ℝ} (hD : 1 < D) (hK : 1 < K) (hs : 4 ≤ s) (hL1 : 1 ≤ suzukiSourceL D K) (hsourceLarge : Real.exp 1 * suzukiSourceL D K ≤ s - 2) (hLprod : suzukiSourceL D K ≤ Real.log (3 * K) * Real.log (3 * s)) (hgain : s * (Real.log (Real.log (3 * K)) + 2 * Real.log (Real.log (3 * s)) + (C + 3 + Real.log 2)) ≤ s * Real.log (1 + s ^ d / Real.log D)) : Real.exp (suzukiSourceL D K + (s - 2) * (1 + Real.log (suzukiSourceL D K) - Real.log (s - 2))) ≤ (1 + s ^ d / Real.log D) ^ s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s

theorem MathlibNt.SieveTheory.claim145_caseA_highS_front_factor_eventually_uniform_in_S {d Δ C1 Θ : ℝ} (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (S : BoundingSieve) (D s : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 4 ≤ s → √K / Real.log K ≤ s → Real.log D ≤ C1 * K ^ Θ → 1 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * s * Real.log D ^ (-Δ)

theorem MathlibNt.SieveTheory.claim145_caseA_highS_front_factor_eventually (S : BoundingSieve) {d Δ C1 Θ : ℝ} (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (D s : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 4 ≤ s → √K / Real.log K ≤ s → Real.log D ≤ C1 * K ^ Θ → 1 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * s * Real.log D ^ (-Δ)

Compatibility specialization of the uniform front-factor cutoff.

theorem MathlibNt.SieveTheory.claim145_caseA_highS_habsorb_eventually_uniform_in_S {d Δ C1 Θ C : ℝ} (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (S : BoundingSieve) (D s : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 4 ≤ s → √K / Real.log K ≤ s → Real.log D ≤ C1 * K ^ Θ → 1 ≤ suzukiSourceL D K → Real.exp 1 * suzukiSourceL D K ≤ s - 2 → suzukiSourceL D K ≤ Real.log (3 * K) * Real.log (3 * s) → Real.exp (suzukiSourceL D K + (s - 2) * (1 + Real.log (suzukiSourceL D K) - Real.log (s - 2))) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * ((1 + s ^ d / Real.log D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log D ^ (-Δ)

Final high-coordinate (14.6) scalar absorption. Unlike an actual-bound wrapper, this statement exposes the complete numerical comparison: the finite Euler reciprocal (through claim14_5VProduct), the moving sourceSigma, all logarithmic powers, and the uniform linear loss C*s from Proposition 13.1(ii). The hypotheses hL1, hsourceLarge, and hLprod are precisely the already proved Lemma-14.3 high-coordinate transition conditions; the only eventual work left here is the source-small-D absorption, uniformly in D and s.

theorem MathlibNt.SieveTheory.claim145_caseA_highS_habsorb_eventually (S : BoundingSieve) {d Δ C1 Θ C : ℝ} (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (D s : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 4 ≤ s → √K / Real.log K ≤ s → Real.log D ≤ C1 * K ^ Θ → 1 ≤ suzukiSourceL D K → Real.exp 1 * suzukiSourceL D K ≤ s - 2 → suzukiSourceL D K ≤ Real.log (3 * K) * Real.log (3 * s) → Real.exp (suzukiSourceL D K + (s - 2) * (1 + Real.log (suzukiSourceL D K) - Real.log (s - 2))) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * ((1 + s ^ d / Real.log D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log D ^ (-Δ)

Compatibility specialization of the uniform high-coordinate absorption.