Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Multiplicity-weighted reciprocal-square summability for all actual critical-strip zeta zeros

Proved
ConnesRZ.actual_zero_reciprocal_square_summable

by waitingintime · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

connes-weilriemann-zetasummabilityzero-counting

Let Z={ρ∈C:ζ(ρ)=0, 0<Re⁡ρ<1}Z=\{\rho\in\mathbb C:\zeta(\rho)=0,\ 0<\operatorname{Re}\rho<1\}Z={ρ∈C:ζ(ρ)=0, 0<Reρ<1} and let mρm_\rhomρ​ be the analytic multiplicity of the actual Riemann-zeta zero ρ\rhoρ. Then the nonnegative family

(mρ1+∣γρ∣2)ρ∈Z,γρ=ρ−1/2i,\left(\frac{m_\rho}{1+|\gamma_\rho|^2}\right)_{\rho\in Z},\qquad \gamma_\rho=\frac{\rho-1/2}{i},(1+∣γρ​∣2mρ​​)ρ∈Z​,γρ​=iρ−1/2​,

is unconditionally summable. The carrier is the full set of actual critical-strip zeros, all analytic multiplicities are retained, and no RH, positivity, abstract-zero-configuration, or zero-count assumption appears in the statement.

This is the summable majorant used by the independently checked Connes–Weil Green-column frontier to control all high-ordinate actual Green reciprocals. The proof uses the already proved actual-zeta unit-window count, while the physical Green metric realization remains a separate obligation.

Preamble
import Mathlib
import Definitions.Def_ConnesRZ_weil_defs
Formal statement
theorem ConnesRZ.actual_zero_reciprocal_square_summable : Summable (fun ρ : {z : ℂ // ConnesRZ.IsCriticalZero z} =>
      (ConnesRZ.zeroMult ρ.1 : ℝ) / (1 + Complex.normSq ((ρ.1 - 1 / 2) / Complex.I))) := by sorry
Source
Anthropic formal-math e1a4e6508154ea59f030480661590a9fe3018011, zeta23/Zeta23/WeilEF/ZeroSummability.lean, zero_sum_inv_sq_gen and zero_sum_inv_sq; reused with license and exact carrier/multiplicities in monocap-tech/weil, WeilDefect/Connes/ActualGreenSummability.lean, actual_zero_reciprocal_square_summable. Local-count prerequisite: https://prove2.me/theorems/2abaa392-a81f-480c-8c0f-d476f67838ae . Literature/source audit addendum (2026-10-11): The exact unchanged native theorem is WeilDefect.ConnesNative.actual_zero_reciprocal_square_summable. The ConnesRZ graph name is a recovered named export, rather than a literal declaration in ActualGreenSummability.lean. The exact graph type was independently checked in Lean, preserving the actual zeta-zero carrier and multiplicities. Literature/source audit addendum (2026-10-11; COR-15): Exact native software custody, independently verified from retained local Git objects: monocap-tech/weil d73d0e7f1477c934a3a8f8b01012852128b977bb, WeilDefect/Connes/ActualGreenSummability.lean, SHA256 0d1e244e5579f71293661e2d83f397f44faafcb11348a0ad15583ac407b9b8c0. Public availability of these historical pins has not been checked; this addendum verifies local source bytes and preserves the original source ancestry.
Human review
  • Endorsed by Shuze Chen · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by waitingintime · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me