theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primeRegion_log_y {x : ℕ} (hx : 3 ≤ x) {pp : ℕ × ℕ} (hpp : pp ∈ chen1973Lemma6Eq21PrimeRegion x) : 1 < ↑x / (↑pp.1 * ↑pp.2) ∧ Real.log ↑x / 3 ≤ Real.log (↑x / (↑pp.1 * ↑pp.2))

Source-region geometry, extracted without changing the analytic-payments module.

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21UniformBudgetConstant (r : ℕ) : ℝ

A fixed, explicit finite coefficient; no cell parameter occurs here.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21UniformBudgetConstant r = (2 + ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * ↑j.factorial) * 104 ^ (r + 1)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_budget_uniform {x d : ℕ} (hu : 4 ≤ Real.log ↑x) (hd : 1 ≤ ↑d) (hdu : ↑d ≤ Real.log ↑x ^ 100) (r : ℕ) : have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; have D := 1 + Real.log (↑d * (1 + a)); have σ := chen1973Lemma6Eq21Sigma x; (σ⁻¹ + Real.log a) * D ^ r + ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * D ^ (r - j) * (↑j.factorial / ↑N ^ (j + 1)) ≤ chen1973Lemma6Eq21UniformBudgetConstant r * (1 + Real.log (Real.log ↑x)) ^ (r + 1)

Uniform arithmetic bound for the already-integrated kernel budget. We deliberately discard the helpful order denominators and use a loose fixed coefficient, rather than impose an integral-shaped premise.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_eventually_loglog_pow_absorb (C : ℝ) (n : ℕ) : ∀ᶠ (x : ℕ) in Filter.atTop, C * (1 + Real.log (Real.log ↑x)) ^ n ≤ Real.log ↑x

Every fixed polynomial in 1 + log log x is absorbed by log x. The cutoff is independent of all conductor and prime-pair cells.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_primitiveVerticalEstimate_one_eventually_of_logDerivative_bound {M : ℝ} (hM : 0 ≤ M) (r : ℕ) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d) (t : ℝ), ‖chen1973PrimitiveLDeriv d (chen1973Lemma6Eq21Line x t) χ / chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ‖ ≤ M * (1 + Real.log (↑d * (1 + |t|))) ^ r) → Chen1973Lemma6Eq21PrimitiveVerticalEstimate 1 x L B k m

A single pre-cell threshold absorbs the real vertical-integral budget into PrimitiveVerticalEstimate 1. The only analytic input is the actual full-height pointwise L'/L bound; it is retained as a hypothesis, not claimed proved.