Claim 14.5, Case A: bounded K

This is the bounded-parameter branch suppressed by the source O(1) notation. There is no numerical search: the quotient range follows from exponentiating log D ≤ C₁ K^Θ, and monotonicity replaces every local-product parameter by the single upper endpoint Kmax.

theorem MathlibNt.SieveTheory.hasDimensionOneLocalProductBound_mono_K {S : BoundingSieve} {K K' : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hKK' : K ≤ K') : SwitchingPrinciple.HasDimensionOneLocalProductBound S K'

theorem MathlibNt.SieveTheory.claim14_5Scale_upperK_le (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) {D d Δ σ K Kmax s : ℝ} (hD : 1 < D) (hσ : 0 < σ) (hs : 0 < s) (hT : 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) s) : SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N D d Δ σ Kmax s ≤ Real.exp √Kmax * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N D d Δ σ K s

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

One Claim-14.5 constant works simultaneously for every 1 ≤ K ≤ Kmax, every natural quotient and depth, and every s ≥ 2 in Case A. The lower edge 1 ≤ K is stronger than necessary here (0 < K would suffice), but is the legal source range and avoids any hidden K < 1 branch.

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

Compatibility specialization of the sieve-uniform bounded-K producer.