Telperion keeps its research programs as a registry of formal statements: each one written down in Lean, tracked in TOML files, and marked proved only when the Lean kernel has checked a proof of exactly that statement. This page puts the first program to reach its goal in front: the Brualdi-Goldwasser problem, which asks which tree maximizes the Laplacian ratio, now answered for every size. Behind it are the three Riemann-hypothesis campaigns, which are open research: they hold many proved steps, and nothing here is a proof of the Riemann Hypothesis.
New here? Start with the first tab, then the registry. For the Brualdi-Goldwasser theorem on its own, with interactive labs, see the project page. 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 until an independent Comparator judge run is recorded for the node.
This is the program that shows what Telperion is for. The conceptual argument fits in a paper, but it rests on far more exact inequalities than anyone could check by hand: the sweep of spider shapes alone covers almost five million configurations. Telperion generated certificates for all of them, and the Lean kernel checked every one. The result is a complete answer to a question that had been open since 1984.
Take a tree T on n vertices. Its Laplacian L(T) is the degree matrix minus the adjacency matrix. In 1984 Richard Brualdi and John Goldwasser studied the permanent of this matrix and the Laplacian ratio
pi(T) = per L(T) / prod over v of deg(v)
and asked which tree makes it as large as possible. The ratio has a friendlier description: it is a weighted count of matchings, pi(T) = sum over matchings M of prod over edges uv in M of 1/(deg u deg v). So the question asks which tree has the heaviest matchings once every edge is discounted by the degrees of its two ends. Stars lose badly: every matching of a star has at most one edge, so its ratio is stuck at 2. Paths lose too, more narrowly: their ratio grows like ((1 + sqrt 2)/2)^n ≈ 1.207^n, while the true maximum grows like 1.2295^n. The answer sits in between.
A conjectured answer by Wu, Dong and Lai was refuted earlier in 2026 by Pant, whose counterexamples were caterpillars of hubs. After that the question was open again.
A cherry is a pendant path of length two. An arm is a vertex carrying some number of cherries. For every n ≥ 4 the maximizer is a spider of cherry arms: one centre, with only arms hanging from it, and almost every arm carrying exactly five cherries.
n ≥ 492, let s = 6(n - 1) mod 11. Every arm carries 5 cherries, except: for s = 1, 2, 3, 4, s arms carry 6 (but for s = 3 with n ≤ 722, and s = 4 with n ≤ 2319, it is instead 11 - s arms that carry 4); for s = 5, ..., 10, 11 - s arms carry 4.4 ≤ n ≤ 491 the maximizer is an explicit table. For small n it may also carry a few cherries or a leaf directly at the centre, and at n = 21 two different trees tie.Why five? An arm with j cherries has 2j + 1 vertices, and each arm contributes a fixed factor to the ratio. The fair way to compare arms of different sizes is the growth rate per vertex. The five-cherry arm is an 11-vertex block contributing exactly 621/64 = rho^11, where rho = (621/64)^(1/11) ≈ 1.2295, and no other arm matches that rate. The chart below draws it (the vertical axis is zoomed in, because the rates are close): move the slider to compare any two arms.
Try the arms yourself on the project site: the Spider lab builds any spider and computes its ratio exactly, and the Tree lab lets you edit an arbitrary tree.
Give every matched edge an extra weight λ, so that πλ(T) = ΣM λ|M| ∏uv∈M 1/(deg u deg v); Brualdi and Goldwasser's ratio is λ = 1. As λ increases, the best of these building blocks (leaf, cherry or arm) climbs A3, A4, A5, A6, …, with breakpoints 0.4305, 0.8725, 1.1924, 1.4356, … increasing to 1 + √5. There the arms run off to infinity and plain cherries take over. The value λ = 1 sits on the A5 rung.
One balance condition decides the whole ladder: a long arm's hub vertex must buy more, H(λ) = 2(1+λ)/(2+λ), than the same vertex would earn in a cherry, ζ(λ) = √((2+λ)/2). The balance point is a single cubic,
8(1+λ)^2 = (2+λ)^3 <=> (x-2)(x^2-6x+4) = 0, x = 2+λ,
with roots λ = 0, the bottom of the ladder, where the problem becomes the Randić index, and λ = 1 + √5, the top, where hub factor and cherry rate both equal the golden ratio φ. Explore it interactively on the project page: Why five: the ladder.
The ceiling along the ladder. That the best block also sets the growth rate of πλ, so that no pendant subtree of any shape beats it per vertex, is now proved for every λ > 0, with no gaps: by computer-assisted interval arithmetic (mpmath interval arithmetic, independently re-implemented in Arb) up to 1 + √5, and by a short hand argument from there on. On the whole range the maximal growth rate is the best-atom rate f*(λ), so the ladder is the whole story for the growth rate. The proof runs in six regimes: a degree-typed induction on (0, 0.1], in which the leaf, the cherry and the arms are exact types and every other branch carries a bound proportional to λ (the interval boxes include λ = 0 itself, and the only equality is the three-cherry arm A3); a power shoulder on [0.1, 0.47]; a quadratic shoulder on [0.47, 1.6]; a three-piece linear certificate on [1.6, 3.22]; a hand argument for the thin window [3.22, 1 + √5) where the best arm runs off to infinity (with about 15/(1 + √5 − λ) cherries; that constant is observed, not proved); and the cherry regime λ ≥ 1 + √5, where the cherry is the best atom and the growth rate is ½ log(1 + λ/2). In the cherry regime a short hand argument shows that the expected number of unmatched vertices in the weighted matching model is at least 2n/(2 + λ) once λ ≥ 2, which makes Tb(λ)/(2 + λ)n/2 nonincreasing in λ; anchored at the single point 1 + √5, where the ceiling is verified by calculus using the golden-ratio identities, that gives the ceiling for every larger λ. The cherry regime is also kernel-checked in Lean (formalization/cherry): the ceiling with equality only for the cherry, the bounds on the maximum, ρ(λ) = √(1 + λ/2) and the growth rate; for every λ > 0 it also checks the one-block formula, that the supremum ρ(λ) of Tb1/|b| over all branches is the growth rate, and the witness framework of the computer-assisted proof (the witness theorem (a)–(c), and (d) up to one step taken as a hypothesis). Below 1 + √5 the ceiling is now also proved in Lean on all of 0 < λ < 1 + √5, with no external input (part_B_full_eq): the inequality, its equality clause (equality exactly at the best arms) and its consequences. The Lean proof takes a shorter route than the six regimes: two piecewise-linear witnesses, on (0, 3/20] and on [3/20, 1 + √5), whose scalar conditions are all proved in Lean, as exact-rational interval checks over proved monotone enclosures and Bernstein polynomials of degree at most 6. The earlier Lean proofs of the window [3.22, 1 + √5) by hand and of [2, 3.22) by box checks remain in the project. As λ → 0 the rate is governed to first order by the Randić limit, which is why the bottom regime is anchored at A3.
The ladder among leaves, cherries and arms, and the cubic, are proved. That the best block also sets the growth rate of πλ is proved at λ = 1 in Lean (the sharp ceiling) and, for every λ > 0, by the argument above: computer-assisted (interval arithmetic) for 0 < λ < 1 + √5, and a hand proof (calculus at 1 + √5 with the golden-ratio identities, then a monotonicity argument) for λ ≥ 1 + √5. The range λ ≥ 1 + √5 is also kernel-checked in Lean, and so is 0 < λ < 1 + √5 (with its equality clause), with no external input, by two piecewise-linear witnesses. That result concerns the growth rate only, not the shape of the maximizers for λ ≠ 1.
For λ ≥ 1 + √5 the cherry is the best block, and every planted branch b obeys the ceiling T_b(λ) ≤ (1 + λ/2)^(|b|/2), with equality only for the cherry. Here T_b is the branch weight from the cavity recursion: a leaf has T = y = 1; a vertex with children has d = #children + 1, R = sum of the children's y, T_b = prod T_c (d + λR)/d and y_b = 1/(d + λR). The first chart shows (1/|b|) log(T_b/(1 + λ/2)^(|b|/2)), the normalized ratio T_b/(2+λ)^(|b|/2) per vertex and shifted so that the ceiling is the zero line: each curve is nonincreasing from λ = 2 on, the cherry's is flat, and from the anchor at 1 + √5 (where the ceiling reads T_b ≤ φ^|b|) none is above zero. The anchor is proved by one-variable calculus with the golden identities 1 + λ/2 = φ^2, 1 + λ = φ^3; the rest of the regime follows by that monotonicity.
The second chart divides by (1 + λ/2)^((n-1)/2) on a log scale: the maximum M_n(λ) (computed here over all 987 trees with at most 12 vertices) always lies strictly below the upper bound, which is never attained, and above the lower bound from a center carrying cherries.
The one-block formula, every λ > 0. With ρ(λ) = sup over all planted branches b of T_b^(1/|b|), every branch gives T_b^floor((n-1)/|b|) ≤ M_n(λ) ≤ (1+λ) ρ(λ)^(n-1) (the lower bound from a center carrying copies of b), and lim M_n^(1/n) = ρ(λ). The chart shows a branch's per-vertex rate divided by ρ; it touches 1 where the branch is a best block. At λ = 1 the arm A5 attains ρ(1) = (621/64)^(1/11).
Kernel-checked in Lean (formalization/cherry): for λ ≥ 1 + √5, the ceiling with its equality case, the strict upper bound for every tree, the lower bound, ρ(λ) = √(1 + λ/2) and lim M_n^(1/n) = √(1 + λ/2); for every λ > 0, the one-block formula; on all of 0 < λ < 1 + √5, the branch bound of the ceiling and a best arm, which give ρ(λ) = e^(f*(λ)) there, with no external input. The ρ drawn below 1 + √5 is that value, computed over the cherry and the arms Aj, j ≤ 400. Larger, interactive versions are on the project page: Why five: the ladder.
Because five-cherry arms dominate, the maximum grows like rho^n. The proof pins this down on both sides, (64/621) rho^n ≤ max pi ≤ 2 rho^(n-1). The chart shows the exact maximum divided by rho^(n-1). For large n it settles into eleven separate strands, one for each value of 6(n - 1) mod 11, because that is all the rule above depends on. The top strand is exact: for n = 1 (mod 11) and n ≥ 254 the maximum is exactly (26/23) rho^(n-1), and 26/23 is the limsup of the whole sequence.
Computed in floating point from the proved maximizers (the paper's figure data).
The statement uses only Mathlib's definitions on the graph side: SimpleGraph.IsTree, SimpleGraph.lapMatrix, Matrix.permanent, SimpleGraph.degree. The only project definitions it relies on are the short closed form F for a spider's ratio and the list bgChildren n of the maximizer's arms (formalization/Statement.lean).
theorem brualdi_goldwasser_upper (n : N) (h4 : 4 ≤ n) {V : Type} [Fintype V] [DecidableEq V]
(G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsTree) (hV : Fintype.card V = n) :
(G.lapMatrix R).permanent / (prod v, (G.degree v : R)) ≤ (F (bgChildren n) : R)
theorem brualdi_goldwasser_attained (n : N) (h4 : 4 ≤ n) :
exists G : SimpleGraph (Fin n), exists _ : DecidableRel G.Adj, G.IsTree and
(G.lapMatrix R).permanent / (prod v, (G.degree v : R)) = (F (bgChildren n) : R)
Symbols written out in ASCII here (N, R, prod, exists); the file uses the usual Lean notation.
The proof reduces every tree to a spider, then finds the best spider. The reduction is where most of the computation lives, and it changes character with the size:
| n | argument |
|---|---|
| 4 to 6 | exact rational evaluation of every tree |
| 7 to 149 | an envelope certificate: a sharded, kernel-checked Bellman bound showing that every tree which is not a spider is strictly beaten |
| 150 to 491 | refined per-vertex rate cells show the maximizer is a spider; an exhaustive kernel sweep of the spider family finds the best one |
| 492 and up | the same reduction to spiders, then exchange arguments and 223 polynomial certificates identify the rule |
Each certificate family is written by an untrusted Python generator and replayed by the kernel. Telperion's provenance layer freezes every family, so anyone can regenerate it and check that the Lean files come out byte for byte the same.
| family | what it certifies |
|---|---|
spider_table | the best spider for each 4 ≤ n ≤ 491 (exhaustive exact search, a 4,977,356-configuration sweep) |
envcert_g149 | the envelope certificate: every non-spider rooting with root degree ≤ 23 loses, 7 ≤ n ≤ 149 |
mid_cells | credited rate cells and root knapsack checks, 150 ≤ n ≤ 491 |
cand_certs | 223 polynomial certificates: the rule spider beats every candidate, n ≥ 492 |
The kernel is the only trusted component. A wrong certificate does not produce a wrong theorem; it produces a failed build.
Checked. The full formalization builds from scratch on Lean 4 v4.32.0 with Mathlib, and continuous integration rebuilds it on every push to the main branch. An axiom guard confirms that every headline theorem depends only on propext, Classical.choice and Quot.sound. A separate job regenerates every certificate family and compares it byte for byte with the committed Lean. And a Comparator check passed on 27 September 2026: a second, independent kernel (nanoda) and Lean's own kernel both accepted the proof against a statement that imports nothing but the definitions of F and bgChildren (run on macOS, without Comparator's Linux sandbox).
Still to come. The paper has not been refereed, and expert review of the statement is welcome.
About the registry tab: Telperion's registry records the Brualdi-Goldwasser campaign as it stood on 2026-09-24, before the final theorem was assembled on 2026-09-26. Its nodes show the path taken, including a refuted capstone and superseded formulations, and its goal node is still a draft there. The theorem above lives in the public repository and is checked there; it has not yet been registered as a node.
Everything you need is public: the repository, the reading guide for reviewers, the paper, and the project page with interactive labs. Archived as doi:10.5281/zenodo.22983412.
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: bg (Brualdi-Goldwasser, shown first) and the three Riemann campaigns mirrormere, rh and anduril. 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, 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.
n ≥ 4 the tree maximizing per L(T) / prod deg(v) is the explicit spider of cherry arms described in the first tab, and the maximum grows like rho^n with rho^11 = 621/64. Kernel-checked in the public repository, three standard axioms only. The registry's bg campaign predates this theorem (see the note in the first tab).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.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 Riemann campaign manifest and in this page.MM_zeta_comb_membership, RH_conjecture, AND_ladder_1e13. All three are drafts. (The bg campaign's registered goal, BG_backbone_conjecture, is also still a draft in this registry snapshot; the Brualdi-Goldwasser answer itself is proved in the public repository.)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, and the claims behind it can be re-checked at three levels: the registry gate, the Lean kernel, and an independent second kernel.
This part is fully public. The build needs a machine with about 96 GB of memory for its largest certificate files; Getting started has the details.
git clone https://github.com/DrMurphyIsIn/brualdi-goldwasser.git cd brualdi-goldwasser/formalization ./build.sh # builds every module, heavy files one at a time lake env lean Statement.lean # the Mathlib-vocabulary statement; prints its axioms cd .. && certificates/verify.sh # regenerate every certificate family, byte for byte
The commands below run in the Telperion development repository, which is private; they are listed so that the page's claims can be traced.
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)