theorem MathlibNt.SieveTheory.caseA_lowerProfile_eventually_one {q : ℕ} {d C : ℝ} (hq : 2 ≤ q) (hd : 2 < d) : ∀ᶠ (x : ℝ) in Filter.atTop, 1 ≤ (1 + x ^ d / Real.log ↑q) ^ x * x * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C x

theorem MathlibNt.SieveTheory.section13Hat_uniform_pos_on_compact {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {M : ℝ} (hM : 2 ≤ M) : ∃ (e : ℝ), 0 < e ∧ ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign), ∀ x ∈ Set.Icc 2 M, e ≤ H.T sign x

theorem MathlibNt.SieveTheory.exists_caseA_scalar_constant_for_fixed_q (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {q : ℕ} (hq : 2 ≤ q) {d Δ K : ℝ} (hd : 2 < d) (hK : 0 < K) : ∃ (A : ℝ), 0 < A ∧ ∀ (n p : ℕ) (x : ℝ), p = ⌈↑q ^ (1 / x)⌉₊ → 2 ≤ x → suzukiSourceL (↑p) K ^ (⌊x - 2⌋₊ + 1) / ↑(⌊x - 2⌋₊ + 1).factorial * Real.exp (suzukiSourceL (↑p) K) ≤ A * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H n (↑q) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑q) d) K x

theorem MathlibNt.SieveTheory.exists_caseA_scalar_constant_for_fixed_q_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {q : ℕ} (hq : 2 ≤ q) {d Δ K : ℝ} (hd : 2 < d) (hK : 0 < K) : ∃ (A : ℝ), 0 < A ∧ ∀ (S : BoundingSieve), SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (n p : ℕ) (x : ℝ), p = ⌈↑q ^ (1 / x)⌉₊ → 2 ≤ x → suzukiSourceL (↑p) K ^ (⌊x - 2⌋₊ + 1) / ↑(⌊x - 2⌋₊ + 1).factorial * Real.exp (suzukiSourceL (↑p) K) ≤ A * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H n (↑q) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑q) d) K x

Fixed-quotient scalar comparison with its coefficient chosen before the varying sieve. Uniformity is paid by the local-product hypothesis at K.

theorem MathlibNt.SieveTheory.exists_claim145SmallDCaseAScalarComparison_of_fixedDmin (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (Dmin : ℕ) {d Δ K C1 ΘK : ℝ} (hd : 2 < d) (hK : 0 < K) (hCaseA_lt : ∀ (q : ℕ), 2 ≤ q → Real.log ↑q ≤ C1 * K ^ ΘK → q < Dmin) : ∃ (C145 : ℝ), 0 < C145 ∧ Claim145SmallDCaseAScalarComparison S H d Δ C145 K C1 ΘK

A fixed finite quotient range admits one scalar constant, uniform in the depth, quotient, natural-ceiling cutoff, and real coordinate.

theorem MathlibNt.SieveTheory.exists_claim145SmallDCaseAScalarComparison_of_fixedDmin_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (Dmin : ℕ) {d Δ K C1 ΘK : ℝ} (hd : 2 < d) (hK : 0 < K) (hCaseA_lt : ∀ (q : ℕ), 2 ≤ q → Real.log ↑q ≤ C1 * K ^ ΘK → q < Dmin) : ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (S : BoundingSieve), SwitchingPrinciple.HasDimensionOneLocalProductBound S K → Claim145SmallDCaseAScalarComparison S H d Δ C145 K C1 ΘK

Uniform-in-sieve fixed-Dmin scalar producer. Its finite maximum is formed before S; the local-product contract is consumed only pointwise.