Complete order-independent actual nonprincipal Goldbach smoothed-prime explicit formula

Proved

Helfgott.actual_primitive_nonprincipal_unordered_explicit_formula

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

explicit-formulasgoldbachl-functionsmajor-arcs

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

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

Every zero and its full positive analytic multiplicity is included. The sum is independent of ordering, and all prime, smoothing and contour integrals are complete. No contour admissibility, zero-count, decay or convergence assumption is imposed. This supplies the full nonprincipal 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_primitive_nonprincipal_unordered_explicit_formula (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (hp : χ.IsPrimitive) (hχ : χ ≠ 1)
    (η : ℝ → ℝ) (hη : η=Helfgott.etaPlus ∨ η=Helfgott.etaStar) (x β : ℝ) (hx : 0 < x) :
    let Z := {ρ : ℂ | -(1/2 : ℝ) ≤ ρ.re ∧ ρ.re ≤ 2 ∧ χ.LFunction ρ=0}
    let g : Z → ℂ := fun ρ => (analyticOrderNatAt χ.LFunction ρ : ℂ)*(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 χ.LFunction s/χ.LFunction s)
    Summable (fun ρ : Z => ‖g ρ‖) ∧
      HasSum g (((1/(2*Real.pi) : ℝ) • ∫ t : ℝ,F (-(1/2 : ℂ)+(t : ℂ)*I))-
        ∑' n : ℕ,χ (n : ZMod q)*((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