theorem ChenEq18.card_primeFactors_mul_log_le {n : ℕ} {R K : ℝ} (hn : 1 ≤ n) (hnR : ↑n ≤ R) (hK : 1 ≤ K) : ↑n.primeFactors.card * Real.log K ≤ K * Real.log K + Real.log R

Elementary prime-factor splitting, uniform in the integer below R.

theorem ChenEq18.log_three_lt_four_thirds : Real.log 3 < 4 / 3

theorem ChenEq18.eventually_aux : ∀ᶠ (t : ℝ) in Filter.atTop, 1 ≤ t ∧ t * Real.exp (t / 2) ≤ Real.exp t / 4

An elementary exponential-domination cutoff in the log-log coordinate.

theorem ChenEq18.uniform_prime_factor_bound : ∃ (R₀ : ℝ), ∀ (R : ℝ), R₀ ≤ R → ∀ (n : ℕ), 1 ≤ n → ↑n ≤ R → 3 ^ n.primeFactors.card ≤ Real.exp (3 * Real.log R / Real.log (Real.log R))

The uniform form of Chen's equation (18); the threshold precedes n.

theorem AnalyticNumberTheory.LargeSieve.chenEq18_actual_conductor_bounds {x L level d : ℕ} (hd : d ∈ chen1973Lemma6ConductorBlock x L level) : 1 ≤ d ∧ d ≤ L * 2 ^ level

Includes level zero, and does not require any branch or pair parameters.

theorem AnalyticNumberTheory.LargeSieve.chenEq18_actual_W_sq_uniform : ∃ (R₀ : ℝ), ∀ (R : ℝ), R₀ ≤ R → ∀ (x L level : ℕ), ↑(L * 2 ^ level) ≤ R → chen1973Lemma6Eq19I x L level ^ 2 ≤ Real.exp (6 * Real.log R / Real.log (Real.log R))

The existing Eq19I is a finite maximum W, NOT the printed exponential I. This theorem supplies the missing upper bridge without changing that definition.

theorem AnalyticNumberTheory.LargeSieve.chenEq18_actual_W_sq_le_source_I : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L level : ℕ), ↑L ≤ Real.log ↑x ^ 100 → chen1973Lemma6Eq19I x L level ^ 2 ≤ Real.exp (6 * Real.log (2 ^ level * Real.log ↑x ^ 100) / Real.log (Real.log (2 ^ level * Real.log ↑x ^ 100)))

A single x-threshold works before ALL actual-cell parameters, including level zero. Here Q₀ = 2^level (log x)^100, and the right-hand side is literally the printed I.