One registry of formal statements about the Riemann zeta function and its zeros, kept in TOML files and checked by a Lean 4 kernel, with the reverse-Dyson quasicrystal program in front. Every status on this page is read from the registry; nothing is inferred, and nothing here is a proof of the Riemann Hypothesis.
The plots are computed live in your browser from bundled data. Where a number is a float-model estimate, an Arb enclosure, or a truncated sum, the plot says so. Where a theorem is conditional, its hypotheses are shown. Every recorded audit is labelled with the independence the registry records: self-attested, independent read-back (a different session and identity from the node's author), or judge-verified once a Comparator judge run is recorded for the node.
Take a discrete set of points on the real line and put a unit mass at each one. Call the result a comb. A comb is a Fourier quasicrystal when its Fourier transform is again a comb: a countable sum of point masses, the Bragg peaks of a diffraction picture, with no continuous part. A periodic lattice is the trivial example (Poisson summation). The interesting examples are not periodic. Kurasov and Sarnak (2020) showed that every Fourier quasicrystal with integer masses on the line is the real zero set of a Lee-Yang exponential polynomial, and Alon, Cohen and Vinzant (2024) showed the converse. The quasicrystal island carries the finite shadow of that dictionary in the kernel: a two-frequency exponential sum is real-rooted exactly when its two coefficients have equal modulus (node MM_twofreq_realrooted_iff), and a one-frequency Lee-Yang polynomial has a crystalline zero set (KSConstruction).
The Guinand-Weil explicit formula pairs two combs. On one side sit the ordinates of the nontrivial zeros of zeta, symmetrised and weighted by multiplicity. On the other side sit the prime powers at frequencies k log p with weights (log p) p^(-k/2), together with a smooth archimedean density and two pole terms. For an even test function g with transform h,
sum over zeros of h(gamma) = archimedean(h) - 2 sum over p, k of (log p) p^(-k/2) g(k log p) + poles
The prime comb exists unconditionally and is, in the kernel, a finite-height identity with the zeros: node MM_bragg_bridge states the explicit formula in diffraction form for a rectangle, with no limit taken, and node RH_limit_explicit_formula states the full limit form (Weil 1952 / Guinand 1948) for smooth compactly supported tests. What is not known is whether the zero comb is real. Unconditionally the ordinates are complex numbers; the Riemann Hypothesis says they are all real.
In Birds and frogs (Notices of the AMS, 2009) Freeman Dyson suggested classifying one-dimensional quasicrystals, on the grounds that if the zeros of zeta lie on the critical line then their comb is a quasicrystal with the prime powers as its spectrum, so a classification would have to contain it. The MIRRORMERE campaign runs this in reverse. It does not assume the zeros are on the line. It asks which weakening of the Fourier-quasicrystal axioms is the smallest one that still admits the zeta comb and still excludes the known counterfeits, and it tries to locate exactly where the hypothesis of reality enters. Kurasov and Sarnak already proved that the classical class is the wrong target: the zeta comb is not uniformly discrete (its counting function grows like T log T), so it is provably not a classical Fourier quasicrystal. Node MM_primelog_spectrum_dense and node MM_zeta_ordinates_not_uniformly_discrete put that obstruction in the kernel.
The draft axioms (telperion/docs/QC_AXIOMS_DRAFT.md) grade two axes: how dense the support may be, and how much is demanded of the spectrum and its weights.
| Variant | What it adds | Verdict in the draft |
|---|---|---|
| A | log-density support, pure-point spectrum on the prime log-lattice, no weight condition | live but fragile: separates Davenport-Heilbronn only through a loose lattice reading |
| B | A plus positive weights of the exact (log p) p^(-k/2) shape | recommended: the weight clause is unconditional for zeta and kills DH; the pure-point clause is the RH content |
| Bm | B with positivity replaced by multiplicative generation of the amplitudes from the prime layer (the Euler product fingerprint) | strictly sharper than B; falsified as an arithmetic-class predicate by L(s, Delta), see the zoo |
| C | A with signed weights, positivity dropped | dead by design: DH passes it, which isolates positivity as the killer |
| D | B up to a bounded defect k of off-line pairs; k = 0 is RH | live, partial: a finite k at each height is unconditional (Alpoge-Furman), driving it to zero is RH |
Claimed and in the kernel. The goal statement of the campaign, Weil positivity of the explicit-formula functional on Hermitian autocorrelations of smooth compactly supported tests, is equivalent to Mathlib's RiemannHypothesis (node MM_zeta_comb_membership_iff_rh, both directions). The same equivalence in two real parameters (node MM_rh_iff_gaussian_positivity), the unconditional free region of that parameter space (node MM_gaussian_positivity_small_lam_3e3), the Theta face with its heat monotonicity (node MM_theta_heat_monotone), and the finite instruments listed under the registry tab.
Not claimed. That either side of any of these equivalences holds. The goal node MM_zeta_comb_membership is a draft and stays a draft: it is RH by theorem. conjecture1_proved = False throughout.
An equivalence changes the coordinates of the wall, not its content. The campaign's own adversarial sweep (WALL_MAP_2026-09-21, section 5) reached that verdict and its replication agreed.
The falsification harness (telperion/examples/quasicrystal/zoo.py) runs each axiom clause against a zoo of control objects at height T = 100 and records a verdict. The matrix exists to be falsified: a clause that the counterfeit passes is dead, and a clause that zeta only passes conditionally is labelled so.
Rows are clauses, columns are zoo objects. Hover or tap a cell for the recorded detail. PASS: the finite certified check succeeded. FAIL: it did not. CONDITIONAL: the clause is RH-adjacent for that object, so the harness refuses to emit an unqualified PASS; the finite evidence is consistent with the clause but cannot certify it.
The spectrum side of the explicit formula is the comb with mass Lambda(n) / sqrt(n) at u = log n, supported exactly on the prime powers. Summing its cosines gives a trigonometric polynomial in the height t; as more prime powers are included, it develops sharp dips at the zero ordinates. This is the picture Dyson had in mind, drawn from the bundled ordinates. The ordinates are a float model (mpmath zetazero), not the certified Arb ladder, and the sum is truncated at n <= N.
The Davenport-Heilbronn function satisfies a functional equation of zeta's type but has no Euler product, and it has zeros off the critical line. It is the object every live axiom variant must reject. The certified inventory (zoo_data/dh_zeros.json, argument-principle winding numbers in Arb interval arithmetic, not kernel) records every zero of the function up to height 300 together with its real part. The plot shows them beside zeta's bundled ordinates.
On 2026-09-21 the campaign put Weil's criterion in the kernel and then rewrote it in two real parameters, a centre c and a width lam. For the Gaussian-derivative test the zero side of the explicit formula is
F(c, lam) = Re sum over zeros of m(rho) (gamma - c)^2 exp(-2 lam (gamma - c)^2), gamma = (rho - 1/2)/i
and node MM_rh_iff_gaussian_positivity says RH holds exactly when F(c, lam) >= 0 for every c and every lam > 0. Under RH every term is a nonnegative real. The wall is the sign of one explicit function on a half-plane.
Three regions are certified today, and each is labelled with the node that certifies it. Everything else is the wall. Drawn on log axes.
lam <= 3/2000 (node MM_gaussian_positivity_small_lam_3e3, a twelve-band layer cake with rational digamma floors; the earlier threshold was 10^-7, node MM_gaussian_positivity_small_lam). Mechanism: the prime side is exponentially small in 1/lam, the archimedean side is not. No zeros are involved.|c| >= envelopeCsharp(lam) (node MM_gaussian_positivity_envelope_sharp). The envelope is 2 pi e^(primeAbs(lam) + 1/2) plus small terms and grows doubly exponentially in lam; primeAbs is an explicit convergent series, evaluated here in floats.MM_gaussian_positivity_of_window: if every zero within distance D of c is on the line (the hypothesis WindowOnLine c D, which a finite ladder supplies as an Arb-conditional input, never as a theorem of this island), and lam is above an explicit threshold that is at least 1, then F(c, lam) >= 0. The band drawn is schematic: its left edge is the floor lam = 1, not the true threshold, and its right edge is the ladder height you pick below.The registry's proved height node is RH_li_rungs_of_height_4000_sharp, conditional on the tiled certificate's Arb band hypotheses. The wall-map memo cites a ladder height of 640000 but the registry holds no proved node at that height; the anduril ladder nodes are open. 3 x 10^12 is Platt-Trudgian (2021), literature only.
F(c, lam) computed in your browser from the bundled ordinates, all placed on the line (a float model of the RH side of the equivalence, truncated to the first 2000 zeros, so the picture is unreliable once c approaches the last bundled ordinate near 2515 or once lam is small enough for the tail to matter). Under RH the curve is never negative; the plot cannot show anything else because it assumes what it draws. Its purpose is to show the shape of the functional, not to test RH.
The plain Gaussian face Theta(c, lam) = Re sum m(rho) exp(-2 lam (gamma - c)^2) is also equivalent to RH (node MM_rh_iff_theta_positivity) and, unlike F, is heat-monotone in the width: Theta(., lam') is a Gaussian convolution of Theta(., lam) for lam' < lam (node MM_theta_heat_monotone), so positivity on the whole line at one width implies it at every smaller width. Move the slider: the smaller-width curve is always a smoothed, rescaled copy of the larger-width one. The free widths form an interval, and RH says that interval is all of (0, infinity).
Li's criterion: RH holds exactly when every coefficient lambda_N of the Taylor expansion of log xi(1/(1 - z)) at z = 0 is nonnegative. The li_positivity island carries the upstream equivalence (Bulka's LiCriterion, pinned) and prices RH rung by rung. Each rung is a paired zero sum, and the Bombieri-Lagarias explicit formula (node RH_bl_explicit_formula, hypothesis-free) says what each rung is.
Bars: lambda_N for N = 1..Nmax, computed in your browser as the paired zero sum over the bundled ordinates plus a smooth tail from the zero-counting density (a float model; the campaign's own numerics agree with a 3400-bit series to about 12 digits, see research/li_face_numerics.md). Highlights: rungs 0..4 (N = 1..5) are nonnegative in the kernel with no hypothesis at all (node RH_li_rungs_lt_five, from the low-height zero box). Rungs 0..19 carry a certified lower bound hlo that enters the kernel as a hypothesis (node RH_li_rung_certificates): Arb-conditional, shown as ticks.
If every zero up to height T is on the line, then rung n is nonnegative for every n + 1 <= 3 pi T / 2 (node RH_li_ladder_height), sharpened to n + 1 <= 2 pi (T - 1/2) (node RH_li_ladder_height_sharp). The rate is linear and explicit. The plot shows both lines with the heights that exist today. A verified height is finite; the tail of rungs is infinite; no finite prefix proves RH (node RH_li_ladder_reduction states exactly that).
Four campaigns, one schema. A node is draft until a readback is recorded, open once it is, and proved or refuted only after the verify gate has matched its verbatim statement against a Lean artifact that carries no sorry, is compiled by a runnable CI step, and prints only the three standard axioms. Goal nodes are drafts by design. Every readback below carries the independence label the registry records: self-attested when it was written by the same session family that wrote the node, independent read-back when mission audit accepted it from a different session and identity (for example the operator), judge-verified when a Comparator run (a separate checker and a second kernel) has re-checked the registered statement against the artifact. Grant digests, judge runs and required CI runs are shown on each card.
RiemannHypothesis (MM_zeta_comb_membership_iff_rh). Neither side is known to hold.MM_bragg_bridge); the limit form for smooth compactly supported tests, discharged from Anthropic's zeta-23-lean (RH_limit_explicit_formula); the Bombieri-Lagarias explicit formula on Li's class, hypothesis-free (RH_bl_explicit_formula).3/2000; below that width positivity is a theorem with no zeros involved (MM_wall_map, MM_gaussian_positivity_small_lam_3e3). Beyond an explicit envelope in the centre, positivity is also a theorem (MM_gaussian_positivity_envelope_sharp). The Theta face is heat-monotone in the width (MM_theta_heat_monotone).RH_li_rungs_lt_five); rungs 0..19 nonnegative modulo an Arb enclosure hypothesis each; every rung up to 2 pi (T - 1/2) nonnegative given zeros on the line up to height T, with T = 4000 conditional on Arb band hypotheses.riemannZeta s ≠ 0 for Re s > 7/8 (openai/math, 2026-10-06, Apache-2.0; replayed here through Comparator with nanoda on, node RH_zeta_zero_free_seven_eighths), composed with de Bruijn's heat-flow theorem on the dbn island (RH_dbn_real_zeros_of_zeta_halfplane: a zero-free half-plane at theta makes every zero of H_t real for t ≥ 2(theta - 1/2)^2). At theta = 7/8 this is t ≥ 9/32, stated and proved in one Lean environment at OpenAI's pin (RH_dbn_real_zeros_nine_thirtyseconds, unconditional, both kernels, judge-verified 2026-10-09). Classically Lambda ≤ 9/32 = 0.28125: the first bound below de Bruijn's 1/2 that is kernel-checked end to end, and weaker than the numerical bounds 0.22 (Polymath15) and 0.2 (Platt-Trudgian). RH is Lambda = 0; the conversion from a half-plane is lossy, and a half-plane at about 0.83 would be needed to beat 0.22 by this route. Paper and Lean sources: qrh-debruijn-newman, Zenodo DOI 10.5281/zenodo.23269134.n = 2, the Satake degree-two instrument that falsifies the multiplicative-twist clause on L(s, Delta).h280000, 10^6, 10^9) are open, and their island had no working CI at the last closure audit.conjecture1_proved = False in every campaign manifest and in this page.MM_zeta_comb_membership, RH_conjecture, AND_ladder_1e13, BG_conjecture1. All four are drafts.Lambda ≤ 9/32. The numerical bounds 0.22 and 0.2 are not in the kernel, Lambda ≥ 0 (Rodgers-Tao) is not in the registry, and Lambda = 0 is RH.WindowOnLine, the DH inventory, every zoo verdict. A hypothesis discharged by interval arithmetic outside the kernel is not a kernel theorem.telperion/docs/QC_AXIOMS_DRAFT.md, QC_PROGRAM.md, QC_LITERATURE.md, ARITHMETIC_FQ_MEMBERSHIP_SPEC_2026-09-16.md, RH_ROUTES_ROADMAP_2026-09-16.md, WALL_MAP_2026-09-21.md, WALL_THETA_FACE_2026-09-21.md.Everything on this page can be regenerated from the repository, and the claims behind it can be re-checked at three levels: the registry gate, the Lean kernel, and an independent second kernel.
The verify gate re-reads every campaign, matches each proved node's verbatim statement against its artifact, scans the artifact for incompleteness markers, and checks that a runnable CI step compiles the artifact's module. It is read-only.
cd telperion python -m venv .venv && .venv/bin/pip install -e . pyyaml .venv/bin/telperion mission status mirrormere .venv/bin/telperion mission verify mirrormere .venv/bin/telperion mission verify # every campaign
Do not run mission grant or mission audit to reproduce this page; they mutate the registry. The page is built from the same loader the gate uses.
Each example island is a self-contained Lake project with its own toolchain pin. The quasicrystal island and the rvm_bridge island are on v4.32.0; the li_positivity island is on v4.34.0-rc1. A full Mathlib build is required the first time.
cd telperion/examples/rvm_bridge/lean lake exe cache get # Mathlib oleans lake build # every module in the lakefile's defaultTargets lake env lean AxiomGuardRvMBridge.lean # prints #print axioms for each node theorem
The axiom guard is what the phrase "3-axiom clean" means: each theorem prints exactly [propext, Classical.choice, Quot.sound]. A sorryAx, a smuggled axiom, or native_decide's Lean.ofReduceBool fails the guard.
The Comparator (leanprover/comparator, from OpenAI's ten-proofs) exports a challenge module and a solution module with lean4export and asserts statement identity, an axiom whitelist, and a kernel replay in a second kernel (nanoda). The repository wires it as a CI job for the R3Cert proofs and for the emitter examples; telperion/docs/COMPARATOR.md is the reference.
cd telperion .venv/bin/pip install python-flint mpmath .venv/bin/python examples/quasicrystal/zoo.py # rewrites zoo_data/zoo_verdicts.json
The zoo consumes the certified Arb ladder (python-flint). Without flint the harness cannot run; this page was built without it and therefore uses the mpmath ordinate table for its pictures.
cd telperion .venv/bin/python explorer/build.py # rewrites explorer/data/*.json and docs/explorer/index.html .venv/bin/python explorer/build.py --check # exit 1 if the committed page is stale .venv/bin/python -m pytest tests/test_explorer_build.py -q
import mpmath as mp
mp.mp.dps = 30
gam = [mp.im(mp.zetazero(k)) for k in range(1, 201)] # ordinates (float model)
def F(c, lam): # the Gaussian-derivative face
return sum(2 * (g - c)**2 * mp.e**(-2 * lam * (g - c)**2) for g in gam)
def li(N): # paired zero sum, no tail
return sum(2 * (1 - mp.cos(N * 2 * mp.atan(1 / (2 * g)))) for g in gam)