Externally verified

01. What the registry did

The Palomar Registry is a registry of Lean-verified mathematics, incubated by the Lean FRO and ICARM, which opened for submissions on 18 August 2026. It stands to a Lean proof roughly as a preprint server stands to a paper: it records a claim from a fixed commit of a public repository, replays the proof, applies an editorial floor for research interest, and publishes the statement together with what the review found.

It did not read our account of the proof. It fetched the commit, rebuilt the development from scratch on its own hardware inside a sandbox, and replayed every step through Lean's kernel and through NanoDa, a kernel written independently of it. Two checkers, and neither of them ours.

02. Zeta Lab: source-admissible strong closure for the F1 window functional

Write A = I + T for the Fredholm operator whose kernel is the Farmer-Gonek-Lee form factor F1 on I = [-1/2, 1/2], and set w = A⁻¹1 and c* = ⟨1, w⟩. Over the compactly supported monotone admissible class of profiles v(s) = φ(Ls)²:

The upper bound is not the content. That ⟨1,v⟩² ≤ c*⟨Av,v⟩ is energy Cauchy-Schwarz. It holds for every v, it is classical, and it is not the thing worth checking. The content is the reverse inequality: imposing evenness, radial monotonicity, an exact compact support, the amplitude ceiling and uniform bounds on the second derivatives does not lower the supremum. It is proved by exhibiting an explicit endpoint-tapered family inside the class whose quotient converges to c*.

The part worth restating, because it is the way this gets misread: it is a statement about a Fredholm operator on an interval and about a class of test profiles. It says nothing about the zeros of the zeta function, nothing about the Riemann hypothesis, and it asserts no numerical value for c*.

Scope, in the words the registry was given

The submission's own scope field, quoted rather than summarised.

Statements, axioms, namespace and the quotation above are read from lean/formalization.yaml and lean/comparator.json at build time, so none of it is a retyping.

03. Zeta Lab: the analytic half of Davenport-Heilbronn

Davenport and Heilbronn (1936) exhibited a Dirichlet series with real coefficients satisfying a functional equation of Riemann type which nevertheless has zeros off the critical line. Write DH(s) = (1 - iκ)/2 · L(s, χ) + (1 + iκ)/2 · L(s, χ⁻¹) for a quartic Dirichlet character χ mod 5 and κ = (√(10 - 2√5) - 2)/(√5 - 1), the value that rotates the two conjugate root numbers onto each other and so makes the coefficients real. The advertised theorem is the analytic half:

This is not the half the theorem is famous for. Davenport and Heilbronn are cited for the zeros off the critical line, and that is not what was checked here. What was checked is that the function exists, is entire, and satisfies the symmetry. The counterexample's punchline is absent, and nothing here establishes it.

The work is in the construction. 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 ℂ, the coefficients as the real period-5 sequence 1, κ, -κ, -1, 0, and the completed functional equation. The last is where the content sits, and 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. Getting κ wrong yields a function whose coefficients are not real, which is then not the counterexample at all. The functional equation carries explicit guards excluding the poles of the two Gamma factors, because Mathlib's junk value Γ = 0 at the poles would otherwise make the unrestricted statement false for reasons that have nothing to do with the mathematics.

The statement is existential in f, so it carries its own non-vacuity. And it is source-based in the registry's own classification: it formalizes a result of Davenport and Heilbronn from 1936. It is not a new theorem, and this record does not present it as one.

Scope, in the words the registry was given

The submission's own scope field, quoted rather than summarised.

Statements, axioms, namespace and the quotation above are read from lean/palomar-dh/formalization.yaml and lean/comparator-dh.json at build time, so none of it is a retyping.

04. What this is not

It is not peer review. No person read it. A machine rebuilt the development, two kernels accepted every step, and an editorial pass by a reviewer model reported no problems across the headings listed above. That is a real check and it is not ours, which is the whole reason for this page. It is not a mathematician saying the argument is right, or that the result is worth having.

It does not add a rung. The certainty ladder this laboratory grades against ends at kernel-checked, and it still ends there. Review by an outside reader is not a grade we can award ourselves, and this does not award it. Each submission's own review field still reads self-assessed.

It covers what it covers. The candidate past the two-thirds constant on the front page is a different chain, it still carries an open step, and it has not been through this. Nothing here transfers to it.

05. Every surface, and what state it is in

Both submissions above are registered and both now have public registry entries, linked in their receipts. Each identifier was read back out of the registry's own published record before being put on this page, rather than guessed from the pattern of the others.

Both are reachable by direct link and both are listed in the registry's own index and search.

Every submission surface the tree carries is below. A surface here is prepared, which is not the same as checked, and the table says which is which.