theorem MathlibNt.SieveTheory.log_two_pos : 0 < Real.log 2

theorem MathlibNt.SieveTheory.bound_K (K : ℝ) (hK : 2 ≤ K) : 1 + K / Real.log 2 ≤ K * (1 + 1 / Real.log 2)

theorem MathlibNt.SieveTheory.log_bound (K : ℝ) (hK : 2 ≤ K) : Real.log (1 + K / Real.log 2) ≤ Real.log K + Real.log (1 + 1 / Real.log 2)

theorem MathlibNt.SieveTheory.log_bound_lower (K : ℝ) (hK : 2 ≤ K) : Real.log K - Real.log (Real.log 2) ≤ Real.log (1 + K / Real.log 2)

theorem MathlibNt.SieveTheory.abs_B_bound (K : ℝ) (hK : 2 ≤ K) : have B := -Real.log (Real.log 2) + Real.log (1 + K / Real.log 2); |B| ≤ Real.log K + |Real.log (1 + 1 / Real.log 2)| + 2 * |Real.log (Real.log 2)|

theorem MathlibNt.SieveTheory.abs_logQ_bound (K : ℝ) (hK : 2 ≤ K) : have Q := Real.log 2 / (1 + K / Real.log 2); |Real.log Q| ≤ Real.log K + |Real.log (1 + 1 / Real.log 2)| + 2 * |Real.log (Real.log 2)|

theorem MathlibNt.SieveTheory.q0_bound (K : ℝ) (hK : 2 ≤ K) (Θ : ℝ) (hΘ : 1 ≤ Θ) (hB : |-Real.log (Real.log 2) + Real.log (1 + K / Real.log 2)| ≤ Real.log K + (|Real.log (1 + 1 / Real.log 2)| + 2 * |Real.log (Real.log 2)|)) (hQ_pos : |Real.log (1 / (1 / Real.log 2 * (1 + K / Real.log 2)))| ≤ Real.log K + (|Real.log (1 + 1 / Real.log 2)| + 2 * |Real.log (Real.log 2)|)) : have C := |Real.log (1 + 1 / Real.log 2)| + 2 * |Real.log (Real.log 2)|; have C_q0 := max 6 (max (C + 2) (max (C + 9) (Real.exp 1 + 2))); have B := -Real.log (Real.log 2) + Real.log (1 + K / Real.log 2); have Q := 1 / (1 / Real.log 2 * (1 + K / Real.log 2)); have q0 := max 6 (max (|B| + 2) (max (9 + |Real.log Q|) (Real.exp 1 + 2))); q0 ≤ Θ * Real.log K + C_q0

theorem MathlibNt.SieveTheory.claim145_caseB_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hTheta : 1 ≤ Θ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (S : BoundingSieve), Claim145CaseBClosed S H d Δ Θ C1min CB

Claim 14.5 Case B with the analytic constants selected uniformly before the varying bounding sieve. The proof's threshold construction uses only the Section-13 source contract and the scalar parameters; S first enters when the pointwise local-product hypothesis is consumed.

theorem MathlibNt.SieveTheory.claim145_caseB_uniform (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hTheta : 1 ≤ Θ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ Claim145CaseBClosed S H d Δ Θ C1min CB

Compatibility specialization of the uniform-in-S Case-B theorem.