The 4 submissions

Description

A variational identity for the Fredholm operator A = I + T on the interval I = [-1/2, 1/2], where T is convolution against the Farmer-Gonek-Lee pair-correlation form factor F1(x) = |x| - 4x^2 + sum_k a_k |x|^(2k+3) with a_k = 2^(2k+3) k! / (2k+2)!. Let w = A^(-1)1 and c* = <1, A^(-1)1>. Over the source-admissible class of scalar profiles v(s) = phi(Ls)^2 induced by even, radially nonincreasing C^2 windows supported exactly on [-L/2, L/2] with 0 <= phi <= 1 and uniform L^1 bounds on phi'' and (phi^2)'', the supremum of <1,v>^2 / <Av,v> equals c*, and the infimum of the reciprocal quotient <Av,v> / <1,v>^2 equals 1/c*.

The upper bound <1,v>^2 <= c* <Av,v> is energy Cauchy-Schwarz. It holds for every v, it is classical, and it is not the content of this result.

The content is the reverse inequality over the constrained class: c* is the value of the unconstrained variational problem, and the identity says that imposing evenness, radial monotonicity, an exact compact support, the amplitude ceiling 0 <= phi <= 1 and uniform L^1 bounds on the second derivatives does not lower the supremum. That direction is proved by exhibiting an explicit endpoint-tapered family inside the class, indexed by the scale L, whose quotient converges to c*. Both orientations are advertised because the orientation is load-bearing: it is the quotient with <1,v>^2 in the numerator whose supremum is c*, and the supporting development also proves that the two are not interchangeable. The advertised statement is existential in the profile and in the two uniform constants, so it carries its own non-vacuity: an IsLUB or IsGLB assertion over the image of an empty class is unsatisfiable in the reals, so the theorem cannot hold unless the class is populated by the constants for which it is stated.

Audience. The kernel F1 is the pair-correlation form factor and the window class is the generalized, load-bearing class of Section 7.1 of the cited paper rather than a convenient flat-topped realization, so the constrained supremum settled here is the quantity that a critical-line proportion argument built on that framework optimizes; analytic number theorists working on the proportion of zeros of the Riemann zeta function on the critical line, and on pair correlation of its zeros, are the audience for which the exact value of that supremum over the admissible class, rather than a bound on it, is the relevant fact. The statement is also a closure result for a constrained admissible class in the variational theory of Fredholm integral operators (MSC 45B05, 49R05) and can be read there without reference to its origin. What the theorem itself asserts is bounded by the scope field below: it is a statement about a Fredholm operator on an interval and a class of test profiles, and it is evidence for nothing beyond that.

Scope

Formalized: the three advertised declarations, unconditionally against pinned Mathlib v4.33.0-rc2. pub1_strong_closure and pub1_strong_closure_reciprocal assume only IsProfile w, which says that w is a bounded continuous solution of Aw = 1, that is, it names the object the statement is about rather than imposing a further condition on it. pub1_strong_closure_exists carries no hypothesis at all, so no advertised statement can be vacuous.

Not formalized, and deliberately outside the advertised statements. The attained maximum over the wider C^2(I) profile class is not itself a formalized statement; only the supremum over the stricter class is, and over that class the value is approached and not attained. The formalized regularity statement is second-order differentiability of w on the open interval (-1/2, 1/2); the upgrade to the closed interval used for attainment in the informal companion note is a short classical mean-value argument and is not formalized. Nothing here formalizes any statement about the Riemann zeta function, its zeros, the proportion of zeros on the critical line, or the Riemann Hypothesis, and the cited paper's realization theorem is neither used nor reproved. No numerical value, enclosure or certificate for c* is part of any advertised statement; the exact-rational certificates in the repository are separate artifacts and are not submitted here. Lean does not verify the interpretation of the Farmer-Gonek-Lee form factor, historical attributions, or novelty relative to the literature.

Sources

• Source-admissible strong closure for the Farmer-Gonek-Lee window functional: the supremum of <1,v>^2/<Av,v> over the compactly supported monotone admissible class is exactly <1, A^(-1)1>. original-proof · relationship: other

  The identity is a result of this laboratory. The cited paper below supplies the setting that is analyzed, namely the form factor, the admissible window class and the induced scalar profile; it does not state or prove this supremum identity. An informal companion note by the same author, "The Optimal Bandwidth-One Window Functional for the xi-prime Pair-Correlation Method" (Zeta Lab, August 2026), presents the same mathematics and names these Lean declarations in its formal-verification section; at the time of this submission that note is in preparation and not yet publicly posted. Originality here is a claim about provenance only. No literature search for prior art on this identity has been run and no claim of novelty is made.

• More than two thirds of the zeta zeros are simple and on the critical line. L. Alpoge, R. Furman. paper · relationship: background · arXiv:2608.13637 · https://www-cdn.anthropic.com/95c246936988e43127bc6b2ceb7077c1dad2d68e.pdf

  Contributor Claude (Anthropic): the official record for arXiv:2608.13637 states that the proof was discovered autonomously by Claude (Anthropic) and verified and communicated by the listed authors

  Supplies the setting, not the result. The cited edition is the revised version dated 11 August 2026, 17 pages, linked from https://www.anthropic.com/research/riemann-zeta and retrieved 2026-08-17, with SHA-256 19f827bee5834d61aa6dd756cdaea582492703ddbfd6bdc2058de10b93f7e814. The admissible class formalized here is not that edition's profile class: it is the stricter compactly supported monotone window class of the earlier edition dated 10 August 2026, 35 pages, retrieved 2026-08-16 from https://www-cdn.anthropic.com/564f962e60643842f5fcb4a17c9dbc8f608f1c37.pdf with SHA-256 6792988e6cd0e17690621ce898abd5d534f98407741bc7cb14bbe7d07c77d72f, in its Section 7.1, p. 20, together with the induced scalar profile of its equation (7.3). The supremum identity proved here is not a theorem of either edition, and nothing in this submission formalizes, restates or depends on that paper's zero-proportion conclusion.

• Pub 1 source-admissible strong closure: exact-rational evidence package (in-repository working document). other · relationship: background · hunts/wide_search/RESULTS-xiprime-admissible-closure.md

  The laboratory's own informal development, pinned in this repository at the submitted commit. It records the exact rational trial polynomial and the strict-concavity bound behind the radial-monotonicity condition of the admissible class.

Related formalisations

• https://github.com/anthropics/zeta-23-lean · independent

  The Lean development accompanying the cited paper, at commit ce196b66685e96f874850a2836e183feccebef2a. It formalizes generic xi-prime window-functional and trace-assembly machinery over its own WindowProfile class and verifies the displayed flat and quartic instances. It does not contain the supremum identity proved here, and this submission neither imports from it nor depends on it.

How the proofs were produced

Models: Claude (Anthropic), Aristotle (Harmonic) · Framework: Zeta Lab, github.com/teal-sea/zeta-lab

The mathematical decomposition and every Lean statement were specified by the laboratory. Proofs of the named subgoals were machine-found through the Harmonic Aristotle service and checked by the Lean kernel; the modules under ZetaLean/Pub1/Aristotle/ are what that service returned. Assembly, auditing, obligation tracking and this Challenge/Solution submission surface were done by Claude agents running in Claude Code against this repository. No step uses native_decide and no step uses floating point.

Wall time: The development ran across agent sessions from 2026-08-12 to 2026-08-16, when the last of its four analytic obligations was discharged and the result became unconditional. The Palomar submission surface was added on 2026-08-21. Spend (USD): not tracked. Hardware: local machine plus hosted API services.

The working pattern was statement-first: the laboratory fixed each Lean statement and its hypotheses, then requested a proof of exactly that statement, then audited what came back. On a neighbouring item the same service refuted a hypothesis gap in the laboratory's own submission by exhibiting a counterexample, which ships in the tree rather than being removed.

Human direction, machine proof search, kernel checking, and an explicit obligation ledger. Every analytic fact the argument consumes was carried as a named field of the StrongClosureData interface until it was discharged, so that a conditional result could not be read as an unconditional one. The status of that interface is tracked in ZetaLean/Pub1/OBLIGATIONS.md. The derivations and computations supporting these results were directed and verified within an AI-assisted computational mathematics framework operated by Thomas Lince at Zeta Lab.

Where the formal argument departs from its source

The formalization is not a literal transcription of the L^2 Fredholm presentation used in the informal companion note, and the differences are deliberate. It works with continuous functions on I under the pairing given by the integral over I rather than on an L^2 quotient space; completeness is never needed, since the Cauchy-Schwarz half is algebra and the limit half needs only boundedness. It obtains w by a Banach fixed point rather than by inverting an operator on that quotient space. It derives the interior second-derivative identity by splitting the integral at t = s rather than through distribution theory. These are mathematically equivalent formulations of the same argument, chosen to avoid formalizing quotient-space machinery the proof does not require.

One further modelling choice is internal to the development: the defining equation for the profile is stated with a clamped kernel, clampedKernel s t = F1(clamp s - clamp t), which on I x I is exactly F1(s-t) and off I repeats the boundary values. F1 is not entire and its row mass is bounded by 4/9 only for s in I, while the Schur and Banach fixed-point lemmas require a hypothesis holding for every real s. The clamped kernel makes those lemmas applicable without changing the quadratic form or the equation on I.

Review

Status: self-assessed

No external mathematical review has been performed.

Internal checks that were performed and are recorded in the repository: the development is sorry-free and uses no theorem-specific axioms, and each advertised declaration was confirmed by #print axioms to depend on exactly propext, Classical.choice and Quot.sound; the four analytic obligations of the StrongClosureData interface are tracked individually in ZetaLean/Pub1/OBLIGATIONS.md and each is discharged; the advertised existential form is quantified over every parameter so that it cannot be vacuous; and a stale status row that understated this item's grade for three days was corrected in the open rather than swept, as recorded in docs/27-state-of-the-transplant.md.

On the submission surface itself: Challenge.lean imports Mathlib alone and restates the needed definitions verbatim in a fresh namespace, Solution.lean reproduces that definition block byte for byte before bridging it to the development, and the three advertised statements are textually identical in the two modules.

The mathematics under lean/ at the submitted commit is unchanged from the tree pinned by the informal companion note, which cites this repository at tag xi-prime-ceiling-support-v1, commit 197cee922270a3ceba7c21de0a21dd816a29adad. Between that commit and the submitted one the only file changed under lean/ is ZetaLean/HardyRamanujantheorem.lean, which is not in the import closure of any advertised declaration.

Acknowledgements

Lean 4 and Mathlib. The Harmonic Aristotle service, which found the proofs of the named subgoals collected under ZetaLean/Pub1/Aristotle/. The authors of the cited paper, whose admissible window class is the object analyzed here.

Description

Let N(T,2T) count the nontrivial zeros of the Riemann zeta function with ordinate in (T,2T], with multiplicity, and N_0^s(T,2T) the simple zeros on the critical line in that range. The Lean development accompanying arXiv:2608.13637 (anthropics/zeta-23-lean) proves, for Mathlib's riemannZeta and unconditionally, that for every eps > 0 and all large T, (H - eps) N(T,2T) <= N_0^s(T,2T) with H = 3/2 - (1/sqrt 2) cot(1/sqrt 2) = 0.6725007036794116... (its Theorem D). Ainta (github.com/ainta/zeta-simple-zeros, paper/riemann.tex, August 2026) refines this to 0.6730085279277797... by a stability term in the rank-trace inequality: the defect D(M) = tr Psi(M) of the Gram matrix of the simple-zero vectors, with Psi(t) = (t-1)^2 on [0,2] and 2t-3 beyond, is carried through the argument, bounded below block by block through a seven-point local inequality F6(g) >= c on six nonnegative gaps, and solved for. The only computer-assisted input is that inequality, which an interval-arithmetic program accepts at c = 19/5000.

This submission advertises that refinement as a theorem of Lean, conditional on exactly that inequality. The principal advertised statement is: for every real c > 0 and naturals m >= 7, p > 0 with c(m-6) <= 1, if c <= F6_p(g) for every nonnegative six-gap vector g (the hypothesis hCert), then for every eps > 0 and all large T, (Phi(c,m,p) - eps) N(T,2T) <= N_0^s(T,2T), where Phi(c,m,p) = (H - 6(m-1)/(pm)) / (1 - c(m-6)/m). Three corollaries instantiate it. The first takes (c,m,p) = (19/5000, 269, 3000), discharges the side conditions by norm_num, and reads (1345000 H - 2680)/1340003 - eps in place of Phi - eps, which is the paper's Theorem 1.1 constant exactly. The other two take this laboratory's own verified parameters (c,m,p) = (34697/10^7, 294, 3400), where the constant is (520625000 H - 915625)/518855453 = 0.6730295534796928...: a finer pressure sweep than the paper's puts the seven-point peak at p = 3400, the same interval-arithmetic verifier accepts c = 34697/10^7 there and refuses 34701/10^7, and the cap c(m-6) <= 1 then gives m = 294. The last of the three states the conclusion as a bound on the ratio N_0^s(T,2T)/N(T,2T), with no positivity guard on the denominator, which is the form the result is usually quoted in. All four are conditional on hCert at their own parameters.

What the work consists of. Every step of the paper between the finite inequality and the zero count is a Lean theorem with standard axioms: the stability rank-trace inequality (as a corollary of the upstream rank-trace theorem at its eigenbasis presentation), the regrouping of the normalised matrix into the simple-zero factor and a complement of bounded positive index, the counting inequality with defect, the tail passage carrying the defect through the upstream endgame at the lambda = 1 window (which turned out to be available there, so no limit over windows was needed), the uniform-in-T limit of the Gram entries to the Montgomery-Taylor overlap kernel k(x) = K(x)/K(0) (proved for every pair of retained zeros at every separation, without the paper's bounded-separation hypothesis), the o(N) count of zeros in the deleted end strips, the block energy, block defect and block bound lemmas, block pinching for convex trace functionals (proved from the fact that the spectrum of a principal submatrix of a Hermitian matrix is a row-stochastic mixture of its spectrum, which is absent from Mathlib at the pinned revision), the averaging over block starts, and the final linear solve. The hypothesis hCert is the paper's Proposition 4.1 and is not formalised; it is named in the statement and nowhere else.

Audience. Analytic number theorists working on simple zeros and zeros on the critical line, for whom the question is which finite inequality a published proportion actually rests on and what it would take to replace it: the theorem exposes that dependence as a single named hypothesis and makes the constant a closed-form function Phi of the certificate parameters. It also isolates, as reusable Lean, block pinching for convex trace functionals on Hermitian matrices and the uniform kernel limit for the Montgomery-Taylor window. What the theorem asserts is bounded by the scope field: it is conditional on hCert, and it is evidence for nothing about the Riemann Hypothesis.

Scope

Formalized: the four advertised declarations, sorry-free, against pinned Mathlib v4.33.0-rc2 and anthropics/zeta-23-lean at the pinned commit, with #print axioms reporting exactly propext, Classical.choice and Quot.sound for each of the four.

CONDITIONAL, AND THE CERTIFICATE IS A HYPOTHESIS, NOT A LEAN FACT. seven_point_bound takes the named hypothesis hCert, which says: for every g : Fin 6 -> R with every g i >= 0, c <= F6 p g, where F6 is Ainta's seven-point functional (the pressure term (1/p) sum g_i plus the 21 pairwise overlap weights w(y_j - y_i) = k(y_j - y_i)^2 with coefficient 2/(7-r) for a pair spanning r gaps). This is the paper's Proposition 4.1. What is known about it is that an interval-arithmetic program written in Arb accepts it: at (c, p) = (19/5000, 3000) in the published run at github.com/ainta/zeta-simple-zeros, which this laboratory reproduced field for field, and at (34697/10^7, 3400) in this laboratory's own run, both recorded under hunts/ainta_seven_point in the submitted repository. A verifier's acceptance is not a kernel-checked proof and no claim is made here that it is; re-enclosing the underlying sinc table inside Lean is a separate project of a different size. The hypothesis is written into every advertised statement, with its numbers, rather than assumed as an axiom, exactly so that this distinction survives every way of quoting the result. Each statement also takes hA0 : c(m-6) <= 1, a rational side condition, and the side conditions 7 <= m, 0 < p, 0 < c; in the three instantiated statements all four are discharged by norm_num, leaving hCert as the only hypothesis. Every other input, including the Riemann-von Mangoldt formula and the explicit formula, is discharged inside the dependency for riemannZeta.

Non-vacuity of the hypothesis: F6 p 0 = 12 and F6 p g >= (1/p) sum g_i, so the class of (c, p) satisfying hCert is nonempty; what the certificate supplies is the specific value, and the theorem's interest is proportional to that value. The difference between the paper's constant and this laboratory's is a difference of assumed certificate, not of proved mathematics: the same parametric theorem is instantiated twice.

Not formalized, and deliberately outside the advertised statements: the seven-point inequality itself, at either parameter set (a 45 600-cell interval table and a branch-and-bound search of 707 901 nodes at p = 3000 and 1 112 733 at p = 3400); the eight-point generalisation, whose bridge from certificate to proportion this laboratory has stated but not proved and which is therefore not offered here at all; the Gohms variant at 191/50000 and the other certificate targets the hunt explored; any numerical value of H beyond its closed form.

NOTHING HERE BEARS ON THE RIEMANN HYPOTHESIS: the conclusion is a lower bound on a proportion of zeros and holds whether or not RH does. The base constant H is the dependency's theorem, not this submission's.

Sources

• More than 67.3% of the zeros of the Riemann zeta function are simple and lie on the critical line. Ainta. paper · relationship: adapts · https://github.com/ainta/zeta-simple-zeros

  Formalised here with departures listed under fidelity.divergences. The Lean statement, the sixteen-step decomposition (hunts/ainta_seven_point/TRUST-MAP.md), the closed form Phi(c, m, p) with its block-size cap, the sharp stability form and the pinching proof are this laboratory's; steps S0 to S5 are theorems of anthropics/zeta-23-lean consumed by import. The informal source of every step between the finite inequality and the zero count (S2 to S16 of the trust map): paper/riemann.tex at commit 040c5e899e658aed7b56a2a87f501798fe10761d, 499 lines, retrieved 2026-08-22. Its Proposition 4.1, the seven-point inequality, is the hypothesis hCert of the advertised theorem and is not formalised; its verifier's run was reproduced by this laboratory field for field (hunts/ainta_seven_point/RESULTS.md). The author is known to us only by the GitHub handle. Not listed as "formalizes" because the assembled theorem is parametric in (c, m, p) and conditional, and because the formal proofs of S8, S9, S14 and S15 follow routes the paper does not take; the relationship is stated here in words instead.

• More than two thirds of the zeta zeros are simple and on the critical line. L. Alpoge, R. Furman. paper · relationship: background · arXiv:2608.13637 · https://www-cdn.anthropic.com/95c246936988e43127bc6b2ceb7077c1dad2d68e.pdf

  Contributor Claude (Anthropic): the official record for arXiv:2608.13637 states that the proof was discovered autonomously by Claude (Anthropic) and verified and communicated by the listed authors

  The base theorem that Ainta refines, and the source of the analytic estimates (Propositions 4.2 and 4.4, sections 5 to 7) the tail passage and the kernel limit reach into. Consumed here entirely through its Lean development, cited under related_formalizations; nothing is transcribed from the paper's text.

Related formalisations

• https://github.com/anthropics/zeta-23-lean · builds-on

  The Lean development accompanying arXiv:2608.13637, pinned at commit 3635e74826a4c1fcece7d1cd2b6fa75e43a00510 as a Lake dependency of the selected project. It supplies the counting functions Ncount and N0simple for Mathlib's riemannZeta, the analytic inputs PaperInputs discharged for riemannZeta, the constant HD 1 = H, the Montgomery-Taylor window and its endgame, the von Neumann trace inequality, the positive-part splitting and the spectral calculus specMap. The advertised theorem is its thmD_0_simple_mult with HD 1 replaced by Phi c m p; dropping the defect recovers that theorem. Nothing in the dependency was modified.

How the proofs were produced

Models: Claude (Anthropic) · Framework: Zeta Lab, github.com/teal-sea/zeta-lab

The sixteen-step decomposition, every Lean statement and every proof were produced by Claude agents running in Claude Code against this repository: one agent wrote the end-to-end skeleton with the eleven unproved steps as named lemmas carrying sorry and their residual goals in words, four agents then closed them in parallel on disjoint files, and one agent integrated, built and audited. The Harmonic Aristotle service was available under a cap of three submissions per agent and was not used: zero of fifteen, because every obligation closed locally before a residual existed (lean/ARISTOTLE-RUNS.md, Batch 12). A further agent pass then packaged the result for this registry: it moved the development into the Lake package lean/bridge so that it assembles at a root, wrote the Challenge and Solution modules, added the two instantiations at this laboratory's own certificate parameters, and corrected the licence headers. No step uses native_decide and no step uses floating point.

Wall time: The skeleton, the five attack branches and the integration ran on 2026-08-23, one working day, following a trust-map pass on 2026-08-22 and the S2 probe earlier on 2026-08-23. Spend (USD): not tracked. Hardware: local machine; no proving service.

Statement-first, as for the laboratory's earlier submissions: the skeleton fixed each step's Lean statement in the dependency's own vocabulary, each attacker was told to leave anything unproved as a named lemma with its residual goal in words, and the integrator was told to turn leftovers into explicit hypotheses of the main theorem. None were left.

Human direction, agent proof writing, kernel checking, and an explicit obligation ledger per attack group under hunts/ainta_seven_point/bridge/. The single non-Lean input is carried as a named hypothesis of every advertised theorem so that the conditional result cannot be read as an unconditional one. The interval-arithmetic runs behind that hypothesis were executed by this laboratory and are recorded, with node and depth counts and their artifacts, in hunts/ainta_seven_point/RUNS.md and RESULTS.md; they are evidence for the hypothesis, not a proof of it. The derivations were directed and verified within an AI-assisted computational mathematics framework operated by Thomas Lince at Zeta Lab.

Where the formal argument departs from its source

The formal argument follows the paper's structure and departs from its text in the following places, each recorded in hunts/ainta_seven_point/BRIDGE.md section 6. The kernel limit (Lemma 3.1) is proved for every pair of retained zeros at every separation; the paper's bounded-separation parameter R_0 is kept in the signature but is not used. The tail passage (Corollary 2.2) does not pass through the dependency's limit over windows lambda -> 1; it re-states two of the dependency's endgame lemmas at lambda = 1 with the defect carried as a hypothesis, which their own inputs permit. Block pinching (eq:pinching) is proved without convexity of the matrix functional or unitary invariance, from the row-stochastic mixture of the spectrum of a principal submatrix and scalar Jensen; the partition form needs no positivity of Psi, the two-block form does. The block defect lemma (Lemma 4.3) is proved for every Hermitian matrix, positivity unused. The block energy lemma (Lemma 4.2) is proved as a fibre count plus an exact telescoping identity, both needing w even. The block bound (eq:269block) uses |k| <= 1, which the paper does not state and which holds because cos(sqrt 2 t) >= 0 on [-1/2, 1/2]; its error term is 2 m^2 delta rather than an unquantified o(1). The averaging of section 5 is over all n-m+1 block starts with one pinching partition per residue class rather than over m offsets with a floor count. The span bound x_{S} - x_1 <= N + o(N) uses L <= l_1 (that is 2 log 2 - 1 >= 0 at lambda = 1) and log T = o(T), neither stated in the paper. Every o(N) in the paper is an explicit eta N in the Lean, consumed as an eventually-in-T statement.

Review

Status: self-assessed

No external mathematical review has been performed, and no person outside this laboratory has read the development. "self-assessed" means exactly that: the checks below were run by the laboratory on its own work.

Packaging state. The three blockers recorded here in an earlier revision are resolved. (1) The advertised development now lives in its own Lake package, lean/bridge, which requires anthropics/zeta-23-lean at the pinned commit and whose root module imports every module in it; `lake build` at that root completes with 8860 jobs and zero errors, so a replay of the selected project builds the theorem rather than stopping on three modules of hunts/frontier_math/zeta23ext that the theorem never imports (repository issue 101, which remains open for that other package and is now unrelated to this submission). (2) The Challenge and Solution modules named by lean/bridge/comparator.json exist: BridgeChallenge.lean states the four advertised theorems over Mathlib alone, in the namespace Zeta23Ext.Palomar, restating verbatim the five counting definitions of the dependency's Zeta23/Statement.lean and the five kernel and functional definitions of Zeta23Ext/Bridge/Defs.lean, and writing the constant H in the closed form the dependency's HD_one proves equal to its HD 1; BridgeSolution.lean proves the same four from Zeta23Ext.Bridge.Main through those bridges, every one of which is rfl except H_eq, which is HD_one. (3) The Apache-2.0 headers the Bridge files had copied from the dependency's house style are replaced by MIT headers matching the repository licence; the one file that adapts the dependency's code rather than importing it, Zeta23Ext/Bridge/Helpers_S8.lean, keeps its attribution to Anthropic, PBC and the Apache-2.0 licence of the transcribed proof bodies in a notice, in its own header and in lean/bridge/NOTICE.

Deliberate sorry count. The Challenge module carries four sorry, one per advertised statement, which is what the Palomar format requires of a statement-only module. The development and the Solution module carry none: a whole-package build reports exactly four `declaration uses sorry` warnings and all four are in BridgeChallenge.lean. Any claim that this tree is sorry-free has to say which object it means, and this field is that statement.

Internal checks performed and recorded: the four advertised declarations and the 72 other audited declarations in the package report exactly propext, Classical.choice and Quot.sound under #print axioms, 76 audit lines in one whole-package build (fourteen of them print Classical.choice as choice, because Classical is open in the module that emits them); a static scan of every Lean file in the package finds no axiom, opaque, unsafe, admit, native_decide, implemented_by or extern; no step lemma's statement was changed by any attack branch relative to the skeleton; the per-group ledgers under hunts/ainta_seven_point/bridge/ record zero proving-service submissions, zero of fifteen permitted; and the hypothesis hCert is named in every advertised statement and in status.scope, so no reading of this entry can take the result as unconditional.

Known limitations of this self-assessment: the interval-arithmetic runs behind hCert were checked by reproducing a third party's run and by re-running a corrected variant, not by any formal method; the constants inside the proofs are not sharp and were not tuned; and whether a conditional refinement of a theorem already registered from the upstream repository clears this registry's notability floor is the registry's call, not a claim this file makes for it.

Acknowledgements

Lean 4 and Mathlib. The authors of anthropics/zeta-23-lean, whose development this theorem extends and whose endgame, window calculus and linear algebra it consumes. Ainta, whose argument this is.

Description

Let N(T,2T) count the nontrivial zeros of the Riemann zeta function with ordinate in (T,2T], with multiplicity, and N_0^s(T,2T) the simple zeros among them on the critical line. The Lean development accompanying arXiv:2608.13637 (anthropics/zeta-23-lean) proves, for Mathlib's riemannZeta and unconditionally, that for every eps > 0 and all large T, (H - eps) N(T,2T) <= N_0^s(T,2T), with H = 3/2 - (1/sqrt 2) cot(1/sqrt 2) = 0.67250070367941164573... (its Theorem D). Ainta (github.com/ainta/zeta-simple-zeros) refines H by carrying the spectral defect of the Gram matrix of the simple-zero vectors through that argument and bounding it block by block through a local inequality on seven points.

Advertised here: that refinement carried out for n points at once, and three instances. Parametrically, for n >= 2, c > 0, m >= n, p > 0 with c(m-(n-1)) <= 1, if c <= F(n,p,g) for every nonnegative vector g of n-1 gaps (the hypothesis hCert), then for every eps > 0 and all large T, (Phi_n(n,c,m,p) - eps) N(T,2T) <= N_0^s(T,2T), where Phi_n(n,c,m,p) = (H - (n-1)(m-1)/(pm)) / (1 - c(m-(n-1))/m). At n = 7 this is Ainta's theorem.

THE THREE-POINT INSTANCE IS UNCONDITIONAL. At (n,c,p) = (3, 1345/10^6, 3000) the hypothesis is proved, not assumed: the overlap weight w = k^2 is enclosed from a twelve-term Taylor bound on cos and sin and the closed form of the kernel, and 368 interval cell lemmas over rationals, applied 1515 times over 487 leaves, cover the quarter-plane of the two gaps. No external interval-arithmetic certificate is assumed for the three-point theorem, and no floating point appears. The cap gives m = 745 and the constant (149000000 H - 99200)/148800133 = 0.67273733450380945032..., exceeding H by 2.3663e-4: for Mathlib's riemannZeta, an unconditional improvement of the dependency's Theorem D.

THE FOUR-POINT INSTANCE IS ALSO UNCONDITIONAL. At (n,c,p) = (4, 2310/10^6, 2500), the finite inequality at every triple of nonnegative gaps is proved inside Lean. The cap gives m = 435 and the resulting constant is (906250 H - 1085)/904171 = 0.67284701976668882760.... The bound and ratio carry no certificate hypothesis and use exactly the same three permitted axioms. The eight-point instance stays conditional. Our n-point generalisation of Ainta's interval verifier accepts c = 41763/10^7 at p = 3200, giving m = 246 and 0.67305298298962888...; interval-arithmetic acceptance is not a Lean proof, so hCert remains explicit. The contrast is explicit in the statements: the parametric and eight-point theorems retain a named certificate hypothesis, while the three- and four-point theorems prove their certificates inside Lean.

RELATION TO THE PUBLIC FIELD, AND WHY THE ADVERTISED UNCONDITIONAL CONSTANTS ARE SMALLER THAN PUBLISHED ONES. Three constants for this quantity are public, and two of them exceed both unconditional instances advertised here. The dependency's Theorem D gives H = 0.67250070367941164573...; Ainta's Theorem 1.1, at c = 19/5000 with m = 269 and p = 3000, gives 0.6730085279277797613...; and Gohms, in issue #1 on Ainta's repository, at c = 191/50000 with m = 267 and p = 3000, gives 0.6730213619501665.... Both figures above H rest on an interval-arithmetic program accepting a finite inequality, not on a proof of it; the Gohms issue says as much of itself, calling the result provisional, not peer-reviewed and not formally verified. This laboratory reproduced both runs at the pinned commit 040c5e8, found that the verifier's compactification prune is applied without consulting the target and is therefore justified at Ainta's target only, re-ran both targets with the cutoff derived from the target instead, and reported all of it on that issue on 2026-08-23; every published claim survived the correction. That same public comment records the seven-point family's own ceiling, 0.673029553 at p = 3400 with m = 294, and the eight-point figure 0.673052983 that appears here as eight_point_bound. So the strongest constant reported in this family, as far as this laboratory knows, is the one advertised here, and it is precisely the one this submission leaves CONDITIONAL, with its certificate hypothesis and that hypothesis's numbers written into the statement. What is offered here is therefore not a larger constant. It is a different kind of evidence for one: the analytic passage from a finite inequality to a proportion of zeros, which every figure above quotes informally, is machine-checked against Mathlib's riemannZeta, and at n = 3 and n = 4 the finite inequality itself is proved inside Lean, so those two instances carry no certificate and no hypothesis at all. They are numerically smaller than Ainta's and Gohms's figures and they are the only ones in the list that are theorems about riemannZeta. No novelty is claimed for the n-point generalisation beyond this: no prior formalisation of it is known to this laboratory, and no systematic search has been performed that would establish that none exists.

Scope

Formalized: V2Solution proves the seven advertised declarations without sorry against pinned Mathlib v4.33.0-rc2 and anthropics/zeta-23-lean at the pinned commit. V2Challenge contains seven deliberate statement placeholders. Each proved declaration reports exactly propext, Classical.choice and Quot.sound.

WHICH ARE CONDITIONAL. Three of the seven carry the named hypothesis hCert: for every g : Fin (n-1) -> R with every g i >= 0, c <= F n p g, F being the n-point functional (the pressure term (1/p) sum g_i plus the n(n-1)/2 pairwise overlap weights with coefficient 2/(n-(j-i))). n_point_bound takes it parametrically; the two eight-point statements take it at (8, 41763/10^7, 3200), where what is known is that an interval-arithmetic program written in Arb accepts it over 64 of 64 shards and 6 504 134 nodes, the run recorded under hunts/ainta_seven_point in the submitted repository. That is not a kernel-checked proof and no claim is made here that it is; the hypothesis is written into the statement, with its numbers, so the distinction survives every way of quoting the result.

WHICH ARE NOT. three_point_bound, three_point_bound_ratio, four_point_bound and four_point_bound_ratio carry NO hypothesis. At (3, 1345/10^6, 3000) the finite inequality is a theorem of Lean in this package, 368 interval cell lemmas over rationals applied 1515 times over 487 leaves, resting on a twelve-term Taylor enclosure from Complex.exp_bound and the closed form of the kernel. No external interval-arithmetic certificate is assumed for the three-point theorem, no floating point is used. At (4, 2310/10^6, 2500), the finite inequality over every triple of nonnegative gaps is likewise a theorem of Lean in this package and yields (906250 H - 1085)/904171 = 0.67284701976668882760.... native_decide appears nowhere in the package. The side conditions 2 <= n, n <= m, 0 < p, 0 < c and c(m-(n-1)) <= 1 are rational and closed by norm_num. Every analytic input, Riemann-von Mangoldt and the explicit formula included, is discharged inside the dependency for riemannZeta.

Not formalized: the n-point inequality at n = 7 or n = 8; any numerical value of H beyond its closed form.

NOTHING HERE BEARS ON THE RIEMANN HYPOTHESIS: the conclusion is a lower bound on a proportion of zeros and holds whether or not RH does. The base constant H is the dependency's theorem, not this entry's.

Sources

• More than 67.3% of the zeros of the Riemann zeta function are simple and lie on the critical line. Ainta. paper · relationship: adapts · https://github.com/ainta/zeta-simple-zeros

  paper/riemann.tex at commit 040c5e899e658aed7b56a2a87f501798fe10761d, retrieved 2026-08-22: the informal source of the argument from the finite inequality to the zero count. The generalisation to n points, the closed form Phi_n with its cap, the pinching proof, every Lean statement and proof, the eight-point certificate and the three- and four-point enclosures are this laboratory's. Not "formalizes": the theorem is parametric, the three- and four-point instances are unconditional where the paper's result is not, and several steps take routes the paper does not. Its reported constant is 0.6730085279277797613..., at c = 19/5000 with m = 269 and p = 3000, which exceeds both unconditional instances advertised here; its finite inequality is established by an interval-arithmetic search rather than by a proof, and its passage from that inequality to a proportion of zeros is informal. Reproduced here at the pinned commit 040c5e8, every search statistic matching the committed certificate: nodes 707901, depth 37, kernel hash. The reproduction, the defect found in the shared verifier and the family's measured ceiling were posted to that repository on 2026-08-23 under the submitter's GitHub account; the audit itself is in hunts/ainta_seven_point/TRUST-MAP.md in the submitted repository.

• More than two thirds of the zeta zeros are simple and on the critical line. L. Alpoge, R. Furman. paper · relationship: background · arXiv:2608.13637 · https://www-cdn.anthropic.com/95c246936988e43127bc6b2ceb7077c1dad2d68e.pdf

  Contributor Claude (Anthropic): the official record for arXiv:2608.13637 states that the proof was discovered autonomously by Claude (Anthropic) and verified and communicated by the listed authors

  The base theorem this work refines, consumed entirely through its Lean development. Nothing is transcribed from its text. Its constant H = 0.67250070367941164573... is the figure both unconditional instances advertised here exceed.

• Provisional stronger 7-point certificate: F6 >= 191/50000 gives 67.302136%. Gohms. web discussion · relationship: background · https://github.com/ainta/zeta-simple-zeros/issues/1

  Contributor ChatGPT (OpenAI): the issue states that the campaign behind the constant was conducted by prompting ChatGPT, and describes its own result as provisional, not peer-reviewed and not formally verified

  Posted 2026-08-19T03:25:43Z. Nothing in this submission depends on it; it is cited because it is the strongest constant reported by an outside group for this quantity and it exceeds both unconditional instances advertised here. Its figure is 0.6730213619501665..., at c = 191/50000 with m = 267 and p = 3000, obtained by running Ainta's published verifier with TARGET_NUMERATOR and TARGET_DENOMINATOR changed and nothing else. Reproduced here at the pinned commit 040c5e8: nodes 786421, pruned 393575, depth 43, matching the three figures the issue reports. One defect was found against it and reported on that issue on 2026-08-23 under the submitter's GitHub account, with the audit in hunts/ainta_seven_point/TRUST-MAP.md section 5.1 of the submitted repository: verify_seven.py prunes any box whose gap sum reaches PRESSURE_CUTOFF_CELLS / GRID = 11.4 on the grounds that the linear term alone then gives 11.4/3000 = 19/5000, and applies that rule unconditionally without consulting the target, so it is justified at Ainta's target, at equality, and unsupported at this larger one, where the recorded run pruned 3087 boxes on those grounds. This does not show the claim false, and the claim is not disputed here: re-running with the cutoff derived from the target instead accepts 191/50000 at grid 4000 in 786085 nodes at depth 43, so the published figure survives the correction. What it means is narrower and is the reason the distinction matters for this submission: the evidence for that constant, before and after the correction, is an interval-arithmetic program's acceptance of a finite inequality, and the passage from that inequality to a proportion of zeros is quoted informally. Neither step is a proof about riemannZeta. The three- and four-point instances advertised here report smaller constants and prove both steps.

Related formalisations

• https://github.com/anthropics/zeta-23-lean · builds-on

  Pinned at commit 3635e74826a4c1fcece7d1cd2b6fa75e43a00510 as a Lake dependency of the selected project. It supplies Ncount and N0simple for Mathlib's riemannZeta, the analytic inputs discharged for riemannZeta, the constant HD 1 = H, the Montgomery-Taylor window and its endgame, and the linear algebra. The advertised theorem is its thmD_0_simple_mult with HD 1 replaced by Phi_n n c m p. Nothing in it was modified, and three_point_bound and four_point_bound improve its Theorem D under the same axioms and with no certificate hypothesis.

How the proofs were produced

Models: Claude (Anthropic) · Framework: Zeta Lab, github.com/teal-sea/zeta-lab

Every Lean statement and proof was produced by Claude agents in Claude Code against this repository, under human direction and an explicit per-step obligation ledger, statement-first: each step's statement was fixed in the dependency's vocabulary before any proof was attempted, and leftovers became explicit hypotheses of the main theorem. The three- and four-point covers are emitted by generators in this repository and checked by Lean, not by the generators. The Harmonic Aristotle proving service was available under a cap and was not used.

Wall time: 2026-08-23. Spend (USD): not tracked. Hardware: local machine and hosted CI; no proving service.

Human direction, agent proof writing, kernel checking, within an AI-assisted computational mathematics framework operated by Thomas Lince at Zeta Lab.

Where the formal argument departs from its source

The formal argument follows the paper's structure; each place it departs from the text is recorded in hunts/ainta_seven_point/BRIDGE.md section 6. The kernel limit is proved at every separation; the tail passage carries the defect as a hypothesis at lambda = 1 rather than taking a limit over windows; block pinching is proved without convexity or unitary invariance; every o(N) in the paper is an explicit eta N in the Lean. The n-point layer and the proofs of the finite inequalities at n = 3 and n = 4 have no counterpart in the paper.

Review

Status: self-assessed

No external mathematical review has been performed and no person outside this laboratory has read the development.

Deliberate sorry count: V2Challenge.lean carries seven sorry, one per advertised statement, which is what the Palomar format requires of a statement-only module. The development and V2Solution.lean carry none. A claim that this tree is sorry-free has to say which object it means, and this field is that statement.

Checks: the seven advertised declarations report exactly the three standard axioms in a whole-package build; a static scan of every Lean file in the selected project finds no axiom, opaque, unsafe, admit, native_decide, implemented_by or extern; the Challenge's copies of the definitions are tied to the development's by rfl bridges in the Solution, the one exception being H, whose bridge is the dependency's theorem HD_one.

Limitations: the run behind the eight-point hCert was checked by reproducing a third party's run and re-running a generalisation of it, not by any formal method; and whether this entry clears the notability floor is the registry's call, not a claim this file makes. Replay cost note: the selected project compiles the generated ThreePoint and FourPoint tables; the merged four-point source adds approximately 78,000 generated lines, so this replay is materially heavier than the earlier V2 surface.

Acknowledgements

Lean 4 and Mathlib. The authors of anthropics/zeta-23-lean, whose development this theorem extends. Ainta, whose argument this is.

Description

Davenport and Heilbronn (1936) exhibited a Dirichlet series with real coefficients satisfying a Riemann-type functional equation which nevertheless has zeros off the critical line. It is the standard demonstration that a functional equation of Riemann type does not on its own force the Riemann Hypothesis, it is the reference counterexample against which structural explanations of the Riemann Hypothesis are tested, and the location of its zeros remains an active subject. The function is DH(s) = (1 - i*kappa)/2 * L(s, chi) + (1 + i*kappa)/2 * L(s, chi^-1) for a quartic Dirichlet character chi mod 5 and kappa = (sqrt(10 - 2*sqrt 5) - 2)/(sqrt 5 - 1), the value that rotates the two conjugate root numbers onto each other and so makes the Dirichlet coefficients real.

This submission advertises one theorem, the analytic half of the Davenport-Heilbronn theorem: there exists an entire function represented by the Davenport-Heilbronn Dirichlet series on Re z > 1 whose completion (pi/5)^(-(s+1)/2) * Gamma((s+1)/2) * f(s) is symmetric under s -> 1-s. The statement is existential in f, so it carries its own non-vacuity and needs none of the character theory used to construct the witness.

What the work consists of. The Davenport-Heilbronn function is not a library object anywhere we could find, so the development builds it: the quartic character mod 5, the linear combination, entirety on all of C, the identification of the Dirichlet coefficients as the real period-5 sequence 1, kappa, -kappa, -1, 0, and the completed functional equation. The last of these is where the content sits. It reduces to a root-number identity whose convention-sensitive constants are derived inside the development, from Mathlib's Real.cos_pi_div_five by radical algebra, rather than transcribed from a table; the standard sources state kappa without deriving it in a form a kernel will accept, and getting it wrong yields a function whose coefficients are not real and which therefore is not the counterexample. The functional equation is stated with explicit guards excluding the poles of the two Gamma factors, because Mathlib's junk value Gamma = 0 at the poles would otherwise make the unrestricted equation false for reasons having nothing to do with the mathematics.

Audience. The Davenport-Heilbronn function is a named object of analytic number theory with a continuing literature on its zeros, so a machine-checked construction of it is of direct interest to number theorists working on zeros of L-functions and on what a Riemann-type functional equation does and does not imply. It is also the object a formalized treatment of the Davenport-Heilbronn theorem has to have before it can say anything, and this supplies it in a form that carries its own non-vacuity.

Prior art. A search of Mathlib at the revision pinned by this repository found no Davenport-Heilbronn function and no formalization of this functional equation. That is a bounded search of one library. No systematic search of other proof assistants or of the mathematical literature for prior formalizations has been run, and no novelty against the literature is claimed: the mathematics is Davenport and Heilbronn's, published in 1936.

Scope. The Davenport-Heilbronn theorem itself is NOT proved here. Its full statement additionally requires a zero s with Re s different from 1/2, and that conjunct appears nowhere in the advertised theorem. What is offered is the analytic half alone. No numerical enclosure for any zero of DH is asserted, and nothing here is a statement about the Riemann zeta function or the Riemann Hypothesis.

Scope

Formalized: the single statement advertised in DHChallenge.lean, unconditionally. That is the existence of an entire function satisfying the Davenport-Heilbronn series representation on Re z > 1 together with the completed functional equation.

Not formalized, and deliberately outside the advertised statement: the existence of a zero of the Davenport-Heilbronn function off the critical line, and therefore the Davenport-Heilbronn theorem itself; any numerical enclosure, interval evaluation or certificate for any zero; and any statement about the Riemann zeta function or the Riemann Hypothesis.

Sources

• On the zeros of certain Dirichlet series. H. Davenport, H. Heilbronn. paper · relationship: formalizes · J. London Math. Soc. 11 (1936), 181-185 and 307-312

  The source constructs the function and establishes both its analytic properties and the existence of zeros off the critical line. This formalization covers the analytic half only: the existence of an entire function with the stated Dirichlet series representation and functional equation. The off-line zero, which is the substance of the source's theorem, is not formalized here. The definition formalized matches the standard one in the subsequent literature, including the value of kappa.

How the proofs were produced

Models: Claude (Anthropic) · Framework: Zeta Lab, github.com/teal-sea/zeta-lab

Every Lean statement was specified by the laboratory and the proofs were written and audited by Claude agents running in Claude Code against this repository. Unlike some other modules of this laboratory, no external theorem-proving service was used for the Davenport-Heilbronn development. No step used native_decide and no step used floating point.

Spend (USD): not tracked. Hardware: local machine plus hosted API services.

The functional-equation half reduces to a root-number identity, and the convention-sensitive steps are derived in the development rather than remembered, from Mathlib's Real.cos_pi_div_five by radical algebra. The development records explicitly which half of the Davenport-Heilbronn theorem is kernel-checked and which remains a numerical obligation.

Where the formal argument departs from its source

One deliberate modelling choice, documented at the point of use. The functional equation is stated with explicit guards Complex.Gamma ((z+1)/2) != 0 and Complex.Gamma ((1-z+1)/2) != 0. These exclude exactly the points at which Mathlib's junk value Gamma = 0 would make the unrestricted equation false; away from them both sides are the honest completed function. Without the guards the statement would be false for reasons having nothing to do with the mathematics.

Review

Status: self-assessed

No external mathematical review has been performed.

Internal checks recorded in the repository. The substantive development under lean/ZetaLean and the DHSolution module are sorry-free and axiom-clean against pinned Mathlib v4.33.0-rc2. This claim deliberately excludes the Challenge modules: Challenge.lean and DHChallenge.lean together carry four placeholder sorrys, one per advertised statement across this repository's two submission surfaces, because the Palomar format requires a Challenge to state its claim without proving it. Those placeholders are not steps in any proof, and Comparator checks that the corresponding Solution declarations are hole-free. Further internal checks: the definitions in DHChallenge.lean are verbatim copies of the development's own definitions and the DHSolution module reproduces that definition block before bridging it; and the advertised statement was chosen so that it does not contain the off-line-zero conjunct, so that the analytic half cannot be read as the full theorem.

Acknowledgements

Lean 4 and Mathlib, whose Dirichlet L-function library the development rests on. Davenport and Heilbronn, whose construction is the object formalized.