teal-sea / zeta-labstate of record · compiled
14 Aug 2026 · revision
dec3e80 ·
source
Record
Everything that happened, including what went wrong. A record
that lists only successes is advertising.
01. We shut down our own flagship
We built a framework for testing whether an empirical claim is about its
subject at all: structure-matched controls, ablations, null models, planted
faults. Roughly eight thousand lines. Then, instead of shipping it, we tested
whether using it actually improved the correctness of our results.
Four preregistered experiments, three subjects, 74 agent runs. Every protocol
was committed before its arms ran, so the ordering is checkable in the git log.
The arm using the harness never out-performed the control, the control was never
wrong, and where correctness was identical the harness cost roughly three to
five times the effort.
Preregistered experiments and their verdicts
| experiment | result | evidence |
| Gate v1 | FAIL | harness/gate-evidence/HARNESS-GATE-2026-08-13.md |
| Gate v2 | FAIL | harness/gate-evidence/HARNESS-GATE-V2-2026-08-13.md |
| Gate v3 | RECORDED | harness/gate-evidence/HARNESS-GATE-V3-2026-08-13.md |
| Gate v4 | FAIL | harness/gate-evidence/HARNESS-GATE-V4-2026-08-13.md |
Development stopped that day. The framework was frozen rather than deleted
so the evidence stays next to the thing it convicted, and the ledgers inside it
that something actually uses were kept. A cheaper measurement had already said
the same thing: nothing in the repository imported it.
Being able to kill something you funded, on evidence, is
the habit worth keeping. A laboratory that cannot do that has preferences rather
than a method.
02. Claims, and who was sent to break them
Every claim goes on the record with the reasoning that produced it and the
assumptions it rested on, before anyone knows whether it survives. Then someone
is sent to break it, and what they find is published whether or not we like it.
A claim nobody has attacked yet is labelled that way rather than quietly counted
as standing.
withdrawn
blockpos-0.672529
the constructive block-positivity residue transplants to the pinned upstream zero side, giving 0.672529 unconditionally
claimed by frontier_math blockpos session (2026-08). positivity of each block was checked numerically; the construction was believed basis-independent
rested on: the upstream zero side uses u u* (it uses u u^T)
rested on: off-line pair blocks interact non-negatively with on-line part
frontier_math clean-kill session (2026-08-11) (white-box) found: the pinned upstream zero side uses u u^T, not u u*: an off-line pair is the hyperbolic block 2m(xx^T − yy^T), whose interaction with the on-line part can be negative; exact witness u_x=1, u_z=i, u_conj(z)=-i gives tr(P1 Q') = -2; with five unit on-line labels the final inequality reads 9 >= 13
unattacked
urms2-0.51
the URMS2 bandwidth extends past the half band to 0.51, with the algebraic frontier formalized (main, 503158a and ancestors)
claimed by urms2 bridge sessions (2026-08-11). several apparent bandwidth barriers were artifacts of lossy estimates; this one fell to preserving frequency separation
rested on: the true logarithmic frequency separation is preserved rather than collapsed into a cutoff estimate
no adversarial pass recorded. This claim is open, not confirmed
03. Corrections
Defects that actually occurred, each with the test that now catches it. A
guard nobody has watched fire is a claim rather than a control, so the ledger
tracks which is which instead of flattering itself.
Guards, and the incidents behind them
| incident | what it would have let through |
fires |
|---|
| docs/25-the-director-run.md (2026-08-11), defect #1 | zeta.rigor._exact taking an unrecognised numeric type's printed decimal as its exact value, silently moving the abscissa and producing a wrong proven_sign on both backends at once | yes |
| two documents shared number 21 on 2026-08-10 | two documents sharing a leading number, making every bare docs/NN reference ambiguous | yes |
| written before any incident | a probe file under hunts/ using the reserved word and so claiming a certainty regime only zeta/rigor.py and lean/ carry | yes |
| written before any incident | a docs/doors/ entry page whose quoted command no longer runs — a front door that opens onto a wall | not shown |
| written before any incident | CONTEXT.md drifting stale after a public function, doc or script is added or renamed | yes |
| twice on 2026-08-12: all eight BandCert/ modules, then the five EForm/ modules landed after that fix — a repair that recurred, which is what turned… | a Lean artifact landed into hunts/frontier_math/zeta23ext with the proving service's own module prefix (RequestProject) left in its import lines, so the package fails to assemble at the… | yes |
| twice on 2026-08-12: 'import Zeta23Ext.Bridge' was replaced by another import in the root module by a one-line edit, twice, leaving a kernel-checked… | a module that exists in the package but is reachable from no import chain out of Zeta23Ext.lean, so `lake build` never touches it: it rots silently while the package still reports success… | yes |
04. Withdrawn results
11 Aug 2026 · withdrawn
blockpos 0.672529 (and siblings 0.6725124, 0.6725318)
the construction used u u* where the pinned upstream zero side uses u u^T; an off-line pair is the hyperbolic block 2m(xx^T - yy^T), whose interaction with the on-line part can be negative, and the proposed final additive inequality reads 9 >= 13
14 Aug 2026 · withdrawn
conditional 0.6728294 (the bin artifact)
midpoint bin-to-cell assignment inflated chain counts, briefly producing a conditional bound past CG 1993
11 Aug 2026 · closed
naive prime-by-prime (placewise) positivity
individual place contributions can sometimes be represented as norms, but the local pieces do not consistently carry the sign naive global assembly needs
05. Scope
This laboratory works on the structure around the Riemann hypothesis, and
what it establishes are results about that structure. Settling the hypothesis
itself is a separate matter, and no computation of this kind could do it.
When a result looks like it settles something, our first assumption is that
we have a bug. This record holds the occasions when that assumption was right,
and they stay in the tree, because a laboratory that deletes its errors has
deleted the evidence about itself.