Prove2Me

Theorem A at fixed λ∈(0,1)\lambda \in (0,1) for an abstract zero configuration

Proved
Zeta23.Assembly.thmA_abstract

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

number-theoryriemann-zetazero-countingzeta23

The ε\varepsilon-form of Theorem A at a fixed mollifier exponent, for an abstract zero configuration ZZ (any locally finite multiset of points in the strip 0≤β≤10 \le \beta \le 1, symmetric under ρ↦1−ρˉ\rho \mapsto 1 - \bar\rho). Here N(T,2T)N(T,2T) counts zeros of ZZ with ordinate in (T,2T](T,2T] with multiplicity, N0∗(T,2T)N_0^*(T,2T) counts distinct zeros on the line β=1/2\beta = 1/2, and H(λ):=2−1/λ−λ/3H(\lambda) := 2 - 1/\lambda - \lambda/3.

Assume: the published analytic inputs PaperInputs Z (explicit formula H-EF, Riemann–von Mangoldt H-RvM, Chebyshev–Mertens, Montgomery–Vaughan, Stirling facts for Γ′/Γ\Gamma'/\Gamma); a valid parameter pack PP (taper profile, 0<λ≤10 < \lambda \le 1, w≥1w \ge 1) with λ<1\lambda < 1; the trace asymptotics [thm:traces] for the prime-side traces (ThmTracesHyp P Z); eventually in TT: the block inputs of prop:block, the tail inputs of prop:tail with θ0(T)≤C l Tλ/2−1\theta_0(T) \le C\, l\, T^{\lambda/2 - 1}, the boundary count N(I′∖I)≤CT lN(I' \setminus I) \le C \sqrt{T}\, l, the explicit-formula bridge Gzero=GprimeG^{\mathrm{zero}} = G^{\mathrm{prime}} ([eq:Gdef]), and the taper normalization 1−2w/L≤a≤11 - 2w/L \le a \le 1 ([eq:abdef]); and finally ET→0\mathcal{E}_T \to 0.

Conclusion:

∀ε>0, ∃T0, ∀T≥T0:(H(λ)−ε) N(T,2T)  ≤  N0∗(T,2T).\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).

This is the specialization Err:=ET\mathrm{Err} := \mathcal{E}_T (P.calE) of thmA_abstract_err. It is the summit of the Zeta23.Assembly module: Zeta23.thmA_lam_of_traces instantiates it with the actual zeta zeros, after which the λ→1−\lambda \to 1^- and dyadic steps yield the headline constant 2/32/3.

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 (Z : ZeroConfig) (H : PaperInputs Z) (P : Params) (hP : P.Valid)
    (hlam : P.lam < 1) (hTr : ThmTracesHyp P Z)
    (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 P.calE 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#L1284-L1296

View graph