theorem MathlibNt.SieveTheory.claim145_sqrt_div_log_eventually_ge (M : ℝ) : ∀ᶠ (K : ℝ) in Filter.atTop, max M 4 ≤ √K / Real.log K

The high-coordinate cutoff sqrt K / log K eventually exceeds any fixed Section-13 threshold. The threshold is chosen before all later parameters.

theorem MathlibNt.SieveTheory.claim145_caseA_highS_actual_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∃ (K0 : ℝ), 2 ≤ K0 ∧ ∀ (S : BoundingSieve), Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 1

Actual high-s producer for source Case A. Proposition 13.1(ii) supplies its uniform lower-profile constants first; one subsequent K threshold then works for every K, depth N, natural cutoff D, and coordinate s.

theorem MathlibNt.SieveTheory.claim145_caseA_highS_actual (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∃ (K0 : ℝ), 2 ≤ K0 ∧ Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 1

Compatibility specialization of the uniform high-coordinate leaf.

theorem MathlibNt.SieveTheory.exists_claim145_caseA_highS_actual_claim14_5Bound (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 < C1) (hΘ : 0 ≤ Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) (hgap : 0 < d - 2 * Θ) : ∃ (C145 : ℝ), 0 < C145 ∧ ∃ (K0 : ℝ), 2 ≤ K0 ∧ ∀ (K : ℝ) (N D : ℕ) (s : ℝ), K0 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → √K / Real.log K ≤ s → Real.log ↑D ≤ C1 * K ^ Θ → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Bound (fun (m : ℕ) (D' z' : ℝ) => suzukiActualT S m ⌈D'⌉₊ ⌈z'⌉₊) S H N (↑D) (↑⌈↑D ^ (1 / s)⌉₊) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s C145

Public Claim14_5Bound spelling of the same actual producer.