noncomputable def AnalyticNumberTheory.LargeSieve.eq19AlphaQ0 (x level : ℕ) : ℝ

Real source conductor before the rounding of L.

Equations

• AnalyticNumberTheory.LargeSieve.eq19AlphaQ0 x level = 2 ^ level * Real.log ↑x ^ 100

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_source_geometry {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) : chen1973Lemma6Eq19SourceQ L level = 2 * chen1973Lemma6Eq19SourceD L level ∧ chen1973Lemma6Eq19SourceQ L level ≤ 2 * (B * 2 ^ k) ∧ ↑(chen1973Lemma6Eq19SourceQ L level) ≤ eq19AlphaQ0 x level ∧ eq19AlphaQ0 x level ≤ 2 * ↑(chen1973Lemma6Eq19SourceQ L level)

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_I_log90 {x level : ℕ} (hu : 1 ≤ Real.log ↑x) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : 1 ≤ chen1973Lemma6Equation20Ilx x level ∧ chen1973Lemma6Equation20Ilx x level * Real.log ↑x ^ 90 ≤ eq19AlphaQ0 x level

The exponential source I leaves ninety logarithmic powers after division by Q0. The log-log condition is uniform in every dyadic level.

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_loglog_eventually : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (level : ℕ), 1 ≤ Real.log ↑x ∧ 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_source_weight_budget : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k : ℕ), Chen1973Lemma6Eq19SourceParameters x L B lastD level k → chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD → chen1973Lemma6Eq19I x L level ^ 2 * Real.log ↑x ^ 90 ≤ 2 * ↑(chen1973Lemma6Eq19SourceQ L level) ∧ ↑(chen1973Lemma6Eq19SourceQ L level) * Real.log ↑x ^ 100 * chen1973Lemma6Eq19I x L level ^ 2 ≤ ↑(chen1973Lemma6Eq19PrintedHeight x level)

True-height source payment, already strong enough for dyadic alpha smallness. No cellwise existential or conclusion-shaped analytic source is used.

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_printedHeight_logs {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (hQ : chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD) (hcap : ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2)) (htt : 60 ≤ Real.log (Real.log (eq19AlphaQ0 x level))) : 2 ≤ chen1973Lemma6Eq19PrintedHeight x level ∧ 1 + Real.log ↑(chen1973Lemma6Eq19PrintedHeight x level + 1) ≤ 120 * Real.log ↑x ∧ Real.log ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 4 * Real.log ↑x

Height logarithms are controlled only after imposing the honest source conductor cap. No fixed-level convention is hidden in this statement.

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_ratios {u W D Q H : ℝ} (hu : 1 ≤ u) (hW : 1 ≤ W) (hD : 0 < D) (hH : 0 < H) (hQD : Q = 2 * D) (hWQ : W ^ 2 * u ^ 90 ≤ 2 * Q) (hWH : Q * u ^ 100 * W ^ 2 ≤ H) : W ^ 2 * (Q / H + 1 / D) ≤ 5 / u ^ 90 ∧ W ^ 2 * Q ^ 2 / H ^ 2 ≤ 1 / u ^ 200

Algebraic consequences of the source weight ledger.

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_budget_scalar {u W D Q H t n p ell a : ℝ} (hu : 1 ≤ u) (hQ : 0 ≤ Q) (hH : 0 < H) (ht : 1 ≤ t) (hn : 0 ≤ n) (hnle : n ≤ 2 * t) (hp : 0 ≤ p) (hple : p ≤ 4 * u) (hell : 0 ≤ ell) (hellle : ell ≤ 120 * u) (ha : 0 ≤ a) (hale : a ≤ 1 / H) (hmain : W ^ 2 * (Q / H + 1 / D) ≤ 5 / u ^ 90) (hrem : W ^ 2 * Q ^ 2 / H ^ 2 ≤ 1 / u ^ 200) : W ^ 2 * (2 * chen1973Lemma6Eq14DyadicConstant * (Q / H + 1 / D) * ell ^ 5 + 2 * Q * (40 * n * √Q * p * a * ell) ^ 2) ≤ (10 * chen1973Lemma6Eq14DyadicConstant * 120 ^ 5 + 2 * (40 * 2 * 4 * 120) ^ 2) / u ^ 80 * t ^ 2

The complete weighted dyadic budget is small, not merely integrable.

noncomputable def AnalyticNumberTheory.LargeSieve.eq19AlphaBudgetConstant : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.eq19AlphaBudgetConstant = 10 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq14DyadicConstant * 120 ^ 5 + 2 * (40 * 2 * 4 * 120) ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.eq19AlphaNumeratorConstant : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.eq19AlphaNumeratorConstant = √(27 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19SharpConstant * AnalyticNumberTheory.LargeSieve.eq19AlphaBudgetConstant)

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_pair_shape {Q Y D σ : ℝ} (hQ : 0 ≤ Q) (hY : 1 ≤ Y) (hD : 1 ≤ D) (hQY : Q ≤ 2 * Y) (hσ : 1 ≤ σ) : (Q + Y / D) * Y ^ (1 - 2 * σ) ≤ 3

theorem AnalyticNumberTheory.LargeSieve.eq19Alpha_actual_numerator_small : ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq19SourceParameters x L B lastD level k → chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD → ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → ∀ (v : ℝ), 0 ≤ v → chen1973Lemma6A x L level B k m (chen1973Lemma6Eq19PrintedHeight x level) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) ≤ eq19AlphaNumeratorConstant / Real.log ↑x ^ 40 * (1 + v)

Uniform linear-v numerator bound using the new dyadic moments and the true printed height. The extra geometric cap is explicit.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6A_line_continuous {x L level B k m H D Q : ℕ} (σ : ℝ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : Continuous fun (v : ℝ) => chen1973Lemma6A x L level B k m H (↑σ + ↑v * Complex.I)

Continuity of the actual numerator from its finite sums and primitive L-functions.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_alpha_integrable_and_small : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq19SourceParameters x L B lastD level k → chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD → ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → MeasureTheory.IntegrableOn (fun (v : ℝ) => chen1973Lemma6A x L level B k m (chen1973Lemma6Eq19PrintedHeight x level) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) / chen1973Lemma6Eq17CorrectedKernel x (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I)) (Set.Ioi 0) MeasureTheory.volume ∧ chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m (chen1973Lemma6Eq19PrintedHeight x level) ≤ C / Real.log ↑x ^ 22

Uniform smallness of the actual corrected alpha integral at the printed height. Only source parameters and explicit geometric caps remain.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_alpha_contribution_small : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq19SourceParameters x L B lastD level k → chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD → ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq20CorrectedFirstIntegral x L level B k m (chen1973Lemma6Eq19PrintedHeight x level) ≤ C * ↑x / Real.log ↑x ^ 20

The actual alpha contribution, including the outer factor from corrected (17).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation19_small_alpha_actual_beta : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), ∀ (x : ℕ), X₀ ≤ ↑x → ∀ (L B lastD level k m : ℕ), Chen1973Lemma6Eq19SourceParameters x L B lastD level k → chen1973Lemma6Eq19SourceQ L level ≤ 2 * lastD → ↑(chen1973Lemma6Eq19SourceQ L level) ≤ 2 * ↑x ^ (1 / 2) → chen1973Lemma6NmBlockActual x L level B k m ≤ C * ↑x / Real.log ↑x ^ 20 + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m (chen1973Lemma6Eq19PrintedHeight x level)

Physical wiring into the actual cell. Only beta remains on the right; this is not a claim that equation (19) as a whole has been paid.