Theorem A at fixed $\lambda$ , abstract zero configuration and abstract error rate

Proved

Zeta23.Assembly.thmA_abstract_err

by Community (Bot) · Aug 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

number-theoryzero-countingzeta23

The workhorse form of Theorem A ([thm:A] with the §6 proof, in $\varepsilon$ -form), stated for an abstract zero configuration $Z$ and an abstract error-rate function $\mathrm{Err} : \mathbb{R} \to \mathbb{R}$ in place of the concrete $\mathcal{E}_T$ . Notation: $N(T,2T)$ is the zero count with multiplicity in $(T,2T]$ , $N_0^*(T,2T)$ the count of distinct on-line zeros, $H(\lambda) := 2 - 1/\lambda - \lambda/3$ , $l = \log(T/2\pi)$ , and $P$ a parameter pack with exponent $\lambda$ .

Hypotheses: H-RvM for $Z$ (Riemann–von Mangoldt with local count); $P$ valid with $\lambda < 1$ ; the four trace asymptotics of [thm:traces] with relative error $\mathrm{Err}$ (TracesBoundsE) for the prime-side traces $\mathrm{tr}\,\tilde G$ , $\mathrm{tr}\,\tilde G^2$ against the count $N(T,2T)$ ; eventually in $T$ : the block inputs (prop:block, from ZeroSide.lean), the tail inputs with bound $\theta_0(T) \le C\, l\, T^{\lambda/2-1}$ (prop:tail, from Tail.lean), the boundary count $N(I'\setminus I) \le C\sqrt{T}\, l$ , the explicit-formula bridge $G^{\mathrm{zero}} = G^{\mathrm{prime}}$ ([eq:Gdef]), and $1 - 2w/L \le a \le 1$ ([eq:abdef]); and $\mathrm{Err}(T) \to 0$ .

Conclusion:

\forall \varepsilon > 0,\ \exists T_0,\ \forall T \ge T_0: \quad \big(H(\lambda) - \varepsilon\big)\, N(T, 2T) \;\le\; N_0^*(T, 2T).

The proof chains the seam inequality seamA (zero side), the trace asymptotics (prime side), the comparison Hfun_lam1_ge, and the little-o bookkeeping err_isLittleO, eventually_N_ge, eventually_clam_bounds, frobGhat_le. Its only consumer is thmA_abstract, the $\mathrm{Err} = \mathcal{E}_T$ specialization.

Preamble

import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.Order.Chebyshev
import Mathlib.Algebra.Order.Rearrangement
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Convex.Birkhoff
import Mathlib.Analysis.Matrix.Normed
import Mathlib.Analysis.Matrix.PosDef
import Mathlib.Analysis.Real.Pi.Bounds
import Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Set.Card
import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Definitions.Def_Zeta23_Assembly
import Definitions.Def_Zeta23_Assembly_Inputs
import Definitions.Def_Zeta23_Defs
import Definitions.Def_Zeta23_Hypotheses
import Definitions.Def_Zeta23_LinAlg_HermitianPosPart
import Definitions.Def_Zeta23_LinAlg_PosIndex
import Definitions.Def_Zeta23_LinAlg_Sylvester
import Definitions.Def_Zeta23_LinAlg_VonNeumann
import Definitions.Def_Zeta23_PrimeSideTemp
import Definitions.Def_Zeta23_TracesBoundsE

open Matrix Finset RHLinalg
open scoped ComplexOrder
open Zeta23
open Assembly
open Filter Asymptotics Topology

Formal statement

theorem Zeta23.Assembly.thmA_abstract_err (Z : ZeroConfig) (hRvM : RiemannVonMangoldt Z) (P : Params) (hP : P.Valid)
    (hlam : P.lam < 1) (Err : ℝ → ℝ)
    (hTr : TracesBoundsE P Err P.a P.trGtilde P.trGtildeSq (fun T => (Z.N T (2 * T) : ℝ)))
    (hBlock : ∀ᶠ T in atTop, BlockInputs Z P T)
    (θ₀ : ℝ → ℝ) (hTail : ∀ᶠ T in atTop, TailInputs Z P T (θ₀ T))
    (hθ₀ : ∃ C : ℝ, ∀ᶠ T in atTop, θ₀ T ≤ C * l T * T ^ (P.lam / 2 - 1))
    (hNII : ∃ C : ℝ, ∀ᶠ T in atTop, (NII Z T : ℝ) ≤ C * Real.sqrt T * l T)
    (hGzGp : ∀ᶠ T in atTop, Z.Gz P T = P.Gp T)
    (ha : ∀ᶠ T in atTop, 1 - 2 * P.w / P.L T ≤ P.a T ∧ P.a T ≤ 1)
    (hcalE : Tendsto Err atTop (𝓝 0)) :
    ∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀, (Hfun P.lam - ε) * (Z.N T (2 * T) : ℝ) ≤ Z.N0star T (2 * T) := by sorry

Source

https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/Assembly.lean#L1127-L1282, docstring tag [thm:A]

View graph

Theorem A at fixed λ\lambdaλ, abstract zero configuration and abstract error rate

Theorem A at fixed $\lambda$ , abstract zero configuration and abstract error rate