RiemannZetaZeros: cumulative 0.6734775223 variant and a 25-mode certificate-class obstruction #7277

Requested cumulative variants, not a dyadic scope change

Please consider Jonas J. Gebendorfer, Compatible local windows and a certified lower bound for simple critical-line zeros, audit revision8 September2026, manuscript DOI reference, with the full stand-alone manuscript and complete fresh certificate replay attached.

The existing RiemannZetaZeros module was freshly read. Its simple_prop_lt and related assertions count zeros in (T,2T]. This manuscript's theorem counts in (0,T]. A cumulative liminf does not itself imply the same dyadic liminf; please add/review a cumulative variant rather than silently marking the existing dyadic statement solved.

Let N(T) count all nontrivial zeta zeros of ordinate0<Im(rho)<=T, with multiplicity; N0^s(T) counts only simple zeros on Re(rho)=1/2. The exact unconditional statement is

liminf_(T->infinity) N0^s(T)/N(T) >= 8269551442741204889710953/12278882618209750000000000 > 0.6734775223.

It is asymptotic, not a lower bound for every finite T. No RH, all-r Dirichlet-family extension, or global0.6739 result is asserted.

Analytic and computational proof dependencies

The external analytic premises are the fixed-function unconditional weighted pair-correlation formula of Baluyot–Goldston–Suriajaya–Turnage-Butterbaugh, Lemma5 (Acta Arith.214,2024), and Riemann–von Mangoldt. Their exact roles are separated from the finite checks. The manuscript writes out fixed Q,Q'' unweighting (with Lamzouri attribution), a signed multiset/Hilbert–Schmidt reduction retaining the clipped spectral remainder, AMTOPA's credited trace-corrected band profile, nine universal local inequalities, a complete compatible three-window cover, exact495-point aggregation and polyhedral verification, offset averaging, smoothing and the order of limits. The reproduced programs do not mechanically verify those written analytic arguments.

The paper also proves a distinct certificate-class obstruction: for its complete normalized nonnegative25-mode cosine-window class, any universal clipped-Gram block inequality with nonnegative gap prices and0<R<m has certificate value(m*(2-C(f))-sum prices)/(m-R)<0.674034. This is neither an upper bound on the actual zero proportion nor a claim that the class supremum is attained/sharp. Both statements should keep their exact definitions and quantifiers.

Complete fresh reproduction,13 October2026

With Python3.12, python-flint0.9.0 and g++, the unchanged full revision entrypoint passed: six byte-identical regenerated Arb tables; all nine local subdivisions; complete37,328-box sublevel cover, outward coarsening and exact281-box compatible join; the restricted eight-gap proof; all141 regenerated rational projection vertices; coefficient/manuscript audits and negative controls. 58,577,037 subdivision nodes were freshly rerun, taking about880 seconds here. This is a complete fresh local/coverage replay, not just a static hash check of the old report. The original44 proof-input files and archive remain unchanged. The public supplement retains both the historical evidence and separately identified new run.

The proposed four-window0.0078711/0.00787132 targets fail at the included exact rational counterpoint; they are not promoted. The later0.6739 frontier remains separate and open in the relevant handoff.

Literature status and formalization scope

This is not a current-record or first-priority claim. Knausgård, arXiv:2610.08965v1,6 October2026, references15–17, cites the Gebendorfer drafts; Section7 expressly discusses the0.674034 class obstruction. That paper announces a larger numerical lower bound and describes the earlier numerical reports as unrefereed. Its citation is external attribution, not a verification of this supplement; its claimed Lean result has additional local-certificate axioms as explicitly disclosed in its abstract. Neither its build nor any new Lean build was run here. Please do not apply a formal_proof attribute solely from our written manuscript or C++/Arb replay.

This is an intake request with a written proof and reproducible internal computation, not an accepted entry, Lean proof, independent peer review or priority adjudication. Author: Jonas J. Gebendorfer. OpenAI Codex assisted with source comparison and fresh replay.

• Up for grabs: I would like to see the exactly stated variant added by somebody else.

Gebendorfer_WOWII_Zeta_Intake_2026-10-13.zip