Complete order-independent actual principal zeta Goldbach smoothed-prime explicit formula

Proved

Helfgott.actual_zeta_unordered_explicit_formula

by raresbuhai · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

explicit-formulasgoldbachl-functionsmajor-arcs

Let $\eta$ be either actual Goldbach smoothing $\eta_+$ or $\eta_*$ , let $x>0$ , and let $\beta\in\mathbb R$ . Put $H(s)=(s-1)\zeta(s)$ with $H(1)=1$ , $M_\beta(s)=\mathcal M[\eta(t)e^{2\pi ix\beta t}](s)$ , and $F(s)=x^sM_\beta(s)(-\zeta'(s)/\zeta(s))$ . The complete weighted zero series is absolutely convergent, and its unconditional sum is

\sum_{\substack{H(\rho)=0\\-1/2\le\Re\rho\le2}}m_\rho x^\rho M_\beta(\rho)=x\widehat\eta(-x\beta)+\frac1{2\pi}\int_{-\infty}^{\infty}F(-1/2+it)\,dt-\sum_{m=0}^\infty\Lambda(m)\eta(m/x)e^{2\pi im\beta}.

Every zero and its full analytic multiplicity is included. The Fourier main term is the exact principal pole contribution. All zero, prime and smoothing sums and contour integrals are complete, with no ordering or admissibility assumption. This supplies the order-independent principal explicit formula for the Goldbach major arcs; certified numerical zero contributions and the final residual remain separate.

Preamble

import Definitions.Def_Helfgott_Smoothings
import Definitions.Def_CircleMethod_char
import Mathlib.Analysis.MellinTransform
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.Analysis.Analytic.Order
open MeasureTheory Set Filter Complex
open scoped Topology

Formal statement

theorem Helfgott.actual_zeta_unordered_explicit_formula (η : ℝ → ℝ) (hη : η=Helfgott.etaPlus ∨ η=Helfgott.etaStar) (x β : ℝ) (hx : 0 < x) :
    let H := DirichletCharacter.LFunctionTrivChar₁ 1
    let Z := {ρ : ℂ | -(1/2 : ℝ) ≤ ρ.re ∧ ρ.re ≤ 2 ∧ H ρ=0}
    let g : Z → ℂ := fun ρ => (analyticOrderNatAt H ρ : ℂ)*(x : ℂ)^(ρ : ℂ)*
      mellin (fun r : ℝ => (η r : ℂ)*CircleMethod.e (x*β*r)) ρ
    let F : ℂ → ℂ := fun s => (x : ℂ)^s*
      mellin (fun r : ℝ => (η r : ℂ)*CircleMethod.e (x*β*r)) s*
        (-deriv riemannZeta s/riemannZeta s)
    Summable (fun ρ : Z => ‖g ρ‖) ∧
      HasSum g ((x : ℂ)*FourierTransform.fourier (fun r : ℝ => (η r : ℂ)) (-(x*β))+
        ((1/(2*Real.pi) : ℝ) • ∫ t : ℝ,F (-(1/2 : ℂ)+(t : ℂ)*I))-
        ∑' n : ℕ,((ArithmeticFunction.vonMangoldt n : ℂ)*
          (η ((n : ℝ)/x) : ℂ)*CircleMethod.e ((n : ℝ)*β))) := by sorry

Source

Helfgott, Major arcs for Goldbach’s problem, https://arxiv.org/abs/1305.2897 and https://arxiv.org/abs/1312.7748. Mathlib Fourier/Mellin and L-function contributors including David Loeffler; Jensen, orders, divisors, canonical decomposition and Borel-Caratheodory contributors including Stefan Kebekus; gamma, Euler series, residue, improper integral and unconditional summation contributors. Complete original full actual contour estimates, zero-band absolute convergence and unordered explicit-formula assembly. Written by Codex.

View graph