ACTIVE-CLAIMS — live coordination between concurrent sessions
Read this before launching an agent, a prover submission, or a build in hunts/frontier_math/. HANDOFF.md is the serial channel (session to session, across time).
Everything the repository publishes, not only the parts that
worked. 181 documents, 45,788 lines, listed straight off
git ls-files so nothing can be quietly left off.
| 181 | documents |
| 45,788 | lines |
| 7 | shelves |
Most of this is working record rather than finished writing: routes opened and abandoned, tables sized wrong and resized, corrections to our own corrections. It is here because a laboratory that publishes only its results has published the smallest and least checkable part of what it did. Titles and descriptions are the files' own first heading and opening paragraph, so this index cannot describe a document as something other than what it says it is.
The transplant into the source paper's chain: the working paper, the obligation ledger, every route opened and every one closed. The largest single body of working record in the tree, and the least finished.
Read this before launching an agent, a prover submission, or a build in hunts/frontier_math/. HANDOFF.md is the serial channel (session to session, across time).
Sprint 1 draft, 2026-08-12. Lane 1 step 2 of PIPELINE.md. This is the specification a later session turns into an Aristotle submission for Zeta23Ext/Bridge.lean.
The 0.672529 candidate is withdrawn. Its first required algebraic lemma is false. The failure occurs before taper, truncation, census, bootstrap, or LP questions can affect the result.
Verdict: the discrepancy resolves, your measurements reproduce exactly, and the transfer does not survive — for a reason that is not in your data, because it is outside your scan window.
An audit run from a fresh clone by a session that did not build any of the instruments below, against the source paper's own text.
Record of a measurement-and-proof exchange with the theorem-proving service during submission 9 , 2026-08-13.
No positive portion of the ordered-gap floor follows from the paper's existing unconditional zero-side inputs. The obstruction is quantitative, not merely a missing sign argument.
Date: 2026-08-13. Reads: gram_form.py (the three-term form), kpair_identity.py (the identity and the joint search), PROOF-LEDGER.md defect #20.
Level 2 of the hierarchy in INTERACTION-CONTROL-REPORT.md asks for state retaining one off-line pair marked against two consecutive on-line gaps, an exact object giving projective…
No — and for a sharper reason than incompatible offsets: the level-1 envelope is not attained in even one cell.
Theta is positive at the single-pair reduction, by a wide measured margin (the scan stays safe through theta = 0.9), and the mechanism is exact.
Level 3 left two named gaps in promotion order: a bound on the adversary's value valid over all configurations (its worst case was measured over two families), and the multi-pair slack…
The directive set two promotion gates: rigorous enclosure of the level-4 cells, and closure of the general multi-pair interaction.
Level 5 ended with the combined per-pair budget overdrawing by 0.151–0.387 of slack at every depth and two named reversing estimates. Both landed:
Level 6a's theta_full = 0.02 carried the label "at unit pair density". This level asks what happens when the density is the adversary's to choose, and the answer has a structure worth…
1. The joint cap exists and closes the entire swept density axis. The named theorem object of level 6b — an on-line-configuration-free upper bound on the joint profit against a pair cluster…
The operator's instruction: go find previously unknown mathematics adjacent to the 10 August 2026 paper (More than two thirds of the zeros of the Riemann zeta function lie on the critical…
Date: 2026-08-13. Purpose: price the asset before anything is built on it publicly. Companion to NOVELTY-CHECK.md, which killed a different claim from this hunt on 2026-08-12.
Date: 2026-08-12. Purpose: avoid a false novelty claim.
O9Check.lean had never been elaborated (§5 explains why: nothing imports it, and it was additionally missing the import of its own damageIv).
Status: ready to build. Scoping is done (O9-SCOPING.md, o9_scoping.py, 17 pins in test_o9_scoping.py). Nothing below is research; every number it needs already exists.
2026-08-13. Follows O9-2D-STATUS.md §0, which recorded that decide +kernel refuted the generated O9 table on 7 of 9 chunks.
Date: 2026-08-13. Code: o9_scoping.py, test_o9_scoping.py (17 pins). Reads: RETENTION-PROBLEM.md §4 (the obligations) and §7 (the arithmetic).
Written 2026-08-12. The plan for finishing the Lean arm of the transplant chain (and the one adjacent higher_xi batch), arranged as four independent lanes plus a standing collection loop.
Zeta Lab — August 2026. Working paper: candidate result, external review invited.
Audited local state: add40513fb1919ea4d00f87bdb61b5b433f7801d.
Evidence for the meta/ arm, written from the job history rather than from impressions. This hunt ran nine submissions to Harmonic's Aristotle service on 2026-08-12/13 (a tenth is still…
Status: CLEAN KILL. The unconditional candidates 0.6725124, 0.672529, and 0.6725318 are withdrawn.
Target: remove the hypothesis hsep from Retention.retention_separated_of_le and the hypothesis n ≤ 3 from Retention.retention_le_three, in the package hunts/frontier_math/zeta23ext…
State as of 2026-08-13. The single-pair (k = 1) retention inequality is closed at hardened grade with no separation hypothesis (ledger, four instruments plus a coordinator reproduction).
INTERACTION-CONTROL-REPORT.md closed with: "No decimal search should run before level 1 below has an unconditional zeta constraint that excludes the obstruction family." This report…
Clone: git clone --depth 1 https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean.git →…
Written 2026-08-13 as a handoff, because the working record grew to 29 markdown files and 8131 lines and buried the one thing that matters. Read this file.
Scope: fit against the four open items — the bandlimited nonnegative-kernel inequality over exponential sums, uniform in configuration; the finite→infinite-lattice bridge and the…
The candidate reading's most dangerous unproven step — "the transplant lemma" connecting theta_full (proved at the hunt's window) to the Cheer-Goldston floor (computed with the…
A Lean 4 package depending on the source paper's formalization (anthropics/zeta-23-lean, pinned by commit; toolchain and Mathlib pin inherited from it) into which the frontier_math formal…
Exploratory studies, explicitly not results. A hunt records a claim before any control has been run against it, which is why each one carries a mission stating what it may touch.
Adopted on probation, 2026-08-11 (ROADMAP.md, "The outside memos, triaged", adopted build 3). A HuntSpec is a fenced block inside a hunt's MISSION.md that states, in a form a validator can…
A hunt is an exploratory study: a scoped directory where an agent or a person pursues one specific idea, with the understanding that most such ideas fail.
Every claim this run touched, whether the run generated it or the repository already carried it. A claim with no disposition is an unfinished claim, not a true one.
The point of a graveyard is that a laboratory which remembers why ideas failed becomes harder to fool.
The metric the operator named is legitimate research output per unit of scarce human judgment. That needs a denominator, and the denominator is only useful if it is not gamed.
Agent persona: the Directorate (an internal organization with deliberately conflicting roles, not one agent) Scope: hunts/director_run/ for artifacts; docs/25-the-director-run.md for the…
Written before the first result came back, so the allocation can be scored against what actually happened. Amendments are appended with a timestamp, never edited in place.
Opened 2026-08-13. Nothing in this directory is a result.
Agent Persona: The Hunter Your Scope: hunts/factorization_vs_position/
Agent Persona: The Hunter (unsupervised-fun edition, second outing) Scope: hunts/flow_repair/ only. Nothing outside this directory is modified except the case-log entry in hunts/README.md.
Run of 2026-08-07, probe.py, raw numbers in results.json. Probe language throughout: measured, observed.
A cartography exercise, not a search. wide_search mined one method — the 10 August 2026 paper More than two thirds of the zeros of the Riemann zeta function lie on the critical line — for a…
Status: a map, not a result. Every computed number below was produced by frontier.py (optimiser shared with wide_search), cross-checked against the paper's closed form where one exists, and…
Question. The sharpest gate in this repository is the quasicrystal gate (zeta/quasicrystal.py, docs/18 §4): the zero measure's Fourier transform is atomic, and the atom pattern detects the…
Status: probe, complete. The quasicrystal lane now has its ground-truth universe: the tapered-transform instrument, pointed at a golden cut-and- project set whose atomic diffraction is…
The finite logarithmic mean square is now present in Lean. Its RC2 specialization reduces the remaining coefficient bookkeeping to two explicit endpoint-energy sums.
Half-band update. URMS2-051.md retains the individual log n spacings and the exact two-range coefficient weights in the finite mean square.
The corrected coefficient series is not presently identified with the pair form factor of the zeros of xi'' by the available analytic argument.
The displayed kappa=2 row in Bian Figure 10.1 does not survive independent reconstruction. The first divergence is already
The corrected coefficients define an absolutely convergent power series on |alpha|<=1. In fact, the majorant below has infinite radius.
Status: proposal, not a result. Written from the higher_xi side and aimed at another arm's open step; nothing here is promoted, and the arm it is aimed at owns the decision.
Status: probe record. Two independent derivation chains for the retargeted gate of LEAN-FRONTIER.md item 19, each with every link checked numerically at X = 250 and X = 5000, plus two…
The HigherXi, LogMeanValue, ComplexLogMeanValue, TwoRangeWeights, PowerMargin, MeanSquareAssembly, AristotleRAMS2, and RC2PrefixAssembly modules are the first formal slices of the rebuilt…
Attack the open higher-derivative form-factor problem left by Ji Bian's 2008 thesis and exposed by the August 2026 rank-trace paper.
The source of the elementary x(log x)^2 bound is exact. It is a support overcount, not genuine mass in the level-one resummed coefficient family.
Bandwidth update. BANDWIDTH-FORENSICS.md audits the constants used below. The rho<=1/10 and |alpha|<1/100 values in this report are the first explicit promotion, not final endpoints.
The 0.9544 and 0.9774 proportions on page 93 of Ji Bian's 2008 thesis are chapter-11 calculation errors.
The corrected level-2 coefficient series is now an understood infinite object. The present outcome is split:
This audit closes at Outcome D, current technology barrier.
The old coefficient-tail barrier is closed. CORRECTED-F2.md gives an exact majorant for the infinite corrected series and the uniform bandwidth-one bound
This phase reaches Outcome B: level one repaired, level two blocked.
URMS2-051 survives the independent internal audit.
The strict half-band restriction was created by a worst-frequency-spacing majorant. It is not present in the RC2 Dirichlet polynomial.
This attack closes at Outcome D, resummed barrier sharpened.
Question. zeta/li.py's real-rootedness lane asks about Jensen polynomials J^{d,n}; hunt #4 measured when the de Bruijn–Newman flow lands the Davenport–Heilbronn off-line pairs.
Things that belong to other parts of the tree, recorded here rather than done, because this hunt may not touch zeta/.
Status: probe, complete. Instrument kept; no claim promoted; the headline is a measured dictionary — finite Jensen degree acts on the counterexample's off-line pair as de Bruijn–Newman heat…
Agent Persona: The Hunter (unsupervised-fun edition) Scope: hunts/lehmer_pair/ only. Nothing outside this directory is modified except the case-log entry in hunts/README.md.
Run of 2026-08-07, probe.py, backends 'mpmath.iv', 'python-flint', raw numbers in results.json. Probe language throughout: measured, observed, decided (= an enclosure returned lo > 0 or hi…
One documentation defect found in the repository, one new hunt to file, and one process note. Ordered by what needs a decision from you.
Agent Persona: The Hunter (ontology-attempt edition) Scope: hunts/local_positivity/ only. Nothing outside this directory is modified except the case-log entry in hunts/README.md and the…
tests/test_hunt_probe_discipline.py::test_no_hunt_claims_the_reserved_word is the guard that keeps hunts/ from claiming the word zeta/rigor.py owns.
Status: settled. The guard's boundary is a case-insensitive match on one literal substring. Everything outside that substring passes, including the four words the repository's own…
harness/departments/guard_ledger.py carries the guard scripts/make_context.py --check with fired=None, known_misses=() and scope="undetermined until demonstrated".
Question. Does scripts/make_context.py --check catch its declared smallest mutant, and where does its sensitivity stop?
harness/departments/guard_ledger.py carries this record:
Status: settled, at the level a mutation battery can settle it. Ten mutants built, ten run, one null control.
Written for an agent starting cold. Read MISSION.md for scope, RESULTS-xiprime.md for the finished piece, RESULTS-higher-derivatives.md for the blocked one. This file is the operating state.
A breadth-first search for one externally checkable mathematical contribution adjacent to the Riemann zeta function, run under the laboratory's standing controls.
Status: a measured obstruction and a located piece of buried prior art. Not a result about zeta. Nothing here is evidence for or against RH.
Status: one exact collapse result, a full reproduction of every number the public artifact makes reproducible, and one measured gap between the paper's prose ceiling and the finite law…
Status: measured, and independently reproduced three ways. Not a new analytic theorem — an optimisation, run to its exact answer, of a functional somebody else derived.
The framework this laboratory built, tested against the practice it meant to improve, and shut down. Protocols were frozen and published before their arms ran, so the negative result cannot be re-cut.
This package answers one question about an empirical claim:
Repository: teal-sea/zeta-lab · Date: 2026-08-13 Subsystem under test: harness/ — a subject-independent validation framework Question, as posed: does using the harness improve the…
Ten departments authored by ten independent parties against a sealed kit, and the evidence behind docs/23 §8. Read docs/23 first; this directory is the artifact, not the finding.
Module: $BLIND/party01/department.py Final grade: CALIBRATED (all 18 named checks pass) check.py runs: 4 (counted honestly — 3 that drove changes, plus one final confirmation run after…
Result: grade: CALIBRATED, all 17 named checks pass. The battery measures nothing.
Module: $BLIND/party03/department.py Domain: shipping container manifests. Final grade: CALIBRATED (18/18 named checks pass).
Module: $BLIND/party04/department.py Final grade: CALIBRATED (18/18 named checks pass)
Module: $BLIND/party05/department.py Grade reached: CALIBRATED, in 3 runs of check.py (counted honestly, including the one that never got as far as a grade).
Result: grade: CALIBRATED, all 18 named checks pass, and every absurd claim I have thrown at the battery comes back distinguishes=True.
Final grade: CALIBRATED (all 19 named checks pass). check.py runs: 17. Full log at the bottom, honestly counted, including the six confirmation runs at the end and the two runs that never…
Domain: calendar recurrence rules — does this rule ever fire on a leap day? Module: $BLIND/party08/department.py Final grade: CALIBRATED (18/18 named checks pass)
check.py runs: 5. Final grade: CALIBRATED (19/19 named checks pass).
Status at this commit: pre-registration. No arm has run. No result exists. The claims and the answer key are deliberately not in this commit — agents in this experiment have repository…
Status at this commit: pre-registration. No arm has run. No result exists. Claims and key are held outside the repository during execution, as in v1; only their digest is frozen here.
Status at this commit: pre-registration. No arm has run. No result exists. Items, key and mutation family are held outside the repository during execution; only their digest is frozen here.
Frozen before any run. 6 items, 12 runs. One question, yes or no.
Evidence about the research system rather than about zeta: what a human had to do that the machinery could not, with the missing capability named.
This repository studies a mathematical object. It also, increasingly, studies the research system attempting to study it. This directory holds the second kind of evidence.
Nothing here is a mathematical result. This is evidence about the laboratory, in the sense of meta/README.md: an attempt to name missing capabilities, because you cannot automate what you…
Pre-registration draft, 2026-08-10. Nothing here has been run. Predictions are stated before any data exists, and the whole point of writing them down now is that they can embarrass me…
2026-08-10. Derived from the intervention ledger's first cohort plus the disagreements recorded in the session that produced it.
The reading path, derived line by line. Laid out in order on the reading page; listed here for completeness.
The short version. The Riemann zeta function starts life as the sum 1 + 1/2^s + 1/3^s + ..., which converges only when Re > 1, but extends uniquely to a function defined on the whole…
Or: "is the harmonic series / Riemann-sum thing actually connected to the zeta function and to derivatives?" — yes, and here is exactly how.
"Can you model the theta function with a differential equation?"
Riemann's functional equation is not a coincidence you verify afterwards; it is a change of variable.
"What do the zeros actually have to do with the primes?"
The payoff of docs/02-theta-heat-and-modularity.md. There we watched heat flow produce Xi. Here we run heat flow on Xi and ask how the zeros move.
Or: the spectral dream. Why "there ought to be a differential equation behind this" is the right instinct, why nobody has produced the equation, and why the zeros nevertheless behave…
A curated catalogue of statements exactly equivalent to RH, with honest notes on which ones have ever gone anywhere.
Every technique in this repository — Mellin transforms, the functional equation, contour integration, the explicit formula — is genuinely powerful, and every one of them has a known ceiling…
The sequel to docs/08-why-it-is-hard.md. That document catalogued why the existing tools provably stall.
"The explicit formula looks like modal analysis. So what is the structure — and who gets to tap it?"
A companion to docs/09-new-ontologies.md. That document surveyed the "new objects" landscape and docs/10-trace-formulas-and-connes.md slowed down on the trace-formula corner; this one slows…
docs/08-why-it-is-hard.md catalogued what fails. docs/09-new-ontologies.md described the one time a rebuild worked.
The moments programme starts with a data contract, not a formula. The lab's local cache reaches only the low thousands in height; the external tables that matter live at much larger indices…
A companion to docs/12-how-hard-problems-die.md. That document is a kill board: eight problems, the mechanism that killed each, and RH scored against them.
Building the Polya-Hilbert Operator Computationally
The goal of the current sprint is to pass the Counting Gate. To do this, we must build a computational model of the Poisson-summation map on the Adelic Schwartz space, and demonstrate that…
A methods retrospective. Everything in docs/00–16 is about the mathematics; this document is about the refereeing.
A session's worth of deliberately improbable attacks on RH, each pushed until it either produced something measurable or hit a named obstruction. None of them advance RH.
A side project, and a probe rather than a department — see §6, which is the most useful part of this document because it is the part that says no.
The architectural record of the 2026-08-09 build: what was latent, how it was attacked before it was built, what survived, and where it stops.
Status when this file was committed: pre-registration only. No result in it. Everything below §5 was written before the gate existed, before any case was run, and before any number was…
Abstract The Riemann Hypothesis possesses numerous mathematically equivalent statements (Li's Criterion, Weil Positivity, Mertens' Conjecture, etc.).
Status of this file when it was committed: pre-registration only. Nothing in §§5–8 existed. No number below §4 had been measured.
An ontology attempt in the sense of docs/09 §4: propose a structure, push it at the gates, and record exactly where it bleeds.
2026-08-10/11. An operator handed the laboratory over with no theorem, no direction, and no assurance that the agenda was the right agenda.
ROADMAP.md ("The outside memos, triaged") records the decision; this document records what landed the same day, what each piece can and cannot claim, and where each one's honest edge is.
12 August 2026. A reading of the laboratory's current frontier work, written because the state changed four times in one day and the front page carries only the conclusions.
One page per way into the repository. A repository with several purposes does not get several repositories; it gets one verified core and several short entry points.
For you if you care less about the Riemann Hypothesis than about the problem it forced this repository to solve: when plausible ideas cost minutes to generate, the scarce resource is…
For you if you care about the difference between a number that is accurate and a statement that is proved, and want to work where nothing is measured.
LLVM IR rewrites — department #3, and the first whose subject shares no vocabulary with the mathematics: programs, not functions.
Subject. A frozen implementation of true union semantics for restricted day-of-month/day-of-week cron fields under the # (nth weekday) and W (nearest weekday) special forms — a feature…
For you if you want to generate leads automatically — and, more usefully, to see what fraction of them survive.
Curves over F_p — department #2, and the first second subject: the same referee architecture under a property that is decidable.
For you if you want real intuition and real numerics about ζ — to watch the theorems occur rather than read that they hold.
Subject. Batteries themselves. The payload of every claim in this department is a harness.protocol.Department bundle, and the claims are about whether such a bundle deserves trust: not…
For you if you have a structural claim about the zeros — a spectral operator, a positivity argument, a pattern in the statistics — and you want to know whether it is about ζ at all before…
Subject. The commonest claim in applied machine learning: "model B genuinely improves on the baseline." A subject here is a comparison — candidate pipeline, baseline, and the pair's own…
The Riemann zeta function and RH — department #1, and the worked example every later department should copy.
Zeta Lab should evolve from a zeta-specific research repository into a research operating system built around its validation harness.
Purpose: Identify the highest-value live research fronts in the current Zeta Lab repository and recommend how available parallel-agent capacity should be allocated.
Documents written about the laboratory by parties outside a working session: strategy memos, portfolio recommendations, external evaluations, and the design for an experiment that has not…
Independent repo-side analysis, performed without seeing another model's prior evaluation. Grounded directly in git history and current file contents as of 2026-08-08.
Planning-only pass. Repository not modified. This document turns the prior recommendation (bounded internal probe: E1 intervention ledger, E2 Lab Rotation Benchmark, E3…
Contract = Rev. 2 + Rev. 2.1 patch. This document adds no rules; it sequences the work and specifies the one procedure the contract references but does not define: blind lesion authoring by…
Accepted. The asymmetry in Rev. 2 was inconsistent: success-shaped conclusions required both families, but KILL fired on either.
Planning only. Nothing implemented. This document supersedes the affected sections of e1-e3-experiment-protocol.md; everything not revised here stands as written there.
This packet is the only material the consultant receives before reveal. It contains no owner-authored lesion instance, diff, answer-key entry, surface wording, or benchmark output.
The decisions, the between-session state, and the standing rules any agent working this tree has to read first.
A computational laboratory for the Riemann zeta function and RH. Read README.md for the front door and docs/00-orientation.md for scope.
A computational laboratory for the Riemann zeta function and RH. Read README.md for the front door and docs/00-orientation.md for scope.
Generated by scripts/make_context.py. Do not edit by hand — regenerate.
Concise records: what was believed, what invalidated it, what now catches the problem, what conclusion is currently justified.
Status when this file was committed: pre-registration only. No result in it. Everything below was written before any arm was run, any task was authored, or any number was seen.
Date: 2026-08-04 Code: zeta/surrogate.py, scripts/15_null_control.py, tests/test_surrogate.py Commits: 18967ff, 61e3cbf, bb634a8, e248d15 Answers: attacks A1–A3 of REDTEAM.md §3.
A computational and formal workbench around the Riemann zeta function.
Date: 2026-08-04 Scope: the moments build sequence 6814f9d..9bd6dd3 (module zeta/moments.py, scripts/14_moment_experiment.py, its tests, HANDOFF.md, ROADMAP.md, docs/13-moments.md).
README.md says what the lab is. AGENTS.md says how to work in it. This file records the decisions: why the work went the way it did, what is deliberately not being attempted, what is known…
Operational reference for telemetry/. What a run is, where records live, how they get written, what is authoritative, and what this cannot see.
How the pieces are built and why, plus the annotated reading list and the records the other pages cite.
Verdict: PROVISIONAL. The subject fits the protocol better than expected — all four roles have natural compiler-domain analogues, and both calibration directions work on the first attempt.
An experiment: can intent, definitions, provenance, evidence, failed attempts, proof obligations and verification status be represented so that an agent can perform and resume rigorous…
Fetched 2026-08-11. Nothing here is part of the laboratory; these are other people's artifacts, kept local so instruments and literature checks can collide with them offline.
Standalone HTML pages that animate what the laboratory computes. They are illustrations, not results: nothing here is measured, tested for mathematical content, or cited by any claim.
The proof-agent adapter's durable ledger (lean/proof_adapter.py; contract in docs/26 §4). Every submission is recorded here with its project id so any later session can collect.
Target: hardyZ Status: Ready to draft Lean code Workspace: lean/ZetaLean/ Target Host: leanprover-community/mathlib4
To set up your new GitHub repository, follow these steps:
Plan file: rung3_plan2.json. The naive boxed-s lower-bound evaluation is gone; the small-square frontier is now certified by point enclosures on a grid + a Lipschitz bound L, where L = M/…
Phase 4, step 1: the schema and nothing else. No generators, no screens, no pattern hunting. This document defines what a candidate observation is, what can be concluded about one, what…
Generated by scripts/mathlib_gaps.py from docs/1000.yaml — snapshot 2026-08-06. Do not hand-edit; regenerate.
Companion to the course in docs/ (each doc cites what it leans on; this is the consolidated shelf). FREE marks items legitimately available online at no cost.
Recorded before any file was created, because the contract this work runs under is that live frontier research outranks it.
Nothing in this directory is active. These files are templates, and the reason is the isolation contract this system was built under : two frontier research sessions were live when it was…