theorem AnalyticNumberTheory.LargeSieve.PanLow.primeFactors_card_le_log_of_le {m : ℕ} {X : ℝ} (hm : 0 < m) (hmX : ↑m ≤ X) : ↑m.primeFactors.card ≤ (Real.log 2)⁻¹ * Real.log X

Positive modulus only. The coarse log N bound is enough; no arithmetic or analytic estimate stronger than the existing omega bound is used.

theorem AnalyticNumberTheory.LargeSieve.PanLow.low_budget_scalar {X L A W R U b K c : ℝ} (hX : 0 < X) (hL : 1 ≤ L) (hA0 : 0 ≤ A) (hW0 : 0 ≤ W) (_hR0 : 0 ≤ R) (hK : 0 ≤ K) (hc : 0 ≤ c) (hA : A ≤ X ^ (2 / 3)) (hW : W ≤ c * L) (hR : R ≤ L ^ b) (hlog : L ^ (U + b + 1) ≤ X ^ (1 / 3)) : R * (K * X / L ^ (U + b + 2) * (1 + L) + A * W) ≤ (2 * K + c) * X / L ^ U

Pure scalar payment with an explicit elementary log-versus-power premise. The eventual theorem below discharges that premise before quantifying cells.

theorem AnalyticNumberTheory.LargeSieve.PanLow.exists_low_budget_payment (U b K : ℝ) (_hU : 0 < U) (_hb : 0 ≤ b) (hK : 0 < K) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (m A₂ Q : ℕ), 1 ≤ m → ↑m ≤ √↑N → ↑A₂ ≤ ↑N ^ (2 / 3) → ↑Q ≤ Real.log ↑N ^ b → ↑Q * (K * ↑N / Real.log ↑N ^ (U + b + 2) * (1 + Real.log ↑N) + ↑A₂ * ↑m.primeFactors.card) ≤ C * ↑N / Real.log ↑N ^ U

All constants and the threshold precede N, m, A₂ and Q. s=U+b+2. The only limiting input is Mathlib's log-versus-positive-power little-o.