A real stab at the
Riemann Hypothesis

The Riemann Hypothesis. Every nontrivial zero satisfies Re s = ½. Equivalently, writing γ_ρ := (ρ − ½)/i, RH says every γ_ρ is real — i.e. Ξ(t) := ξ(½+it), whose zeros sit at t = γ_ρ, has only real zeros. (The zeros of ξ itself would stay on a vertical line; it is Ξ that becomes a real-point spectrum.)

THEOREMN₀^s(T,2T) ≥ (⅔ − o(1))·N(T,2T),  N_d(T,2T) ≥ (5/6 − o(1))·N(T,2T),

unconditionally: at least ⅔ of zeros (with multiplicity) are simple and on the critical line, at least ⅚ are distinct; with the Montgomery–Taylor window the constants become 0.67250… and 0.83625…. Formalized in Lean 4, statement built on Mathlib’s own riemannZeta.

Level repulsion (δ → 0 suppressed) is numerical evidence for simplicity of low-lying zeros — the property Theorem A now proves in bulk. The smallest normalized gap found here is flagged as a mini Lehmer-phenomenon watch: near-ties of zeros, which make both simplicity and RH hard.

THEOREMG̃ ≈ P + Q, normalized so an isolated simple on-line zero contributes 1 to tr G̃:

• each on-line zero contributes a rank-one positive piece to P: trace 1 if simple; a zero of multiplicity m still has rank 1 but trace m;
• each off-line pair {ρ, 1−ρ̄} contributes to Q a block 2(aaᵀ − bbᵀ) of signature (1,1) — writing v = a+ib;
• so tr P ≤ N₀, n₊(Q) ≤ #off-line pairs, N ≥ s₁ + 2s₂ + 2p, and tr G̃ = (1+o(1))·N, where s₁ = simple on-line, s₂ = multiple on-line points, p = off-line pairs.

LEMMAIf P₁ ⪰ 0 and Q′ is Hermitian with n₊(Q′) ≤ b, then the matrix form of m² ≥ 2m−1; combined with the block bookkeeping — simple zeros on the rank side, multiple ones charged a flat 4 — it yields m² ≥ 3m−2.

N₀ˢ/N ≥ 2 − R(ψ₀) = 2 − 4/3 = 2/3

Sharpness: given only tr G̃, ‖G̃‖²_HS and the block structure, inequality (1.1) is sharp — improving on ⅔ by this rank–trace route would require pair-correlation information beyond Fourier support 1. Broader bandwidth-one certificates reach ≈0.682, and under RH semidefinite programming using form-factor positivity outside [−1,1] reaches 0.6792. Also from the paper: ≥85.8% of zeros of ξ′ are simple and on the line; averaged over primitive Dirichlet characters, 81.1% / 90.5%. Lab F (section 9) runs the September 2026 matrix-free proof of the same constants on the same zeros.

PROPOSITION 2.1 (Lamzouri) Let η ∈ L²(ℝ) be real and even with compact support and (η²)^∧(0) = 1, and put K := (η²)^∧, an entire function. For every finite multiset 𝒵 ⊂ ℂ invariant under complex conjugation, with m_z the multiplicity of z: sums over 𝒵 count multiplicity. No term K(z−s)² is required to be non-negative — that is the point, and the reason no positivity of K off the real axis is needed, which is what confined the earlier unconditional pair-correlation results to a thin horizontal strip.

Lamzouri writes the constant as Q₀(0) + 2∫₀¹ αQ₀(α)dα with Q₀ = f₀∗f₀; this page has carried it as R(ψ_MT), the second-moment functional at its critical point; both are ∫ψ² + ∬|u−v|ψ(u)ψ(v) with ψ = f₀, and the closed form is where the cotangent comes from. The weight w = 4/(4+(γ−γ′)²) that the unconditional lemma carries is removed by the exact per-pair identity K² = K²w + π²x²K²w/(log T)² — the two pieces are in the stat grid above — which is how the paper avoids a T-dependent test function.

Tried and shelved (in the spirit of the 650 discarded ideas in the paper’s Appendix B):

• Li/Keiper coefficients λ_n ≥ 0 from live zero data — tail truncation at accessible heights swamps λ₁, λ₂; the criterion is exact, browser data is not.
• Direct numerical optimization of the Weil quadratic form Q[φ] ≥ 0 over smooth bumps — rediscovers that positivity off bandwidth 1 is exactly the open problem.
• Finite-dimensionality hunting in the pair-correlation kernel (looking for an accidental Hilbert–Pólya truncation) — the kernel knows it must stay infinite-dimensional.

SURVEYThe record, re-checked 2026-09-07 against the community ledger at vibemathed.com (689 entries; a “Frontiers” page tracks records):

• Proportion of zeta zeros on the critical line: last moved 2026-08-10, to >67.25% (Claude; Alpöge–Furman). Six steps on that frontier — Hardy 1914, Selberg 1942, Levinson 1/3, Conrey 2/5, Pratt–Robles–Zaharescu–Zeindler 5/12, then 0.6725. Nothing since.
• Lamzouri, 2 Sep 2026 (arXiv:2609.02882): the same constants by a matrix-free route — a reproof, not a new number, and its Remark 3.4 states that C_MT is optimal for it. Lab F above.
• Bounded gaps between primes ≤ 212 (AxiomProver, 3 Sep 2026) and long gaps between primes (GPT-6 Astra, 3 Sep 2026): sieve results in the Maynard–Tao and Rankin lines. No bearing on the zero-proportion problem, which is a zero-density and pair-correlation question.
• The Radchenko–Viazovska Fourier-interpolation question (Bondarenko–Seip, arXiv:2608.13468): Fourier-invariant functions vanishing at √n. Kin to the explicit-formula duality, but it carries no statement about zero multiplicities or proportions.

Frontier value unchanged at 0.6725. Off the frontier, one thing did move, and the survey found it only by following the link the earlier ledger paragraph carried: teal-sea/zeta-lab now holds the n-point assembly as a Lean 4 theorem, n_point_bound, parametric in the point count and the pressure, with its finite certificate as a named hypothesis — and at three and four points the certificate is proved inside Lean, giving unconditional constants Φ₃ = 0.6727373345 and Φ₄ = 0.6728470198 for Mathlib’s riemannZeta. Registered at the Palomar Registry (PALOMAR-2026-08-25-000005, kernel-replayed, standard axioms), reviewed by no person — and rebuilt on this laboratory’s own machine on 2026-09-07: 8905 Lean jobs, exit 0, and #print axioms reporting exactly [propext, Classical.choice, Quot.sound] for all seven advertised declarations. So the defensible unconditional record is now two-tiered: 0.672500704 with human review (Alpöge–Furman), 0.6728470198 for anyone who accepts a kernel-checked Lean build, replayed by a registry and rebuilt here, without one. What that theorem does and does not accept from this page is worked out in dev/investigation/ASSEMBLY_AUDIT.md and summarised in the E·iv status panel below.

MODELThe certificate hierarchy. Modern proportion results are triples (test-function family, input tuple, extraction lemma). Placing them on one ladder:

route	input tuple	extraction	constant
Selberg–Levinson–Conrey mollifiers	mean values of ζ(s+α) with mollifier	mollified moments	1/3 → 2/5
Pratt–Robles–Zaharescu–Zeindler	long mollifiers	mollified moments	5/12
Montgomery 1973 (conditional)	pair-correlation 2nd moment, support ≤1	positivity of zero side (uses RH!)	2/3
Alpöge–Furman 2026	same support-≤1 inputs, unconditionally	rank–trace + Sylvester inertia	2/3, 0.67250
Lamzouri, Sept 2026	same support-≤1 inputs (BGSTB, unconditional)	one Hilbert-space inequality: Bessel + a²+1 ≥ 2a	2/3, 0.67250 — reproof; Lean-certified by AxiomProver
Ainta seven-point; Gohms	Alpöge–Furman + a per-block finite inequality (Arb-accepted, not Lean)	n-point assembly, informal in the manuscript, Lean in zeta-lab	0.6730085; 0.6730214 — conditional on the Arb run
zeta-lab three- and four-point, Aug 2026	same, with the finite inequality proved in Lean by interval cell lemmas	n-point assembly in Lean, Palomar-replayed, no human review	0.6727373; 0.6728470 — unconditional for Mathlib’s riemannZeta
this page’s chain floors	same inputs; a telescoping (coboundary) certificate instead of a per-block one	signed-endpoint variant of the assembly — Lean, in a branch (n_point_bound_signed)	0.6731094 (sharp) — conditional on the sweep
bandwidth-one obstruction [Easley–McAleer]	any support-≤1 certificate (256-periodic programs)	numerically enclosed optimization	≈0.68183
under RH, SDP [CGdL20]	form-factor positivity outside [−1,1]	semidefinite programs	0.6792

The gap this session probed: 0.67250 → 0.682, i.e. whether smarter extraction can spend the same support-≤1 inputs more efficiently.

RETRACTED BARRIER, WORKING EXPERIMENT. An earlier draft claimed a “combination barrier”: for PSD matrices, ‖A+B‖²_HS ≥ ‖A‖²_HS+ ‖B‖²_HS (true), whence additive combinations cannot help. The inference was invalid, in two ways. First, certificates normalize by trace: take A = diag(1,0), B = diag(0,1) — each has trace 1 and ‖·‖²_HS = 1, while C = ½(A+B) has trace 1 and ‖C‖²_HS = ½, so trace-normalized mixtures evade the inequality entirely. Second — and deeper — even where a mixture lowers the moment, the matrix wG₁+(1−w)G₂ makes one simple zero contribute wv₀v₀ᵀ+(1−w)v₂v₂ᵀ, generally of rank two: the chain’s conversion rank P₁ ≤ N₀ˢ no longer applies. What remains legitimate is a mixed-Gram statistic, governed by with both parents first normalized to a common trace N̄; the statistic dips below the better parent precisely when M < min(X,Y). Lab E·iii runs it on live zeros, next to its certificate-valid cousin: the rank-one-preserving window mixture φ_w = √w φ₀+√(1−w) φ₂, whose per-zero contribution uuᵀ keeps rank one (and whose cross terms are included).

E·iii — LIVEMixed-Gram statistic vs window mixture: smoothed-indicator parent vs Montgomery–Taylor parent on the same grid and zeros.

PROPOSITION B (slack formula). In the idealized frame of Lab E·i with s₁ simple on-line zeros, s₂ doubled zeros, and p off-line pairs at offset s>0, all four quantities are exact: where B = 4 tr G̃ − 2N − ‖G̃‖²_HS is the certified bound. Verified to machine precision across the parameter grid (including fractional offsets and the boundary s = 0, where an off-line pair degenerates into exactly a doubled on-line zero — coherence check). Three readings:

• Tightness. For s>0, slack vanishes iff there are no off-line pairs: multiples cost nothing — the flat charge 4 absorbs them exactly. (At s = 0 an off-line pair degenerates into exactly a doubled on-line zero and likewise costs nothing.)
• Monotone offset penalty. 8ps²(1+s²) increases in s>0: larger offsets depress the certified bound more; s→0 recovers the doubled on-line zero exactly.
• Hypothesis, not consequence. s is an artificial orthonormal parameter with no proven bridge to |β−½| in the real Gabor frame. If an offset-sensitive inequality were proved for the real frame, partitioning zeros by scaled distance |β−½|log T and combining with zero-density estimates would inject information beyond the first-two-moment ceiling — flagged as an open experiment.

An elementary computation — useful as a conjecture generator and as an explicit accounting of where every unit of slack goes in the model.

NUMERICAL OBSERVATION (exploratory). Beam 2’s second-moment identity, normally verified from the prime side, can be probed from the zero side: build G̃ from live computed zeros near t = 400 and measure ‖G̃‖²_HS/tr G̃. At d = 16 this page measures 1.256 against asymptotic c⁻¹_MT = 1.32750; across frame lengths d = 8…24 the ratio fluctuates in 1.15–1.28 without clean convergence. Scale disclaimer, stated properly: this experimental frame carries ~20–30 zeros from a ~30-unit interval around t = 400, whereas the theorem’s regime is d ∼ N(T,2T) ≈ 289 across all of [400,800] — and the O(√T log T) localization error belongs to that full-width argument, not to this toy. What the study measures is sensitivity to frame length, not asymptotic convergence.

LEDGERApproaches tried this session, with final status.

approach	status	one-line reason
Li/Keiper coefficients from live zeros	dead	tail truncation swamps λ₁,λ₂ at accessible heights
sieve-relaxed positivity beyond support 1	dead	sieve upper bounds have the wrong sign — certificate needs the moment small
interlacing ξ′/ξ	dead	presupposes real zeros — circular
Connes trace formula	dead (here)	equivalence needs a cuspidal input of RH-depth
de Branges Hilbert-space kernels	dead (here)	known structural gaps recur
Turán power sums	dead (here)	yields hyperbola regions, never β=½
Nyman–Báez-Duarte/Beurling completeness	dead (here)	finite-dimensional approximations carry no proportion content
third/fourth-moment extraction tr G̃ᵏ	blocked → open	X≈T needs three-prime correlations; kλ≤2−ε Christoffel tradeoffs untried
beyond-support parametrized positivity search	open	restricted families are legitimate probes (Weil-criterion discussion)
ξ″ weight-system transfer of Remark 7.1	open follow-up	plausible, mechanical-looking, unverified here
stability-defect extraction [external candidate family]	open — reproduce first	claimed +0.0005078 via seven-point overlap certificate; audit: finite cert sound, pruning defect repaired; needs end-to-end independent rebuild
raw-addition window combinations	retracted	trace-normalized mixtures evade the PSD inequality — rebuilt as E·iii
E·iii mixture statistics	numerical only	mixed-Gram dip + rank-preserving curve; feeds no theorem yet
Beam-2 identity from the zero side	numerical only	HS²/tr near c−1MT at toy scale; sensitivity study in E·ii
Proposition B slack formula	numerical + hypothesis generator	exact in-model; offset bridge to real frames unproven
overlapping seven-point blocks	active numerical probe	exact cyclic reindexing; an additive coboundary certificate audits at 0.003957227285, and an exhaustive subdivision verifies the chain floor 0.003956 in double precision, and 0.003956 with proved enclosures — the two now equal, and both strictly above the published 19/5000
Hilbert-space route (Lamzouri) as a base for a stability-defect term	open — untried	for an all-simple multiset the slack is exactly the off-diagonal Gram mass; a defect term would have to price it from support-≤1 inputs — the same wall, seen from the other side

The Riemann hypothesis stands exactly where it did.

PROPOSITION C (cyclic block identity). For a periodic chain of nonnegative gaps g₀,…,g_L−1, let the seven-point functional be evaluated on every shifted six-gap window. Directly reindexing its pair terms gives the exact finite identity A pair spanning s gaps occurs in exactly 7−s shifted windows, cancelling the local coefficient 2/(7−s). The verification suite checks the direct and reindexed formulas on periods 1 through 9.

E·iv — OVERLAPPING-BLOCK TILING PROBE.

Evidentiary status — read before quoting any number here. A review found the suite was accepting recorded sweep results without replaying them, so an invented or stale row would have passed. Rows now carry a traversal checksum, stirred once per box from that box’s computed bound and shape, plus hashes of the certificate and every source that determines the result. Three statuses, which had all been called “verified”: (a) replayed by the suite every run — fast to 0.0025, rigorous to 0.003, plus the bare-block controls; (b) transcripted but too large for a test to redo, hashes checked, and the suite says it did not replay it — fast to 0.003956; (c) reported with no transcript — the entire rigorous ladder above 0.003, including the headline, stale in any case because the trigonometric bound moved. Those are being re-run starting at 0.0038, the rung that would recover the published threshold.

The honest ladder, today (2026-09-08). Replayed rigorous floor 0.003. Transcripted rigorous floor 0.003956 — the sharp certificate, re-run on 2026-09-07 after a review found its rigorous row had never been committed: 67 608 431 boxes, checksum 37308f214a50bb25, current input hashes, replay command included, but not replayed by the suite: a reproducible claim, not an independently reproduced result. Its proof tape (74 694 256 nodes, emitted separately in double precision) is structurally verified in full and Arb-checked on a 5000+5000 sample with nothing refuted, by a checker that an external review of 2026-09-07 found unsound in four places (float hulls, an acceptance comparison in floats, kernel tables that stopped at distance 30, a tube leaf accepted on its word) and that was repaired, put under nineteen negative controls, and frozen the same day; the complete verification of every node was then done by a compiled sibling of that checker (dev/tapecheck, Rust with correctly rounded intervals, the Python one being two milliseconds an obligation and this machine no supercomputer): all 26 688 759 discharged leaves and all 21 317 467 collapses confirmed, nothing refuted, nothing unresolved, 41 minutes on eight threads (dev/tapecheck_sharp_full.results.json). That is an independent check, in double-precision intervals, of every claim the double-precision sweep made; it is not Lean, and the theorem still takes the sweep’s inequality as a hypothesis. It now exceeds the published local floor 19/5000, and through n_point_bound_signed it projects to 0.6731093501 with that sweep’s coboundary inequality as the only remaining hypothesis. The compact certificate’s rigorous 0.0038 row (7 048 899 boxes, checksum 791eadaf99dafbf6) matches the published certificate exactly and is kept for the record. The defensible unconditional record on this ladder is 0.6725007037 — on this ladder, meaning the additive certificate. The pair certificate reaches much further and its status is stated separately in “Where this stands, now”; the two are not rungs of the same ladder and should not be read as one. An earlier version of this paragraph ended “0.0039 is running next”, which stopped being true some sessions ago and stayed on the page: nothing is running it. For scale, the earlier untranscripted 0.0038 run reported 7 200 335 boxes against the 7 048 899 measured now — the difference is a Taylor form added after that run and never re-measured against it. Neither number was wrong; nothing was tracking which code produced which.

Read this first — what is established, and at what strength. Exact: H_MT = 2 − R(ψ_MT), with ψ_MT = cos(√2 s) the unique critical point of the second-moment functional — derived from its Euler–Lagrange equation, and the reason the √2 and the cot(1/√2) in the published constant are there at all. Also the cyclic block identity, the reversal cohomology lemma, the telescoping lemma turning a per-edge coboundary floor into a chain floor with an O(1) boundary term, the two-phase charge identity, the nonnegativity and compact support of the weight’s Fourier transform, and the projection arithmetic two-sided-pinned at the assumed floor — sixteen Lean theorems, standard axioms only, which is the count the axiom audit prints. Exhaustively subdivided in double precision: with the additive record certificate, the chain floor 0.003956, for every gap sequence, periodic or not — 99.1% of the whole available improvement, against a ceiling of 0.6731102697. Exhaustively subdivided with proved enclosures: with the pair-state certificate and the tube argument, the chain floor 0.003957393309109344 − 2.186×10⁻¹⁵ — the alternating chain’s own energy, so the alternating chain is the minimiser to within 2.2×10⁻¹⁵, 100% of the available improvement; see below, including what it rests on and what is being recomputed. With the additive record certificate, the chain floor 0.003956 — the same floor the double-precision sweep reaches, so these two rungs have merged. 67 608 431 boxes, proved trigonometric error bounds, outward-rounded arithmetic throughout, projecting to 0.6731093501 against 0.6730085279 (99.1% of the whole available improvement), with Lean pinning that constant two-sidedly, strictly above the published pin and strictly below the alternating-chain ceiling. (It cannot lie between the published pin and the double-precision one: identical floors give identical projections, which is the whole point of the merge.) Numerical only: the certificate coefficients, every floor above the swept ones, the kink and Bloch numbers, and the whole block-size scan. The external shifted-block assembly, re-examined 2026-09-07: it is Lean now — n_point_bound in teal-sea/zeta-lab, whose projection formula Φₙ(n,c,m,p) = (H − (n−1)(m−1)/(pm)) / (1 − c(m−(n−1))/m) is term for term the projectedSimpleZeroBound every number above was pushed through, and which takes n and p as free parameters (so the block-size scan and the pressure optimisation are questions about a well-posed theorem). But its hypothesis is a per-block floor, c ≤ F(g) for every block, which no chain floor on this page satisfies: the isolated-block minimum is 0.003826. The Lean proof consumes that hypothesis in exactly one place, summed over the m−(n−1) windows of a sorted block, so the exact missing lemma is the same theorem with the window-sum inequality as its hypothesis — which a telescoping certificate supplies once its endpoint loss is paid. That variant is now proved, in a branch of zeta-lab (n_point_bound_of_windowSum, standard axioms; the original theorem re-derived from it as a regression), together with the adapter from a coboundary certificate to it. The endpoint loss is the oscillation of the state potential, not the single-edge amplitude the tail lemma uses — a reviewer caught that the first estimate here was too small — and it is 0.00171 for sharp, 0.00815 for the pinned pair certificate. Paid conservatively, the sharp chain floor projects to 0.6731051, not 0.6731094, and the pair certificate to 0.6730895, not 0.6731103; the amplitude-minimised certificate is the better one once the chain has ends. A signed-endpoint extension that keeps the loss through the offset average recovers 0.6731094 for sharp under the cap cW + B ≤ 1, met at 252 windows — and that extension is now Lean too (n_point_bound_signed, standard axioms), so the endpoint penalty is gone from the theorem and survives only as the cap. The sharp potential itself, its 51 exact coefficients, its bounds and its oscillation are Lean too (sharp_chain_bound_signed_concrete), so between the shipped certificate and a theorem about ζ at 0.6731094 the single remaining hypothesis is the sweep’s coboundary inequality. Both scores still sit above zeta-lab’s conditional eight-point 0.6730530 and its measured seven-point per-block ceiling 0.6730296. Everything downstream stays conditional on this page’s own sweep arithmetic, whose rigorous sharp transcript turned out to be absent and is being re-run; dev/investigation/ASSEMBLY_AUDIT.md has the derivation and both scores.

What none of the rungs are. Every floor above is a statement about the auxiliary chain — a one-dimensional particle system with a pressure term and an oscillating pair interaction. None of them is a theorem about primes or about zeta zeros. Nor is the phase diagram: the certified orbits, the period-five window, the interface tensions and the defect costs are statements about that same chain, and the pressure is an auxiliary parameter of it, not a quantity with an arithmetic meaning. The bridge from the chain to a simple-zero proportion is the external shifted-block assembly, which nobody here can check, so every projected number on this page is conditional on a step this page does not contain. That remains true of the strongest rung, and would remain true of a fully rebuilt one.

The isolated-block search reproduces the known numerical floor candidate Exhausting the original verifier’s three gap basins modulo rotation and reflection for periodic chains through period eight finds its best candidate at the alternating two-cycle Analytic-gradient searches with long-wave, quasiperiodic, random, and both alternating-phase starts were then run through period 64. Every tested even period returned the two-cycle; odd periods carry a localized phase kink, with period 9 at ≈0.003973743750. The observed candidate separation is 1.31162×10⁻⁴. This is evidence that an isolated minimizer cannot tile without paying an overlap-compatibility cost, but not a proof. Note that the period-by-period search alone could always have missed a continuous or aperiodic configuration; the coboundary certificate below does not have that gap, because a per-edge floor telescopes over any gap sequence, periodic or not. Numerically the chain infimum is therefore pinned inside [0.003957227285, 0.003957393309] — width 1.66×10⁻⁷ — over all configurations, not just the tested periods. If one certifies the conservative global floor 0.00395 with boundary error o(m), the existing shifted-block assembly projects a simple-zero constant of 0.6731055997, versus 0.6730085279 from the published local certificate.

Dual experiment: on the two-gap alphabet, a 32-state Bellman computation closes numerically at 0.003957393309 on the alternating cycle. Continuous smooth potentials did not close: the best audited candidates were ≈0.00389481 (one-body) and ≈0.00391999 (degree-two clipped Walsh), and a degree-five search did not improve the latter.

What closed it: drop smoothness. Antisymmetrising an additive state potential Φ(s)=Σ_kψ_k(s_k) gives an exact normal form with two free functions,

and every antisymmetric additive potential is of this shape. Two facts come free: R is reversal invariant by construction, so the reflection quotient that caused the autopsy below is legal here; and on both alternating blocks every feature cancels, so R = F₆ = 0.003957393309 there for any (a,b) — a hard ceiling equal to the conjectured chain minimum. Letting a and b be free piecewise-linear functions on a 51-knot grid and solving the max-min by LP cut generation raises the audited floor from 0.003923427087 to 0.003957227285, i.e. 1.66×10⁻⁷ below the ceiling. Three JavaScript adversaries sharing no code with the search agree to ≈4×10⁻¹⁸.

Payoff curve — 0.00395 was the wrong scoreboard. The projection is strongly concave in the certified floor. Between the published 19/5000 certificate (0.6730085279) and the ceiling (0.6731102697) the previous 0.003923427087 candidate was already buying 78% of the available gain, and the record certificate buys 99.9% (0.6731101602). Chasing the last 10⁻⁷ is worthless; running the interval sweep against a certificate with margin is not.

Three certificates ship. The record one audits at 0.003957227285 (99.89% of the gain) over the cube [0,28]⁶ with amplitude 5.20×10⁻³. The sharp one — the record certificate put through the amplitude-minimising refine stage at target 0.003957, within 2.3×10⁻⁷ of its own floor — audits at 0.003956981146 (99.73%) over [0,16]⁶ with amplitude 1.28×10⁻³, and is the sweep target: it keeps essentially all of the record floor in a cube 29 times smaller by volume. The compact one (0.003950948242, 96.0%) is kept because the recorded sweeps used it. All three are re-audited from scratch by the verification suite.

Two lessons, neither obvious beforehand. The refine stage is not merely tidying for the tail lemma: run at a high target it improves the floor, the cube and the boundary term at once, and the m = 7 attempt failed partly for want of exactly this stage. And it can be driven almost to the ceiling — thirty rounds at target 0.003957 converge, after an alarming excursion down to 0.0038736 around round six. I called that excursion a divergence and killed the run; the two rounds already in the log showed it recovering. Wrong twice: in the claim, then in the correction that called the question open. Settled now, and sharp is the answer.

The sweep runs. Two routes failed first, and both are worth recording. Naive subdivision is hopeless: the box bound’s enclosure slack is first order, about 0.045×diameter, so a 5×10⁻⁵ margin needs diameter-10⁻³ boxes and the cube holds ~10²⁰ of them. A fully separable certificate — replacing the 6-D inequality by one-dimensional sup-convolution constraints — is far too lossy: cut generation drove it below 0.0031, under the published 19/5000, still descending. Separability discards exactly the correlation the compatibility effect lives in.

What works is the monotonicity reduction: when the enclosure of ∂R/∂g_k over a box misses zero, the minimum lies on a face, so the box collapses and loses a dimension. That plus exact one-dimensional ranges for w and w′ — w is nonnegative with zeros exactly at the zeros of K and one interior maximum between consecutive zeros, so its range over any interval is a table lookup — turns 10²⁰ boxes into 10⁷. The sweep completes at 0.003956 in 54 518 075 boxes and 458 seconds, and telescopes to a chain floor for every gap sequence: projected simple-zero constant 0.6731093501 against 0.6730085279, which is 99.1% of the entire improvement the alternating-chain candidate could ever deliver. It sits 9.8×10⁻⁷ below sharp’s own audited floor, so the certificate is again the binding constraint, not the subdivision.

Control. With the zero potential the reduced cost is the bare block functional, so the same machinery exhaustively reproduces the published Proposition F₆ (F₆ ≥ 19/5000 for all nonnegative gaps) in 3 147 403 boxes, sharing no code with the external Arb certificate — and it refuses 0.0039 with an explicit counterexample at 0.003840817, correctly, since the isolated-block minimum is 0.003826231219. A verifier that never fails proves nothing.

Closing the floating-point gap. That table leans on Math.sin, which is not correctly rounded and carries no proved error bound. The kernel is now also implemented with proved bounds: Cody–Waite reduction against a four-term split of π/2, Taylor series to r¹⁹ and r¹⁸ whose truncation is below the first omitted term, and outward rounding by 2.3×10⁻¹⁶ relative plus a 10⁻³²⁰ absolute floor — sound because IEEE 754 + − × ÷ are correctly rounded, the absolute term because the relative one alone vanishes into subnormals and was excluding exact products there. Against a 6174-row mpmath oracle at 60 digits — biased towards multiples of π/2 and tiny offsets from them, where argument reduction cancels catastrophically — containment holds everywhere and the worst true error is 9.99×10⁻¹⁶. The declared bound is 8×10⁻¹⁵, eight times that. An earlier 2×10⁻¹⁵ carried only twofold headroom; the uniform random comparison against the engine’s own Math.sin that had been standing in for the oracle never reached the cases that show it. For the record, on those rows Math.sin reaches 1.11×10⁻¹⁶ and this implementation 9.99×10⁻¹⁶ — it is the less accurate of the two, and is used anyway because its error is bounded by an argument rather than by a vendor’s reputation.

Naively interval-evaluating the weight’s formula is not good enough: its slack grows with the interval width even where the weight is flat, about thirty times looser than the exact range, which would demand boxes 700× smaller and 10¹⁷ of them. Centered forms fix it — f([a,b]) ⊂ f(m) + f′([a,b])·[−ρ,ρ] has slack proportional to the width times the variation of f′, measured at 1.35×10⁻⁶ at width 10⁻³ against 7.3×10⁻⁴, 540× tighter and second order as advertised. The rigorous sweep then costs about 2.4× the boxes and 7× the wall clock, which is affordable.

And it finishes. The rigorous sweep costs about 1.9× the boxes and 9× the wall clock of the table version. It completes at 0.0038 in 7 200 335 boxes (equal to the published floor), at 0.0039 in 14 817 467, at 0.00392 in 18 260 117, at 0.00394 in 25 523 525, at 0.003949 in 42 531 993, and — once the sharp certificate removed compact as the binding constraint — at 0.003952 in 40 938 447 boxes (fewer than 0.003949 had needed on compact, because the margin to resolve is larger), at 0.003954 in 47 516 991, and at 0.003956 in 67 608 431 boxes — exactly the floor the double-precision sweep reaches. All strictly above 19/5000 after the first. That projects to 0.6731093501 against 0.6730085279: 99.1% of the whole available improvement, established with proved enclosures rather than with Math.sin. Two attempts to narrow the remaining overhead failed instructively: a second-order Taylor form for the value bought 0.1% where a sixth-power argument predicted eightfold, and the same treatment for the derivative bought 0.4% for 1.7× the wall clock and was removed. The overhead is not about local expansion order.

What it found on the way. Cross-checking the enclosures against the laboratory’s own kernel exposed a real bug: sinOverXDerivative switched to (x cos x − sin x)/x² at |x| > 10⁻⁵, where that form cancels catastrophically — at x = 10⁻² the numerator is ~4×10⁻⁷ assembled from terms of size ~10⁻², losing eleven digits. Eleven of 240 000 sampled derivatives fell outside their true enclosure. Fixed; no golden pin moved. A verifier is only worth what its cross-checks catch.

Unusual stone: seven is not the best block size. The programme inherits n = 7 from the manuscript and nobody varied it, though the projection already takes n as a parameter. For every n the chain minimiser is again the alternating two-cycle, and pushing each chain minimum through the same projection peaks at n = 8: 0.673129621611 against 0.673110269740 at n = 7. The trade-off is visible — a larger block raises the floor, which raises the defect coefficient, but lengthens the span term subtracted from it — and n = 7 sits on the rising side of the peak. One step along adds 1.9×10⁻⁵, about a fifth again of the whole chain-versus-block improvement.

But not by the easy route. Certifying the seven-gap block minimum and stopping is worthless: 0.004388737 at n = 8 projects to 0.673042788, a gain of 0.34×10⁻⁴ — below the 0.78×10⁻⁴ the n = 7 chain certificate already delivers with proved enclosures. The break-even n = 8 floors are 0.0044565 (to beat the n = 7 rigorous sweep) and 0.0044919 (to beat the double-precision one), against a ceiling of 0.0045244. So n = 8 pays only with a coboundary certificate capturing half to three quarters of the compatibility gap. Measured seven-dimensional cost grows like margin^−1.3 (against margin^−0.5 in six), putting a useful n = 8 sweep at order 10⁸ boxes — hours, not minutes, but not out of reach.

A first m = 7 certificate, and the three ways it fails. Ninety rounds of cut generation produced one that does not work, and the failure modes are the useful part. Convergence is far slower than at m = 6 (96.3% of the ceiling in 90 rounds, against 99.98% in 26). Its small-box floor 0.004355584 is below the trivial zero-certificate floor 0.004388737, so the search has not yet bought anything. And it has no amplitude control — the m = 6 pipeline’s amplitude-minimising refine stage was never generalised — so its amplitude is 0.36, its own tail lemma demands the cube [0,1094]⁷, and an audit over that cube returns −0.053: valid only on the box the search happened to look in, which is not a certificate at all. Against a break-even of 0.0044565 this is not close. The n = 8 route needs more search, not more sweeping — the sweep side is solved.

Two caveats remain real. This is conditional on the published assembly being valid for general n, which this page cannot check; and the n = 8 floor is a numerical candidate with no certificate behind it. The third caveat — that the sweep would gain a dimension — has been tested. Seven dimensions is feasible. The whole machinery, rewritten for a general block, reproduces the six-gap modules box for box, and a seven-dimensional exhaustive sweep terminates: 44 339 boxes at 0.003, 1 485 735 at 0.004, and a correct refusal with an explicit counterexample at 0.0045. The seven-gap isolated minimum is 0.004388737 at a palindrome, against the n = 8 chain candidate 0.004524419 — a compatibility gap of 1.36×10⁻⁴, the same order as at n = 7. The normal form generalises to R = F₇ + a(g₀)+a(g₆) + b(g₁)+b(g₅) + c(g₂)+c(g₄) − 2(a+b+c)(g₃), three free functions instead of two, and the linear programme’s cap there sits at exactly the n = 8 chain candidate, so the ceiling argument survives the odd block size.

Unusual stone: the compatibility gap is an end effect. The number this whole probe chases is the chain minimum minus the isolated-block minimum — 1.31×10⁻⁴ at n = 7. Measured at every block size it does not grow: 1.41, 1.52, 1.31, 1.36, 1.30, 1.53, 1.18 (all ×10⁻⁴) for n = 5 through 11, oscillating with block parity rather than trending. The block minima survived six differential-evolution runs at four times the usual budget without moving, so each gap is a lower bound on the true one.

That is what an end effect looks like: a finite block is cheaper than the chain because it can relax its two free ends, and the saving does not care how long the block is — the bulk is already paying chain prices. It also sharpens the block-size question: since compatibility is worth the same ~1.3×10⁻⁴ at every n, the choice of n is governed entirely by the projection’s own trade-off between a floor growing with n and a span term growing with n too. Which is why the peak at n = 8 is shallow on both sides.

A local theorem, proved rather than measured. The lag-six truncation is by index, not distance, which defeats every Fourier argument for the energy itself. It does not defeat the Hessian: at a two-periodic state Ĥ_ab is a finite sum of w″ terms vanishing identically for |a−b| ≥ 6, so a two-site Bloch decomposition reduces positive-definiteness to a one-variable interval problem. Two things are now certified, both in well under a second. Existence and uniqueness: a Krawczyk test on ∂E/∂L = ∂E/∂H = 0 proves a unique two-periodic critical point, pinned by iteration to L ∈ [1.0416801034484717, 1.0416801034485021], H ∈ [1.9794672314032040, 1.9794672314032447]. A spectral gap: for every momentum q ∈ [0, π] and every two-periodic state in a box of halfwidth 10⁻⁴ about it, the smaller Bloch eigenvalue is at least 1.6. So the alternating two-cycle is a strict local minimum with a certified gap of 1.6. The enclosure is 3.0×10⁻¹⁴ wide in L and 4.1×10⁻¹⁴ in H, not “the last bit of a double”: that figure came from a Krawczyk operator that collapsed the gradient enclosure to its midpoint, and so reported an enclosure narrower than the uncertainty that produced it. Unsound, now repaired, and the widths above are what a correct operator gives.

The same theorem again, with none of my arithmetic. All of that rests on a home-grown interval base: sine and cosine I wrote with error constants I chose, derivatives of w I differentiated by hand, an outward-rounding convention I invented. Each of those three has produced at least one unsoundness here. So the theorem is proved a second time in Arb (python-flint, 200-bit balls with proved enclosures), with Arb’s own sine, and with w′ and w″ obtained by Taylor-series arithmetic on the definition of w rather than by hand. Only the mathematics is shared. Arb is not a free pass, though: three defects turned up in the thin layer between it and the mathematics, all mine — b**2 returns nan for a ball centred at zero and b*b straddles zero (ball multiplication does not know its factors are the same number), so the eigenvalue bound was feeding nan into a square root where it read False against every comparison; a ball’s radius crosses into Arb as a Python float, and float() rounds to nearest, which for a radius is inward half the time; and outward rounding then leaves a sum of squares reaching a hair below zero, bringing the nan back. All three are fail-safe and all three cost sharpness, and the file now tests its own ball constructors on 891 cases before it proves anything. The two agree — and Arb resolves the point about 10⁴⁵ times more finely: L = 1.04168010344848698644197575211 and H = 1.97946723140322440794242316550, each to a radius near 2×10⁻⁵⁹. That is the strong direction: the true L sits 1.5×10⁻¹⁴ into the 3.0×10⁻¹⁴-wide interval above, so the double-precision intervals are correct and nearly centred, not merely self-consistent.

Two facts Arb adds outright. The gap is at least 1.6612, not merely 1.6, in 3731 momentum intervals; numerically the minimum is 1.66128101824, and bisection gets within 10⁻⁵ of it before first-order interval slack starts costing exponentially many subdivisions. And the minimising momentum is certified, by an argument a gap certificate cannot make: one point evaluation bounds the minimum from above by 1.661281018241, and the eigenvalue is then certified to exceed that bound everywhere outside a window, so the minimiser must lie inside it. In 16954 intervals that gives q/π ∈ [0.925, 0.933], with the numerical minimiser at 0.9290451141. The 0.929 withdrawn from an earlier draft as a scan reading is now a certified two-decimal statement. Nothing else depends on it.

What it does not establish — and that gap is the whole problem. It is local. It says nothing about configurations far from the alternating state, nothing about the wall energy between the two alternating phases, and nothing about the global floor. A coercivity statement E(g) − E(g_alt) ≥ c·dist(g,𝒜)² + τ·(walls) needs this constant and a wall tension and control of everything between. It also produced a correction, and this time an enclosed one rather than a computed one. The (1.041680, 1.979467) quoted throughout this page is a six-decimal rounding; the chain energy at the certified critical point, rigorously enclosed, is [0.003957393309106188, 0.003957393309112507], while the ceiling constant quoted everywhere here, 0.003957393309209766, lies outside that interval — about 10⁻¹³ too high, having been evaluated at the rounding. Immaterial to every projection, and now a certified statement rather than a number read off the ordinary floating-point kernel, which carries no bound and should not have been called a true minimum.

Required autopsy: an initially reported one-body floor ≈0.00399418 was false. The search had quotiented gap words by reflection, but an oriented coboundary is not reflection-invariant. Enumerating all 729 ordered three-basin words produced an explicit reduced-cost counterexample ≈0.00372737. The counterexample is now pinned in the suite.

A radius for it. “Strict local minimum” with no radius is a statement no global argument can use, and this page said exactly that. The radius is a finite computation, off the two-periodic slice. For g in the sup-norm tube of radius r about the alternating state every distance D_i,s lies within s·r of its crystal value, so the interval Hessian over the tube is a finite object, and Taylor along the segment (the tube is convex) gives E(g_alt+u) − E_alt ≥ (c/2)‖u‖₂² whenever ‖u‖_∞ ≤ r, with c = 1.6612 − drift(r). How far that reaches depends entirely on how the drift is bounded. A Schur bound on the row sums throws away every sign in the perturbation and gives r* = 0.00695574. Keeping the drift an operator — H(g) ≥ M − 2∑_s dw_s S_s^TS_s with S_s the moving sum of length s, which is translation-invariant with period two and so is the same one-variable Bloch problem with the perturbation’s own symbol subtracted — triples it, to r* = 0.02144507. The reason is that the two symbols peak in different places: the moving-sum Gram symbol is largest at q = 0, where it equals s², and collapses to 0 or 1 near q = π where the crystal’s own gap is smallest. The Schur bound charges s² everywhere.

What the radius does not connect to. It says any perturbation of a pure phase with every gap within 0.0214 grows quadratically at a certified rate. It says nothing about a wall, and the temptation to compare r* against the wall’s 8.877×10⁻³ profile deviation should be resisted: that deviation is measured against the frustrated alternating reference, which carries a low-low adjacency at the seam and is not the crystal. A wall is at sup distance |H−L| = 0.938 from either pure phase on its far side — 44 r* — and no sharpening of constants brings it into the tube. So the two halves stand as: coercivity in an explicit tube around each phase, and the certified tension of the wall that occurs. What a Peierls bound needs, and nothing here supplies, is the middle: a lower bound on the excess for configurations within r* of no single phase.

Unusual stones: reversibility gives an exact cohomological simplification. Any coboundary certificate can be averaged with its reversed copy, so one may assume without loss that Φ is reversal-antisymmetric; the abstract integer statement is now Lean-checked. Numerically, the alternating chain also behaves like a two-phase ground state: its full Bloch Hessian is positive — and that part is now certified at a gap of 1.6 rather than measured, by the Bloch reduction described above; the ≈1.66129 figure was a discrete-grid measurement. More surprisingly, the two interface orientations have sharply different limiting costs, and those are now certified too — see below.

Pricing the adjacency. The diagnosis says a potential seeing only individual gaps cannot price an adjacency. So widen the family: for any state potential Φ on five consecutive gaps, R(g) = F₆(g) + Φ(g₂..g₆) − Φ(g₁..g₅) telescopes, and Φ(s) = ∑_jφ_j(s_j,s_j+1) gives R(g) = F₆(g) + ∑_k=1..5ψ_k(g_k,g_k+1) with ∑_kψ_k = 0. Putting ψ_k(x,y) = u_k(x) + v_k(y) recovers the additive family exactly (checked to 10⁻¹⁶ on 300 blocks), so this is a strict widening, and what it adds is the ability to charge (low, low) differently from (high, high). The ceiling does not move and is structural: F₆ is reversal-invariant and the two alternating blocks are reverses of each other, so the coboundary cancels between them and min R ≤ their average = F₆(alt) = E_alt for every telescoping certificate. Reaching E_alt is the whole game; exceeding it is impossible.

What the search finds. Searching the family from scratch does not converge — 4J² parameters against a cut set that cannot cover six dimensions, so the LP digs holes faster than the adversary finds them. What works is a bounded correction to a certificate already at 0.003957227285, absorbed and repeated: 0.003957387719 at 14 knots, 0.003957389338 at 18, 0.003957391049 at 22 — short of E_alt by 2.26×10⁻⁹, which closes 98.6% of the additive family’s 1.66×10⁻⁷ gap, with the residue still shrinking as knots are added. Two things matter more than the size. The binding block has moved: the additive record binds at a block with a 2.956 gap, the pair candidate at (1.04165, 1.97947, 1.04163, 1.97949, 1.04173, 1.97943) — the alternating block itself, which is how a tight certificate should behave. And the correction is tiny, sup|ψ| = 1.2×10⁻⁵, so it costs the tail cube nothing. What it is not: a floating-point candidate, its floor checked by the Python search’s Adam multistart and by a JavaScript gradient multistart sharing no code with it (which reproduces 0.003957391049344 to the last digit), and by nothing else. No interval sweep has touched it and none can yet — a rigorous sweep of a bilinear ψ needs enclosures for bilinear interpolation over a box, which do not exist here. Evidence that the family is rich enough, not a floor.

What the pair widening was actually for. Separating the two things the pinned certificate did at once — bivariate ψ, and equalities making the alternating block a critical point of R at value exactly E_alt — settles the account. At p = 3000: additive on the record’s 51-knot grid, unpinned, 1.660×10⁻⁷; additive on a grid twice as fine, unpinned, 3.21×10⁻⁸ and still falling; additive twice as fine and pinned, 1.68×10⁻³ — it collapses; pair, pinned, 2.19×10⁻¹⁵. So the widening was not needed to approach the ceiling. It was needed to reach it exactly and stationarily. Pinning is fourteen linear equalities, two values and twelve derivatives; 2J additive parameters cannot satisfy them and keep a floor, and the pair family satisfies them at no cost. And exactness is not a nicety: the tube half of the proof is a Taylor argument from the alternating block and needs R(alt) = E_alt with vanishing gradient. A certificate within 3×10⁻⁸ of the ceiling but not stationary there cannot be completed by a tube, and a branch-and-bound cannot finish it either. The pair family’s role is to make the certificate exact at the point the tube argument starts from.

The kernel’s zeros, in closed form. The pressure scan found the kernel’s zeros by looking for sign changes and its resonant pressures by bisecting a relaxation. Neither is necessary. With a = 1/√2 and b = πx the kernel collapses to K(x) = (a sin a cos b − b cos a sin b)/(a² − b²), so the zeros are exactly the roots of b tan b = a tan a, C := a tan a = 0.6042301210686357610, one per period of tan — and expanding b = kπ + ε gives z_k = k + C/(kπ²) − (C²+C³/3)/(k³π⁴) + O(k⁻⁵), with the residual times k⁵ sitting between 6.47×10⁻⁴ and 6.59×10⁻⁴ over k = 3..11. Those two terms account for the whole of the “mean − k/2” column the scan reported and could not explain: it is C/(2kπ²), 1.53×10⁻² at k = 2 against a measured 1.63×10⁻², and 4.37×10⁻³ at k = 7 against 4.38×10⁻³. For a period-one chain, stationarity is one equation, so exact resonance fixes the pressure outright: p_k = −3 / ∑_s=1..6 s w′(s z_k/2). Certified in Arb by an interval Newton test on the zero equation and an interval evaluation of p_k on its bracket.

And it overturns two things the scan said. The bisection reported “no crossing” at k = 2 and “nothing claimed” at k = 8. Both were guessed-window artifacts: p₂ = 198.613218 lies below the window scanned, which started at 300, and p₈ = 776 447.78 lies above the one that stopped at 520 000. Only k = 10 is a genuine none, and the closed form says why — the derivative sum changes sign, so no positive pressure makes z₁₀/2 stationary. What survives, now analytic rather than measured: at even k the period-one branch is the lower of the two at its own resonance (p₂, p₄, p₆, p₈), and at odd k it is not — period two beats it by 7.3×10⁻², 2.6×10⁻², 1.3×10⁻², 7.9×10⁻³ at k = 3, 5, 7, 9. The parity rule, seen from the side where it can be computed instead of scanned.

Is p actually free? Optimising the pressure only becomes mathematics about zeros if p is a free parameter of the external assembly rather than a constant it fixes. The manuscript is not here, so this cannot be settled — but the question can be made sharper than “not checkable”. In the encoded projection, p enters in exactly one place, spanCoefficient = ((n−1)/p)((blockSize−1)/blockSize), and nowhere else: windowsPerBlock and defectCoefficient depend only on the floor, and the base constant does not depend on p at all. So as encoded, p is a free input and the optimisation is well posed. What that does not settle: the 1/p is the weight the local functional gives to the total span. If it is a tunable weight the assembly carries through, p* is a legitimate choice and the +4.75×10⁻⁶ is real; if it is derived — fixed by a normalisation tied to the zero density, or to the window the manuscript works in — then varying it changes the functional without changing the assembly, and the optimisation compares numbers that no longer describe the same object. Nothing here distinguishes those. That is the question to put to whoever has the manuscript, and it is sharper than “please audit the assembly”: does the 1/3000 in F_n come from a choice or from a derivation?

Coexistence at the crossing: what an interface costs. The two branches having the same energy at p* says nothing on its own about whether they coexist. If an interface between them cost negative energy, a mixed chain would beat both and neither pure phase would be the ground state. A ring following the period-two pattern on one arc and the period-three pattern on the other carries exactly two interfaces, and its excess over Nc is their total. In Arb, with the same Krawczyk-plus-Cholesky machinery the wall tensions use — a unique interface configuration proved to exist in a 10⁻⁶ box in 84 dimensions, refined to a gap radius of 3.8×10⁻⁷⁷, strictly locally minimising with λ_min ≥ 1.167 — τ₂₃ = 1.74773822872121908×10⁻⁵, positive, and saturated: identical from N = 84 to N = 156 to within 5.4×10⁻²⁰. Positive means the phases coexist: mixing them costs, so neither pure phase is beaten by a mixture, and p* is a genuine first-order transition rather than a pressure where two curves happen to intersect. It does not say the two phases are the global minima there — but the nearest competitors have now been asked, and they lose. See below.

Read the next six paragraphs with this in front of them. Every certified statement below comes from a seeded Krawczyk test plus a verified Cholesky, which proves: this configuration exists, it is a strict local minimum, and its energy lies in this enclosure. Comparing two such enclosures settles a question about those two configurations. It settles nothing about the minimum over a period, because nothing here searches a period — the seeds come from a floating-point multi-start scan, and a scan finds what it finds. I learned that the hard way in this very section: a period-eight configuration was certified and its cost published, and a wider scan then found a different period-eight stationary point a hundred times lower. Both are genuine strict local minima. The certificate was correct and the claim resting on it was wrong. A review put the general rule plainly and it is the rule now: a claim that something IS below something else survives — two disjoint enclosures settle it — and a claim that NOTHING is below does not, because it quantifies over a space never searched. So “ground state”, “phase window”, “the mediant loses”, “first-order transition” and “not a devil’s staircase” are conjectures with certified evidence, not results. They were stated as results here and that was wrong. What survives as proved is marked.

The two branches are not always the bottom, and one crossing is not a transition. Everything the pressure section said rested on tracking two branches and reading their crossings as transitions; dev/branch_arb.py certified the branches and stated the gap outright, that nothing had excluded configurations off them. So go and look. Minimising the mean block functional over cyclic configurations of each period separately — period by period, many random starts, floating point — turns up the competitors, and every competitor that matters is then certified in Arb, Krawczyk for existence and uniqueness, verified Cholesky for strict local minimality, enclosed per-gap energy to compare. Three findings, all certified, and two of them corrections.

At p* the two configurations tried do not undercut. Period five is 1.69462×10⁻⁶ above the crossing energy c and period seven 5.51479×10⁻⁶ above, both strictly, by enclosures that do not overlap. Nothing of period ≤ 16 gets below c at all: every period that is a multiple of 2 or 3 reproduces c exactly, because such an orbit is one of the two phases, and every period that is not — 5, 7, 11, 13 — is strictly above, by 1.69×10⁻⁶, 5.51×10⁻⁶, 5.97×10⁻⁷ and 2.74×10⁻⁶. Written as tensions those are 0.24, 1.10, 0.19 and 1.02 times the isolated τ₂₃ — so the cost of a mixture is not two interfaces at a distance but depends on how the blocks are arranged, and it oscillates rather than settling. That is a statement about those two configurations. Nothing of period ≤ 16 was found below c in the scan either, which is evidence and not proof — and it is the weakest kind of evidence, since it is the absence of a find.

PROVED: at the lower crossing the two branches do not exchange minimality. At p = 1454.6785461214313 the two branches do meet — certified, |e₂ − e₃| = 1.4×10⁻¹⁵ — and a certified period-five orbit lies 4.18428×10⁻⁷ below both. Its pattern is one period-three block and one period-two block: exactly a pair of 2|3 interfaces at the shortest separation there is. Written as a tension, τ_eff(5) = −1.0460708×10⁻⁶, negative. That is the same quantity dev/interface_arb.py found positive at p*, and it has changed sign. Two branches cannot exchange minimality at a pressure where a third configuration beats them both, so whatever the lower crossing is, it is not a transition between them. That much is proved and does not depend on any search. What is minimal there is a separate question this does not answer. It had already been relabelled once, from “plateau edge” to “metastability limit”, after a review pointed out the walls do not vanish there; this is the stronger and simpler statement, that the ground state near it has a longer period than either branch being crossed.

What replaces it is a window, and the window is a Farey mediant. Period five is the lowest of the three on an interval of pressures, bracketed here by four certified comparisons: at p = 1452 period three is strictly below period five (8.3×10⁻⁸), at 1453 period five is strictly below period three (1.0×10⁻⁷), at 1455.5 it is still strictly below period two (1.9×10⁻⁷), and at 1457 period two is strictly below it again (2.3×10⁻⁷). What that proves is that the window contains [1453, 1455.5] and is contained in (1452, 1457); the edges themselves, 1452.4447 and 1456.1713, are located numerically and not certified. Either way the old crossing at 1454.6785 sits inside it, which is the point. Below the window period three; above it period two; in between a phase of period 5 = 3 + 2 whose pattern is literally one three-block beside one two-block. That is the Farey-mediant arrangement a devil’s staircase is built from. Two different statements, and they are not equally strong: the comparisons among periods two, three and five are certified in Arb, while ground state — nothing of any other period being lower — rests on the floating-point scan, which at these pressures covers every period up to ten and at p* up to sixteen.

The order parameter is not the period. Scanning further down settles what the phases actually are. Below 1068.3 the winner is a period-four word LLLH; from there to the window it is LLH; the window itself is LLHLH; above it LH; and above p* LHH. Written as the density of H in the word those are 1/4, 1/3, 2/5, 1/2, 2/3, locking in that order as the pressure rises — a rotation number, and the periods were only ever a proxy for it. It also disposes of an accidental collision: the period-five orbit that wins at the lower crossing is LLHLH, density 2/5, and the period-five orbit that loses at p* is LHLHH, density 3/5. Same period, different phases, and each is the Farey mediant of its own two neighbours — 2/5 of 1/3 and 1/2, 3/5 of 1/2 and 2/3.

Five mediant configurations built, four cost. This is the sharpest form of the staircase question reachable by seed certification, which is not the same as answering it: each row certifies one configuration of that density, not the best one. Between 1/4 and 1/3, at p = 1068.324562 where those two are degenerate, the mediant 2/7 = LLLHLLH is 9.89517×10⁻⁶ above both: loses. Between 1/3 and 1/2, 2/5: locks, on [1452.44, 1456.17]. Between 1/2 and 2/3, at p*, 3/5 is 1.69462×10⁻⁶ above: loses. At the two edges of the window that 2/5 opened, 3/8 and 3/7: lose, by 5.73192×10⁻⁷ and 6.72987×10⁻⁶. If those configurations are the minimising ones, the Farey construction is realised once and does not iterate. That conditional is the honest form: a devil’s staircase would have every mediant locking on some interval, and here one in five of the ones tried does — suggestive, unproved.

The two second-level mediants, in detail. If the construction repeated, 8 = 3 + 5 (density 3/8) would open a window at the lower edge of the 2/5 window and 7 = 5 + 2 (density 3/7) at the upper one. Both were built and certified, and both are strictly above the two phases they would interpolate — by 5.73192×10⁻⁷ at the 3|5 edge and 6.72987×10⁻⁶ at the 5|2 edge, which is the same statement as τ_eff(8) = 2.29×10⁻⁶ and τ_eff(7) = 2.36×10⁻⁵, both positive. So the mediant configurations that were built cost more than the phases they interpolate. Whether a different configuration of the same density would win is exactly what is not checked, so “the edges are first order” does not follow. That the mediant loses is the sharp form of the question, since a mediant window would have to contain the degeneracy point and be below both phases exactly there; and the scan adds that at either edge no period up to ten is below the two that meet, mediant or not. A finite sequence of commensurate phases, checked at the one level where a staircase would have had to show itself. Twenty-nine checks, all in Arb, in dev/staircase_arb.py. The 5.73×10⁻⁷ read 5.80×10⁻⁵ for one commit, because the period-eight seed was the two certified blocks written end to end and that relaxes into the wrong stationary point — a real one, a hundred times too high. Concatenation is a plausible seed and not a minimiser. The margin moved by two orders of magnitude and the conclusion did not, which is the only reason the conclusion survived it.

A smaller thing that fell out: “the period-three branch” is two branches. At p* the period-three block is LHH and at the lower crossing it is LLH — different words, different densities, and at each pressure the other one exists and sits about 3.9×10⁻⁴ higher. They exchange which is lower at p ≈ 2033.43. That exchange is harmless, because 2033 is well inside the stretch where the period-two phase is the ground state, so it is a level crossing between two excited states and not a transition; and lowerCrossover in tiling_pressure.js already relaxes from both seeds and takes the lower, so the crossing pressure it reports is about the right orbit. But the phrase “the period-three branch” on this page covers two objects, and the certified statements are about whichever one is named by its seed: dev/branch_arb.py certifies LHH over [3300, 3450], and the lower-crossing comparisons here are about LLH.

Why, exactly: it is a single two-block that goes cheap. Write a mixed configuration as a two-blocks beside b three-blocks — period n = 2a + 3b, two interfaces — and tabulate τ_eff = n(mean − c)/2 over the whole table rather than over periods. At p* it reads, in units of the isolated τ₂₃: 0.242, 0.196, 0.188, 0.188 along a = 1, then 1.10, 1.02, 1.02, 1.02 at a = 2, and 1.002, 0.998, 1.000 at a = 3, 4, 5. So the interface pair is essentially decoupled from a = 2 onward, converged in b by b = 2, and the one exceptional cell is a lone two-block inside the period-three phase, which costs a fifth of what two free interfaces cost. That is the whole of the oscillation the periods showed: 5 and 11 were small because they have a = 1, 7 and 13 were near one because they have a = 2. The period is a red herring; the composition is the variable.

And at the lower crossing that one cell goes negative. The same table at p = 1454.6785 — with the local blocks, because the three-block there is LLH and at p* it is LHH, a different word with a different density — reads −0.060 at (a, b) = (1, 1) and positive everywhere else, 0.057 to 0.071 along the rest of a = 1 and 1.19 to 1.36 for a ≥ 2. So the failure of coexistence there is not a general instability: it is exactly one defect, one two-block beside one three-block, and nothing longer. The two immediate neighbours are certified in Arb and both cost — τ_eff(7) = 2.25×10⁻⁵ at (2, 1) and τ_eff(8) = 1.25×10⁻⁶ at (1, 2) — against τ_eff(5) = −1.05×10⁻⁶ at (1, 1). Which is also why the ground state there is period five and not something longer: it is the only mixture that pays.

Dilute defects, and two real metastability limits. The a = 1 column with b large is the isolated defect: one two-block inside a long stretch of period three. Its cost crosses zero at p = 1456.8653 and again at p = 3333.2949 — negative in between, positive outside — so those, and not the wall zeros at 1425.71 and 3521.82, are where the period-three phase actually stops resisting a single two-block. “Isolated” is a limit, so it is taken: the two zeros read 1456.867246 / 3333.279750 with five three-blocks between defects, and settle at 1456.865312 / 3333.294860 from nine onward, unchanged at eleven and thirteen. The mirror defect, one three-block inside period two, costs +1.086 τ₂₃ at p* and turns negative somewhere between p* and 3800. At p* both are positive — certified, τ_eff = 3.28×10⁻⁶ and 1.90×10⁻⁵ — so each phase resists these two defect configurations. A metastability overlap would need every defect profile, and two is not every.

And that is precisely what the lower crossing does not have. At 1454.68 the isolated defect still costs, on both sides: +0.057 τ for a two-block in period three, +1.10 τ for a three-block in period two. Both pure phases are locally stable, and period five beats them anyway. So the two crossings fail differently: at p* the mixture costs at every spacing and the phases coexist; at the lower crossing the isolated defect costs but a dense array of them does not, because the defect–defect interaction turns attractive at the shortest spacing. The intermediate phase arrives by defect attraction, not by single-defect softening — which is also why it arrives as a first-order jump to period five rather than a continuous unbinding.

And below the crossings the period is longer still. At p = 1000 the period-two branch has collapsed to a uniform state — L and H agree to 10⁻⁸² — and a certified genuinely period-four orbit sits 1.2684×10⁻⁴ below it and 3.15654×10⁻⁵ below the period-three branch. Proved: neither tracked branch is minimal there — period four beats both by a certified margin, which needs no search. That nothing else beats period four is the scan talking, up to period nine, and is not proved. Sweeping the scan’s winner across pressure — floating point throughout, no certification — the period that wins is 1 at p = 500, 4 at 1000, 5 at 1454.68, 2 from 2000 to p*, 3 from p* to 4500, and 1 again by 6000 — which is what a devil’s-staircase model looks like from ten sample points — and the paragraph above says why it is not one. What is claimed is the certified part.

What the short orbits say about the calibrated coboundary. They also settle, in the one direction that can be settled cheaply, the question the LP could not. A telescoping certificate with floor c exists only if c is a lower bound for the mean of F_p over every shift-invariant measure, because the coboundary averages to zero against any such measure. Periodic orbits are shift-invariant measures, so a single periodic configuration with mean below c refutes the calibration outright, and no amount of LP tuning could have rescued it. That turns an existence search, which one cannot finish, into a falsification search, which one can. Over every period up to sixteen at p*, nothing gets below c — and this is a search, so it can only ever fail to find one. The calibration is not refuted by short orbits; whatever is stopping the LP, it is not an obstruction of that kind.

The calibrated coboundary: formulated, not settled. The certificate that would establish coexistence against every configuration is a single potential with F_p + Φσ − Φ ≥ c and equality on both cycles. The crossing is pinned: p* = 3370.450721224646523297, period two at (1.0416923434460380797, 1.9795173654714754534), period three at (1.0435744986456292657, 1.9922863695808364586, 1.9922863695808364586), common energy c = 0.00362533155996670429057064. The calibration turns out to be three conditions, not five — the telescoping identity already forces each cycle’s blocks to average to c — and the gradients need no constraint at all, since a block where R = c and min R = c is a minimum. The straight segments joining the five blocks do not obstruct: the calibrated LP bound there is 0.003807958788, above c, and identical across families from 840 to 2128 coefficients. A calibrated certificate exists on any given cut set and gets within 5.5×10⁻⁵ of c. And then it stops: as cuts accumulate the minimum-norm coefficient size grows without bound (1.6×10⁻⁶ → 2.5×10⁻³ over fifteen rounds) while the adversary floor gets worse — the signature of an infeasible system rather than a converging one. Not a proof: that would be the LP returning infeasible on a finite cut set, and it never did, because the solver aborts at around six thousand cuts. Formulated correctly, the obvious obstruction ruled out, no short periodic orbit refuting it, and still undecided — the evidence that was “leaning against” is the LP’s behaviour and nothing else, and the dual test that could have killed the calibration outright has now been run and did not.

The odd-period resonance, decided rather than sampled. For period one the resonance question is a formula. For period two it is not — two stationarity equations and one pressure — and the way through is to subtract them, which kills α and hence p. With L + H = z imposed, the lag-s distance at odd s = 2m+1 is mz + L for one parity and (m+1)z − L for the other, with coefficient difference +1 and −1, so everything collapses to G_k(L) = ∑_m=0..2[w′(mz_k+L) − w′((m+1)z_k−L)], odd under L → z_k−L, with a trivial root at the symmetric point. A resonant period-two configuration exists exactly when G_k has a root off that point, and interval Newton settles it. It has one: at k = 3, certified, L = 1.041502757331298264032 (radius 5×10⁻⁹⁰), H = 1.978740234840183, L + H = z₃ exactly, pressure p = 1155.3172071956. At k = 5 there are three. This overturns a third scan result — the page used to say the period-two branch keeps its sign across the plateau and the odd-k resonance never happens. Same guessed-window mistake: 1155.32 sits below the lower branch crossing at 1454.678546, so a scan over [1455, 3370] could only ever see one sign. What is not claimed: that this configuration is the ground state at its own pressure. It is not — the period-three branch is lower there, and, as the orbit scan below shows, at those pressures neither branch is the ground state either. Three separate statements, and only the first two are proved.

The branches, certified over pressure intervals. The pressure work elsewhere in this directory is exploratory numerics — gradient descent from structured seeds, reporting the lowest branch found — and a crossing of two numerically selected branches is not a certified transition. dev/branch_arb.py does in Arb what the relaxation could not: for a whole interval of pressures at once, a Krawczyk test on the stationarity system proves a branch exists and is unique in an explicit box, and a verified Cholesky on the interval Hessian proves it is a strict local minimum there. A unique period-two branch, strictly locally minimising, for every p in [2900, 3100], [3300, 3450] and [1400, 1600]; a unique period-three branch likewise for every p in [3300, 3450]; and E₂ − E₃ certainly negative at p = 3360 (−9.1605518×10⁻⁷) and certainly positive at p = 3380 (+8.3208743×10⁻⁷), so the two certified branches cross between them. That is not the statement that the ground state changes period there: nothing in it excludes configurations off these two branches, and doing that needs a transfer-operator or coboundary bound that is not built.

A correction, from the pressure scan. This page has said the additive family stops 1.66×10⁻⁷ short at p = 3000, and the pair-state work below was motivated by that. 1.66×10⁻⁷ is the best certificate that was found, on a 51-knot grid with spacing 0.1. On a grid twice as fine — a strictly richer family — a modest search reaches 7.1×10⁻⁸, and the LP’s own bound is not forced below the ceiling anywhere in the interior of the plateau. So “the additive family cannot reach the ceiling at p = 3000” is not established; what is established is that the record certificate’s grid did not. Near the plateau edge it is established: at p = 1500 the LP bound itself sits 1.489×10⁻⁶ below the ceiling. Nothing about the pair-state results changes — the pinned certificate reaches the ceiling and is the one the rigorous sweep closed on — but the account of why it was needed does. Read the next two paragraphs with that in mind.

Where the certificate family’s 1.66×10⁻⁷ actually goes. The best certificate has LP floor 0.003957227285, below the alternating chain energy. For the projection that shortfall is irrelevant; for a crystallization argument it is everything, since a uniform block floor below E_alt cannot prove the alternating chain is the minimiser. Start from an identity: the additive coboundary telescopes over the alternating chain, so R at an exactly alternating block is the chain energy, 0.003957393309109, for every certificate here to 10⁻¹⁵. It is not minimised there. Sweeping the cube minus the two alternating tubes shows the shortfall is not one obstruction but three, within a factor of two of each other — a perturbed near-alternating block (−4.12×10⁻⁷ for sharp, −1.63×10⁻⁷ for record), a high-high defect block (−4.01×10⁻⁷, −8.09×10⁻⁸), and for record a long-gap block at 2.956 (−1.66×10⁻⁷, its own argmin). The low-low defect is the one basin comfortably above, at +2.4×10⁻⁴.

The high-high defect is the interesting one. The chain charges that wall a certified tension of 1.47×10⁻⁴; the block relaxation charges it essentially nothing, coming out below the ground state by about the same margin as the near-alternating basin. The low-low wall, tension 1.09×10⁻³, does show up — the relaxation charges 2.4×10⁻⁴, roughly a fifth. So the relaxation sees a fifth of one wall and none of the other, and lifting the floor to E_alt means lifting all three basins at once while a gaps-only certificate has to lift the high-high defect without noticing it is a defect. A coboundary carrying the block’s symbol pattern — a pair state, any finite memory — could charge the two adjacencies differently, which a purely additive one cannot. That is a concrete reason to want the generalised coboundary state rather than a general preference for more parameters. Numerically the restricted sweep is worth almost nothing: it raises the certifiable floor by 1.1×10⁻⁸. It is a diagnostic instrument, not a record.

Pinning the alternating block. The knot ladder was chipping at the residue with the wrong tool. A certificate attaining the ceiling must have the alternating block as a critical point of R at value exactly E_alt — otherwise R dips just off it, and that dip was the entire residue. Those are linear conditions on ψ: two values and twelve derivatives, put into the LP as equalities. Two false starts, both instructive: solving them first, for the smallest correction that satisfies them, picks a spiky one that pinned the gradient to 7×10⁻¹⁶ and dug a 2.8×10⁻⁵ hole no later round could climb out of; and pinning only the gradient pins a critical point of the wrong value, since the coboundary may shift R(alt, phase 0) down and R(alt, phase 1) up by the same amount — their sum is fixed, each is not — and it promptly did, dropping phase 0 by 10⁻⁵. Both rows are needed, inside the floor-maximising LP rather than before it.

With both, at 22 knots and a correction capped at 2×10⁻⁵: R equals E_alt at both alternating phases to 2.2×10⁻¹⁵, its gradient there is 6.3×10⁻¹⁷, the smallest Hessian eigenvalue there is 0.245, and the adversary floor is 0.003957393309107 — below E_alt by 2.19×10⁻¹⁵, which on a quantity of size 4×10⁻³ is a few hundred ulps: double-precision zero. Three adversaries sharing no code agree — the Python search’s Adam multistart, a JavaScript gradient multistart, and a structured pass over all 64 two-symbol patterns and 1536 long-gap variants — and all of them descend to the alternating block. What that would mean, and the word is would: if an interval sweep confirms R(g) ≥ E_alt for every six-gap block, then averaging over the shifted blocks of any chain gives per-gap energy ≥ E_alt, so the alternating chain is the global minimiser — the crystallization statement, worth 0.6731102697 on the headline projection, the whole of the available improvement.

Where this stands, now. This section used to be six paragraphs written at six different moments, four of them stating in the present tense things the later ones contradicted — one said no sweep existed while another, further down, reported it complete. A reader could not tell what the current claim was. It is collapsed here into one statement of the position; the chronology is in the git log, where it belongs.

The certificate. A pair-state coboundary with the alternating block pinned as a critical point of R at value exactly E_alt: R equals E_alt at both alternating phases to 2.2×10⁻¹⁵, its gradient there is 6.3×10⁻¹⁷, the smallest Hessian eigenvalue there is 0.245, and no adversary has found anything below it. It came out of a floating-point LP, and that does not matter for soundness: any ψ whatever gives a valid telescoping certificate, so the search’s quality affects only which floor comes out, and the floor is what the sweep measures rather than assumes.

The three regions, and what covers each. On the two alternating tubes |g_i − c_i| ≤ 0.008: a Taylor argument from the pinned point, with a covering-and-Cholesky bound on the Hessian, gives R ≥ E_alt − 2.186×10⁻¹⁵. This half is now in Arb (dev/tube_arb.py), with nothing from tiling_rigorous.js anywhere in the file — and it is both independent and sharper: λ ≥ 0.139341, 0.114745, 0.104984 at radii 0.003, 0.005, 0.008 against the JavaScript’s 0.1118, 0.0774, 0.0637 (and, since 2026-09-07, λ ≥ 0.107108 for the other alternating phase HIGH, LOW, … at the same radius — the sweep excludes both phases and the pair certificate is not reversal-symmetric, so the second phase needed its own certificate and had none; the radius is certified at 0.00800000000000001 because the sweep excludes a float box whose cuts stick 6.9×10⁻¹⁸ out of the exact tube), and a shortfall five thousand times smaller, because the JavaScript figure was set by its evaluator’s slack at a pinhole box while Arb encloses the point directly. A branch-and-bound cannot do this region — it would chase a bound that is exactly attained — and the argument is valid only because the alternating gaps clear their nearest knot by 0.0205 in both grids, which the code checks rather than assumes. Outside the tubes, inside [0,28]⁶: exhaustive subdivision, complete, no counterexample. Outside the cube: the tail lemma, which clears E_alt once ∑g reaches 27.942537 — and 27.94 < 28, so the two meet with nothing between them. Together: R(g) ≥ E_alt − 2.186×10⁻¹⁵ for every six-gap block, hence by the telescoping lemma every chain has per-gap energy at least that. E_alt is the alternating chain’s own energy, so the alternating chain is the minimiser to within 2.2×10⁻¹⁵.

The arithmetic, after a review found holes in it. Three places in the enclosure path used ordinary rounded arithmetic where an enclosure was claimed: the Hessian cross terms were computed as plain doubles and inserted as degenerate intervals; a centered form returned at − spread in plain arithmetic and that value was used as a lower bound; and the accumulations in the box bound and the centre enclosure were plain additions covered only by a constant chosen by eye. All three are repaired — every step directed outward, the centered form replaced by four outward-rounded corner evaluations (which is both sound and tighter, since a bilinear function on a sub-rectangle is a convex combination of its own four corners), and the Cholesky pivot margin now computed from the matrix in hand rather than asserted. The tube result is unchanged by the repair (λ ≥ 0.0637 at radius 0.008), and has since been superseded by the Arb version above, which is both independent of that arithmetic and sharper. Both sweeps have reclosed on the repaired arithmetic, and with FEWER boxes than before it: 50 184 539 against 50 203 847 in double precision, and 75 004 893 against 75 037 955 with proved enclosures — complete, no counterexample, nothing unresolved, checksums a8bea1b0b603c5eb and e6bbfa8b87622e6e. Fewer, because the corner enclosure that replaced the unsound centered form is tighter than what it replaced as well as sound. The repair cost nothing and the statement did not move.

A proof-carrying sweep. Rerunning the sweep in a different arithmetic is not affordable — an Arb box costs about half a millisecond, ten hours for seventy-five million. A proof object is, because it separates the search from the justification: the search decided which boxes to look at and in what order, and nobody needs to redo that; what has to hold is local to each node. dev/sweep_proof.js emits the subdivision tree as one byte per node in preorder, and dev/sweep_proof_arb.py replays it against an independently recomputed root partition. On the truncated cube: 53 102 447 nodes, 18 940 108 leaves, 18 924 485 splits, 15 237 854 collapses, nothing unresolved, a 53 MB tape emitted in 344 s and checked in 17 s. Structure is verified for every one of those nodes at no arithmetic cost — tape consumed exactly, counts agreeing, every split’s midpoint inside its parent, every collapse landing on a face, no leaf left open. That is the check that catches a lost region, a sweep reporting “complete” having silently dropped part of its domain. Arithmetic is verified on a sample, and the checker says how far it got: of 220 sampled leaves Arb now confirms 220, and of 220 sampled collapses 220; nothing is refuted. Those numbers started at 3 and 35, went to 39 and 67, and reached 220 when the checker enclosed the pair distance as the sum of the gap intervals rather than a difference of prefix sums. It is still a spot-check of the committed small tape and not an independent arithmetic proof of the sweep; the same checker’s all-nodes mode is what the investigation runs on the full tapes. An external review then showed the checker itself unsound in four places — hulls taken through nearest-rounded floats, the acceptance comparison in floats, kernel tables that stopped at distance 30 while the tapes reach 96 and 168, and a tube leaf accepted on its word — and each was repaired and given a negative control (dev/sweep_proof_arb_controls.py: a forged tube leaf, a deleted subtree, flipped collapses, an altered coefficient, an unresolved obligation, each refused). The sweep’s advantage was exact monotone-piece ranges from precomputed breakpoints, so dev/kernel_pieces_arb.py builds the breakpoints in Arb — they come straight out of the closed form, w vanishing at the roots of b tan b = a tan a and having exactly one maximum between consecutive roots at a root of K′, so between them it is monotone and its range over any interval is the hull of the endpoints and the enclosed breakpoints, exact rather than enclosing. Thirty-one zeros, thirty maxima and fifty-nine w′ breakpoints up to x = 30 (the tables now extend to six times the tape’s cube), each certified by an interval Newton test — and, since the review, proved complete: the gaps between consecutive certified roots are shown zero-free by interval bisection, so no critical point is missing from the hull. Built in a second, worth up to 118× on the interval extension they replace; a centred form for the whole bound does the rest. Neither closes the gap entirely, and the checker still reports the fraction it reached: matching a 10⁻¹⁰ margin means reproducing the sweep’s whole enclosure strategy, which this is a step towards and not a substitute for. The suite carries a small configuration, 27 940 nodes, regenerated and compared byte for byte every run.

What it rests on. The tube half no longer rests on tiling_rigorous.js. The outside-the-tube sweep still does, and that is now the whole of the outstanding item: seventy-five million boxes of w and w″ enclosures from hand-written transcendentals with error constants I chose. Rebuilding that in Arb is a far larger job than the tube was — a few thousand box evaluations against 7.5×10⁷ — and until it is done the global statement is certified modulo my arithmetic. And everything downstream depends on the external shifted-block assembly nobody here can check: a block floor of E_alt projects to 0.6731102697 by this directory’s own table, conditional exactly as every other number here is. Even repaired and rebuilt, this would be a theorem about the auxiliary chain — not about primes, and not about zeta zeros.

The wall, certified. Coercivity supplies the c·dist² half of a crystallization argument; the other half is the cost of an interface, and a Peierls bound needs it to be definitely positive. An odd ring is frustrated — it cannot be alternating anywhere — so it carries exactly one wall, and the seed phase decides whether the core is a low-low or a high-high adjacency. On a 63-gap ring, in Arb: a Krawczyk test in 63 dimensions proves a unique critical point in a 10⁻⁶ box, iterating pins every gap to a radius near 3×10⁻⁸⁹, and a verified Cholesky in ball arithmetic (written out, not delegated to an eigenvalue routine whose rigour contract would then have to be taken on faith) proves the Hessian positive definite there. The tensions come out enclosed and positive: τ_LL = 0.001092786457724342735 ± 2.0×10⁻²⁵ and τ_HH = 0.000147085497481443264 ± 1.1×10⁻²⁶, summing to the independently relaxed two-interface ring excess. The low-low core sits above the bulk Bloch gap 1.66128 (λ_min ≥ 1.6613857650) and the high-high core below it (≥ 1.2272529833): only one of the two orientations softens the spectrum.

And the wall is frozen at finite size. On an odd ring a wall interacts only with itself, around the ring, and that self-interaction dies at about e^−0.78 per gap — the profile deviates from the crystal by 8.9×10⁻³ at the core and 7×10⁻³⁰ eighty gaps away. So τ₆₃ − τ₄₇ = 1.14×10⁻¹⁹ and τ₉₅ − τ₆₃ < 10⁻²⁵: the ring value is the infinite-chain value to twenty-odd digits. What this is not: the tension of this wall, certified to be a unique strict local minimum — an unconditional upper bound on the true wall tension, and a lower bound only conditional on the core being this one. Certifying the infimum over all 63-gap rings is a global optimisation nobody has done. A Peierls bound needs exactly that. The missing constant is now pinned to twenty digits and proved positive for the wall that occurs: more than numerical evidence, less than the theorem.

Why the search box is finite. Every pair term of F₆ is nonnegative, so R(g) ≥ (Σg)/3000 − A with A = 2(‖a‖_∞+‖b‖_∞+‖a+b‖_∞). Any gap reaching 3000(floor+A) satisfies the inequality outright, so the certificate only has to be checked on that cube — and adding a constant to a or to b leaves R unchanged, so gauge-centering both is free and shrinks the cube about fiftyfold. The audits above search the entire remaining cube, not a convenient part of it. The same A bounds the finite-chain boundary term uniformly in the chain length, which is exactly the o(m) condition the projection needs.

Next proof obligation. In order of value per unit work: (1) compute — both rungs are at 0.003956 and the certificate is what binds now — sharp stops at 0.003956981, record at 0.003957227, ceiling 0.003957393 — so the last 4×10⁻⁷ is cut-generation rounds, not sweeping and should land within a part in 10⁶ of the ceiling; (2) an independent implementation — every claim above trusts that this code has no bugs, and the cross-checks, real as they are, are checks by the same author; the surface to reimplement in Arb or MPFI is small (sinPoint/cosPoint, where the only hand-written error bound is asserted; sinRange/cosRange; sincRange, sincDerivRange, sincSecondRange; and weightPairCentered — everything else is exact rational bookkeeping); (3) a checker with no optimizer in its trusted base, reading rationalised knots and coefficients as data; (4) the assembly, which nobody here can check. One design note, because it inverts the old plan: that plan called for verified breakpoint tables and warned that a missed breakpoint silently narrows a range — the one failure mode that invalidates everything, while every other approximation only widens. The rigorous sweep avoids the hazard entirely by using natural interval extension plus centered forms, which need no structural facts about where the kernel’s zeros and extrema are. The price is the 1.8× box overhead. That is a good trade, and it should not be undone in pursuit of speed. Reproduce with dev/sweep.js; certificates in dev/tiling_additive.certificate.json, results in dev/tiling_interval.results.json, handoff in dev/TILING_DUAL_RESEARCH.md.

OPEN PROBLEMSFive concrete directions, ranked by feasibility.

1. Audit the unconditional four-point Lean claim (≈0.6728470197… from teal-sea). Verify pinned dependencies, final statement, absence of certificate hypotheses, axiom set, and correspondence with official zeta-counting definitions. This is now the highest-value audit task.
2. Try a charged two-phase contour proof. Certify local coercivity around the alternating phases, classify every low-energy block, and price low-low and high-high kinks separately. The exact cyclic charge identity #low−#high = #LL−#HH is now Lean-checked at the integer-bookkeeping level. The analytic task is to certify positive defect costs and control their short-range interaction.
3. Map the dimension–moment tradeoff: set X = T^θ, require kθ ≤ 2−ε, and construct the numerical phase diagram in (θ,k). Higher trace moments become available when Dirichlet-polynomial length is shortened; if no (θ,k) point beats 0.6728470197, kill the route cheaply.
4. Formulate the weakest useful support->1 prime estimate. Extend test support to 1+δ; write the exact weighted off-diagonal prime-pair sum; determine the one-sided bound sufficient for the moment upper bound. A weighted upper bound with correct sign may be weaker than full Hardy–Littlewood yet sufficient.
5. Make the ζ′(ρ)-mollifier route unconditional. Highest upside but largest gap: requires a quartet-symmetric zero identity valid off RH and a precise Feng-type vector-mollifier prime-pair estimate.

Sources & certificates

• L. Alpöge, R. Furman, More than two thirds of the zeros of the Riemann zeta function are simple and on the critical line, arXiv:2608.13637 (2026) — argument discovered autonomously by Claude (Anthropic); Lean 4 formalization at anthropics/zeta-23-lean.
• Candidate claim under review: More than 67.3% of the zeros are simple and on the critical line (unsigned manuscript + Arb interval-arithmetic verifier; treats 67.30085% as unconfirmed).
• Candidate ecosystem (audit ledger zeta.teal-sea.com, dated 2026-08-25): roughly fifteen runnable stability-defect candidates above the official constant, leaderboard max ≈67.34165% — fresh-clone verifier run inconclusive (not a soundness finding); a reproduced nine-point/window-replacement candidate at ≈67.33127% is pending mathematical review; two smaller “Lean-internal” claims at 67.27373%/67.28470%. None independently reviewed; audit self-published.
• Formalization status of this repository: dev/lean/ZetaClaims.lean compiles under Lean 4.33.1 (toolchain pinned) with no sorry and no user-declared axioms — it covers the integer bookkeeping skeleton, reversal-coboundary symmetrization, binary phase-defect balance, the telescoping lemma that turns a per-edge coboundary floor into a chain floor with an O(1) boundary term, the two-sided decimal pin of the external headline constant, and the lab’s no-dip snapshot — eleven theorems, each audited to depend only on propext and Quot.sound. The connected proportion theorem is deliberately absent: a first derivation left an unresolved scale inconsistency and was withdrawn (see §9).
• Analytic inputs: Baluyot–Goldston–Suriajaya–Turnage-Butterbaugh (2024, unconditional form factor); Aryan (2022); Montgomery (1973, 1975); Bombieri (2000); Goldston–Suriajaya (2025–26); Pratt–Robles–Zaharescu–Zeindler (2020, previous 5/12 record); Wu (2015, distinct-zeros record 0.6603).
• VibeMathed entry: proportion record · VibeMathed entry: S⁶ complex structure.