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).
Every document this laboratory publishes, not only the parts
that worked. 572 documents, 138,654 lines, listed straight off
git ls-files. The tree's housekeeping is not here: the
instructions its workers read, the between-session handoffs, the harness's
notes on its own trials. Those stay in the repository, which is public, and
anyone cloning it to send a change reads them there.
| 572 | documents |
| 138,654 | lines |
| 5 | 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).
What modification of the world would preserve the appearance of this result while making its interpretation false?
2026-08-13/14. Measurements only. Nothing here is kernel-checked, nothing here is evidence about RH, and nothing here closes blocker 2.
Status: WITHDRAWN / FALSIFIED UNDER CURRENT FORMULATION Date withdrawn: 2026-08-15
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.
2026-08-15. Reads: K2-ROUTE.md (the state it supersedes in part), RETENTION-PROBLEM.md (the k=1 proof whose machinery this transplants), gram_form.py / kpair_identity.py (the identity…
A route to proving lattice extremality, worked out far enough to say exactly what is proved, under which hypotheses, and what is missing.
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.
2026-08-13. Found by trying to perform the final assembly and failing. Nothing here is kernel-checked, nothing here is evidence about RH.
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.
Successor to Hunt #72 (hunts/r_662b12, run 31e8a4f2), whose reported +25pp robustness signal was withdrawn by independent audit (in-sample rule on the 28 labels, scrambled-text control…
Frozen 2026-08-22, before any predictor is fitted against the robustness labels. The descriptive curation finding is not a fitted predictor and does not depend on this document; this…
AIMO Interpretability Challenge at NeurIPS 2026 (Codabench competition 16180), technical report. Every number below is reproducible from the organizers' public datasets by…
Status: report-ready (reframed 2026-08-22); Main-track entry is a legal model-identity prior; Small-track entry is the always-non-robust constant; leaderboard learned-method arm stays…
Formal-native research probe, run 2026-08-23. One obligation, not a formalization of a paper. The success criterion set for it was did formal feedback change the mathematical understanding…
Ainta's seven-point simple-zero bound (paper/riemann.tex at ainta/zeta-simple-zeros commit 040c5e899e658aed7b56a2a87f501798fe10761d, cited A with line numbers), stated and proved in Lean on…
Every figure is labelled VERIFIED (read off a file or a build), MEASURED (computed this session), INFERRED, or NOT MEASURED.
Two outside groups are hill-climbing the same finite certificate for the proportion of simple zeros on the critical line: Ainta (ainta/zeta-simple-zeros, a GPT-5.6 Sol research draft with…
Gohms's run is the published verifier with two constants changed. Nothing else in it is new, and the issue says so.
Environment for every run below: macOS (Darwin 25.5.0, Apple Silicon), Python 3.14.7, python-flint 0.9.0, ainta/zeta-simple-zeros at commit 040c5e899e658aed7b56a2a87f501798fe10761d…
Every figure is labelled VERIFIED (read off a file or a build this session), MEASURED (computed this session), INFERRED, or NOT MEASURED.
Written 2026-08-23. Companion to this hunt's MISSION.md, which reproduces the finite certificates and which was still uncommitted in a sibling worktree when this landed, so this file may…
Agent: bridge/S8 (branch bridge/S8, from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/S9 (branch bridge/S9, from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/finite (branch bridge/finite, from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/pinching (branch bridge/pinching, forked from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/skeleton (branch bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
AMTOPA/zeta-exact-pressure holds the leading public claim for the proportion of simple zeros, 0.6734164909714992949..., first in the fifteen-claim ranking this laboratory's own field audit…
Target pinned at AMTOPA/zeta-exact-pressure, commit 7253fdcab9366af45b8c8caf44e408c0af44a1a7, 2026-08-13 17:26:37 +0800.
Every run of this hunt, including the ones that produced nothing and the one that had to be killed.
Third application of the lab's procedure for a published computer-assisted bound (after the two seven-point simple-zero certificates of Hunt #79): reproduce the bound from its own verifier…
Archive bloch-computations-1.0.0.zip (Zenodo 10.5281/zenodo.21975862), sha256 bdaa1ff3…408e7 verified, all 28 entries of CHECKSUMS.sha256 verified.
Environment for the local runs: macOS (Darwin 25.5.0, Apple Silicon), CPython 3.12.12 in a fresh venv from the archive's requirements.txt (python-flint 0.9.0, numpy 2.5.1, scipy 1.18.0), on…
Is there any mathematically nontrivial correspondence between the twelve chromatic pitch classes and the colour wheel, beyond the fact that both can be drawn on a circle?
One fixed positive Fourier density gives two real multisets with identical power traces at every order and different numbers of simple points.
This note derives a finite-dimensional extension of the counting mechanism in Proposition 2.1 of Youness Lamzouri, A new proof that more than 2/3 of the zeros of the Riemann zeta function…
Started 2026-09-05 under the operator's instruction to pursue substantive mathematical research with the available provers and compute resources.
This note gives a finite counting improvement whose denominator uses a narrow fourth moment. Its first Montgomery-Taylor profiles do not produce a positive numerator.
The repeated-index corrections below are exact. Applying separate bounds to their terms can lose information, and power traces alone do not determine every corrected cycle statistic.
This is a finite statement about a conjugation-invariant multiset. It gives no new asymptotic bound for zeros of zeta. The arithmetic cost is stated below.
Finite counting improvements are proved here. Their application to a stronger zeta-zero proportion remains open.
The hunt produced finite counting inequalities and an exact counting distinction invisible to the complete spectrum. It does not improve the laboratory's asymptotic zeta-zero proportion.
Base commit: 6139de6173ea7e538db6097170a1ccfe93f311cb. The dates below record the research day, not reconstructed wall-clock times.
There is one even, nonnegative, compactly supported probability density whose Fourier kernel gives two full-rank, four-point Gram matrices with identical spectra and different distinct…
Under the finite signed-vector hypotheses of FINITE-THEOREM.md, matched second and third moment limits alone cannot improve the second-moment counting proportion.
Base commit: 85efdcb2b4f8255caed8dbac0961c28361abd413. Status: bounded construction, not an established heat-flow comparison.
Status: candidate ordinary argument with enclosure-carrying numerical steps. Independent Muse and Gemini reviews found no analytic or implementation defect in the complete packet.
Base 85efdcb2b4f8255caed8dbac0961c28361abd413 has successful GitHub Actions tests run 34913353458 and full run 35095988548, read through gh in this session.
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.
Exploratory. Nothing here is a result (see hunts/README.md).
A bounded measurement run. One quantity, two precisions.
zeta/epstein.py caps working precision in one place inside the rival interface it hands the battery: epstein_interface"count_zeros_box" passes dps=min(d, 20) both to count_zeros_box and to…
Opened 2026-08-14. A bounded measurement, not a claim about zeta and not a result. Nothing here has been through a control.
A bounded measurement run, opened 2026-08-14 by the operator. One number, at two precisions, plus the sweep needed to read those two numbers against a scale.
A bounded measurement run. One quantity, two precisions.
Status: probe, complete. At 0.8 + 85.7i the capped precision does not return a worse answer, it returns no answer: 3.1e-33 where the converged value is 1.6e-58, a factor of 1.9e25 and not…
Opened 2026-08-13. Nothing in this directory is a result.
Nothing in this directory is a result. hunts/README.md classifies the area: a hunt is exploratory, and this one was opened to state a single mechanism for the Riemann Hypothesis and then…
Nothing here is a result about the Riemann Hypothesis. This is the report of one attack on one mechanism, and the mechanism did not survive it. No progress on RH was made.
id: epp_herglotz-2026-08-19-run1 hunt: epp_herglotz started: 2026-08-19T00:00Z finished: 2026-08-19T00:00Z ran: - .venv/bin/python hunts/epp_herglotz/probe.py outcome: the mechanism stated…
Agent Persona: The Hunter Your Scope: hunts/factorization_vs_position/
This file has been through an independent adversarial audit and did not come out unchanged. A different model (OpenAI Codex, gpt-5.6-sol), working in an isolated directory outside this…
The n-point pressure certificate family gives, for each n, the bound
lim{n -> infinity} Phi_n = H = 0.6725007036794116 DERIVED, exact sup_n Phi_n <= 0.675142509660254 AUDIT, VERIFIED here configuration ceiling 0.6818286874638 deficit at the family's best >=…
id: family_wall-2026-08-23-analytic-limit hunt: family_wall started: 2026-08-23T15:40-05:00 finished: 2026-08-23T19:10-05:00 ran: - .venv/bin/python hunts/family_wall/verify_chain.py…
You are auditing a mathematical claim that the person who wrote this believes is TRUE and wants you to attack. Your job is refutation, not confirmation.
The isolated repository's history, oldest first:
The supporting argument is false as written. Steps 2 and 3 both omit necessary conditions. Step 2 reverses direction when its numerator is negative.
Each decimal below is interpreted exactly as printed. The corresponding directed interval evaluations are in intervals-requested.json.
Occasioned by discovering, on 2026-08-24, a wave of public repositories created 2026-08-11 and 2026-08-12, a week before this laboratory's own seven- and eight-point work, carrying…
This laboratory's number is not the leading one, and never was. Our best figure, 0.6730529829896288 (eight-point, bridge proved in Lean), is tenth of fifteen public claims for this…
One night, one host (13-inch laptop, no cloud, no Lean build). Every external repository was read or replayed read-only; nothing was posted, opened, commented, forked or starred anywhere.
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.
This directory preserves the arithmetic and terminal verification status of the 2026-09-05 experiment.
Lab kernel build recorded; not ready for Palomar submission. The proof handoff is complete. The registry's current compatibility requirements are a separate obligation.
Current status : the Lean kernel build of the c = 2330/10^6 candidate has been run and passed, locally by this laboratory, on Modal.
Recorded 2026-09-28. This is the laboratory's kernel build of the generated FourPointCand package at the pinned toolchain. It is not external review and it is not a Palomar registration.
- Verdict: FULL PASS: every layer checkpointed, verification clean - Run id 20260928t220203, Modal app id ap-7zxzQj0YqTwlQUP6P06ecn (profile teal-sea) - Source HEAD…
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…
Status at the time this file was committed: nothing has been computed. The parameters below were fixed first, on the reasoning recorded below, and the commit order is the evidence.
Verdict: VACUOUS. A rival satisfies property 6 in the very box chosen in advance to make that hardest.
Status when this file was committed: nothing has been computed. No zero count, for any function, in any box, had been evaluated when this file landed.
Verdict: VACUOUS. Two of the three preregistered boxes were decided for all four functions, and in both of them all three RH-violating rivals satisfy property 6 exactly as ζ does.
Status when this file was committed: nothing has been computed. The parameters below were fixed before a single truth value was produced.
Status: settled, in the sense that matters, and explicitly not settled in one arm. Nothing here is a result in the repository's sense, and nothing here is evidence for or against RH .
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…
RISK STATUS: CLOSED, and it is a mixed verdict.
Written 2026-08-16, as closure item of GATE.md.
Adjudicated 2026-08-16 (verdict NOT YET, five closure items). Re-adjudicated 2026-08-16 after the repairs, by a session that did not make them. Every field below is at post-repair state.
Written 2026-08-16 to close GATE.md item . The hunt said "two independent winding routes" (MISSION.md WP1, pre-registered prediction P2) and printed that adjective in its headline.
Written 2026-08-16. Vocabulary per MISSION.md: measured is one float route, decided is an enclosure with exact endpoints settling a sign or a containment, cited is somebody else's theorem.
Written 2026-08-18, as task 2 of the pre-submission hardening of hunts/lambda_dh_bounds.
Opened 2026-08-16. Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
Recorded 2026-08-16, from a web sweep run before the hunt opened. Per the house rule (ontology/knownness.py: an unrun check can never read as absence of prior art), this file says exactly…
Written 2026-08-16. The separation claim Lambda_DH > Lambda_zeta is load-bearing on the exact statement and frame of Polymath 15's upper bound, so both papers are quoted here at source…
Written 2026-08-16, after the gate returned NOT YET with a five-item closure list, and after those repairs were made. This file is the hunt's written record.
Written 2026-08-16, after the gate closed (GATE.md, verdict YES) and after a dedicated novelty adversary attacked the claim's phrasing.
Section draft for WP2 . Instrument: strip.py; decided values in strip_results.json. Vocabulary per MISSION.md: decided means an interval or ball whose exact endpoints settle a sign, stated…
Section draft for the pre-submission hardening of WP2 . Instrument: strip2.py; decided values in strip2_results.json.
Source pinning for WP2 (upper bound) and for the Dobner half-line structure the lower bound leans on.
Scratch analysis, 2026-08-16. Written by an adversary tasked with breaking the claim 0.0576 < Lambda_DH <= 0.4006343708899557, not with defending it.
Scratch analysis, 2026-08-16. Remit: break the upper side. Nothing in this file is an enclosure; every number below is measured on one route unless it says otherwise, and the routes are my…
Scratch analysis, 2026-08-16. Written by an adversary tasked with breaking 0.0576 < Lambda_DH <= 0.4006343708899557 at the instrument layer, not with defending it.
Scratch analysis, 2026-08-16. Written by an adversary tasked with breaking the novelty of 0.0576 < Lambda_DH <= 0.4006343708899557, not with defending it.
Opened 2026-08-18. Hunt #119 (renumbered from #52 on 2026-09-12). Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
Status: OPEN. There is no result here, and this file exists to say so precisely rather than to leave the question to a reader's charity.
Every run this hunt ever performed, including the ones that produced nothing. Reconstructed 2026-09-12 from the committed artifacts and the session record, because the runs that would…
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…
Opened 2026-09-27 on branch teal-sea/oob-cert from origin/main . Scope: hunts/oob_envelope/ only, plus this hunt's case-log entry in hunts/README.md.
Read first: hunts/oob_envelope/MISSION.md, then AGENTS.md (certainty ladder, compute discipline, reserved words), then arXiv:2608.24827v2 §1–5 and §7.
HOLD after stage B (approved by Thomas 2026-09-27, run, terminal). Stage B: λmin ≥ 5.71789230595e-48 at L = 1.19, T# = 500, N = 500, enclosure-carrying single route, 1.4 core-hours on Modal…
2026-09-28: the L = 0.8 bound and the L = 1.19 stage B bound both passed independent referee review (referee/REVIEW.md, sections "L = 1.19" and 5). Every grade uses the AGENTS.md ladder.
Every run that costs more than a local 10-minute, 2 GB slot is estimated here before launch. Nothing below has been launched remotely.
You are the adversary. You did not write this work and you share no code with it. You are started only when the supervisor has both the theory worker's lemma and modified reduction written…
Authorized by Thomas's 2026-09-27 task, received 2026-09-28. This supersedes only the earlier prohibition on new L=1.19 work. No push or PR. All writes stay under referee/.
COMPLETE: L=1.19 passes independent review on the full even sector. The CC-192/Arb route, N=500, proves lambda_min >5.7179e-48.
1. PASS, independent enclosure: CC-192/Arb proves lambda_min >5.7179e-48 on the full even sector, exceeding both requested and author endpoints. 2.
APPROVED batch completed: 5 successes, 0 failures, 0 inconclusive. Authorization is for these exact five units, sequentially, profile teal-sea, under 20 core-hours and a $0.15 allowance.
Read first: hunts/oob_envelope/MISSION.md, then AGENTS.md (certainty ladder, reserved words, original vs novel), then arXiv:2608.24827v2 §1–4 and §14–16.
STATUS: holding, no compute. RESULTS.md now cites the referee's final REVIEW.md per result, with no change of ladder grade (every proof stays an ordinary derivation, none kernel-checked).
Branch teal-sea/oob-cert-theory. Author: theory worker (Claude Code, Opus). Every statement below carries its grade on the ladder of AGENTS.md.
Status, 2026-09-06: closed on kill condition 2, at prose grade. RESULTS.md section 8: the out-of-band positivity is worth zero to any certificate whose positivity input is Weil's Hermitian…
Verdict, 2026-09-06: kill condition 2 fires, at prose grade. Section 8 has the argument; sections 1 to 7 are the measurements and the lemma it rests on.
All on the operator's 16 GB Mac, .venv/bin/python, HiGHS through scipy.optimize.linprog. Solve time grows like about X^2.7 in the truncation; the strip adds a few dozen rows and roughly…
Every certificate in the current race reads pair-correlation data on -1,1 and nothing else. The configuration ceiling for that information class is 0.6818286874638, and the whole public…
Verdict: the kill condition did NOT fire, and the hunt found a gap rather than a wall. The unconditional out-of-band positivity of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh…
Estimate written before launching. Two solves were timed first, on this machine: X=40, J=200 took 5.7 s and X=80, J=320 took 40.1 s.
Sixth instance of the ceiling procedure, and the first one aimed at a lower bound. Erdos's minimum overlap constant C. Opened 2026-08-23.
The ceiling procedure on the lower side of Erdos's minimum overlap constant. Run 2026-08-23.
One block per autonomous run. A run that produced nothing records that it produced nothing.
Base: a3acc741396940273ec388548d52752f839593c3.
The paid-shortfall construction has an explicit, fully charged family: truncate a finite balanced seed lift at square-root support.
Planned before the durable run: two seeds, three lift depths, N=2..128 and N=1296, with exact floor/cap checks through 1296. No optimizer, parameter search, random input, or unbounded loop.
This hunt evaluates one finite arithmetic diagnostic at N=144,576,2304,9216,36864. It imports the balanced-prefix cutoff choice from hunts/paid_shortfall_scaling/scaling.py unchanged.
This run used the repository virtual environment. Its reported backends were python-flint, with both mpmath.iv and python-flint available.
Checkpoint paid-scaling-01, base 4efa72ad70a1e535709c33d0eded886d29c19274.
This is an additional proposed refinement from the cap reviewer. It is not a dependency of RESULTS.md or the cutoff-selection algorithm.
Mathematical base: 4efa72ad70a1e535709c33d0eded886d29c19274. This continues paid_shortfall. Its definitions of W_c, B_N, psi, w_q, and C_N^U are unchanged.
Before the first diagnostic: five predetermined cutoffs, 144,576,2304,9216,36864; two coefficient families; two capacities; exact rational algebra; two interval logarithm implementations at…
Base: fd04f1fac9d48a4d769048817e678acdea3b4bdb. Read-only predecessor: af13799d3034b4d6a07e76c0d6a409dc7421f056.
Result: the specified finite feasibility problem is feasible. The vector
Base revision: fd04f1fac9d48a4d769048817e678acdea3b4bdb. The mission was the first tracked file created in this hunt. The checkout was already isolated on its assigned branch.
2026-09-11. Base: ENDPOINT_SHARP.md (commit 367573c, the endpoint checkpoint, unchanged), UPPER_BOUND.md sections 2 to 5, LOCALIZED_MIXED_ENERGY.md section 6, SIEGEL_UNIFORMITY.md .
Independent check, 2026-09-12 (attempt a-0078). Scope: the five items listed in the assignment, covering sections 1, 2 , 3 (major arcs), 4 (minor arcs, including 4.1 in full), and 5 of…
Date: 2026-09-20 (revised following independent review). Base commit: 271fc26. Prior work: FRONTIER_2026_09_12.md, SIGNED_MEAN_RENEWAL.md, FRONTIER_INDEPENDENT_REVIEW.md…
Date: 2026-09-20. Reviewer: Muse worker (Grok unavailable; this package covers both the mathematical challenge and the independent diagnostic).
2026-09-09. Base: 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. This is the next arithmetic estimate for the original CHHL total error.
2026-09-10. Builds on CORRECTED_RH_BRIDGE.md, LOCALIZED_MIXED_ENERGY.md and EXCEPTIONAL_ENERGY.md as they stand on this branch.
2026-09-09. Base: 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. PRs #209 and #210 are completed, separate attempts and are unchanged.
2026-09-10. Target: CANDIDATE_ENERGY.md as it stands on this branch, which claims not just the requested domination \(E{\rm corr} but the exact identity \ E{\rm corr}\qquad\text{for every…
2026-09-09. Base: PR #213 at 284a52fbb369f48fe011578bc7e0299b23b5bce0. The records in PRs #209-#213 and the completed literature comparison are unchanged.
This is the coordinator's candidate argument in the exact mathematical version reviewed on 2026-09-09. It had no endpoint commit when reviewed.
The coordinator supplied the candidate argument directly in the Codex review request on 2026-09-09. At review time it had no endpoint commit or attached file.
Correction notice, 2026-09-11. Section 2.3's conclusion that no choice of the Bonferroni cutoff \ works at \ does not hold.
2026-09-11, corrected the same day in three revisions (sections 2 and 4; every correction is recorded in place below rather than silently applied: the Mertens estimate in section 2, the…
Independent check, 2026-09-11. Read in order: ENDPOINT_SHARP.md, ENDPOINT_BOUND.md (section 2 and equations , , , , , , ENDPOINT_HALF.md (including its correction notice), and…
Independent check, 2026-09-11 (attempt a-0077). Scope: only the two substitutions of section 4 (the progression input and the separate sieve level \, which postdate ENDPOINT_SHARP_REVIEW.md…
2026-09-09. Continuation of PR #212 at 76ed1155d087d9137306d3632f66dba7555aadc3. SIEGEL_UNIFORMITY.md and the completed records in PRs #209-#211 are unchanged.
This document records the constructive next step in the arithmetic investigation of $D_N$, the defined signed prime-counting functional.
2026-09-12. Base: science commit 3b0fc2e3c97b46cc1fde6af0ff3dd856898d95fb. Review status is recorded in FRONTIER_INDEPENDENT_REVIEW.md.
Date: 2026-09-20. Runtime observed: Gemini 3.8 Flash high (provenance accurately recorded; not Opus, per coordinator notice).
2026-09-09. Base #215 at 3645324cf69497e197592fdcc2f630c4ed6504b0. Working record only. No research PR or push: this mechanism fails to improve the complete bound. #209-#215 are unchanged.
2026-09-12. Continuation from science commit 3b0fc2e3 and the separately recorded board/history at 88b5d1a5. Earlier work is preserved.
Date: 2026-09-12. Source base: zeta-lab commit 3b0fc2e3c97b46cc1fde6af0ff3dd856898d95fb.
2026-09-09. Base: #214 at cb0189db3863ac43b2314c7df1008636bd4da477. The accepted bridge and #209-#214 are unchanged.
2026-09-12. Base: ARC_SPLIT_BUDGET.md (commit a537765; its arcs, its minor-arc bound and its budget are reused unchanged), ENDPOINT_SHARP.md sections 1, 4 and 5 (the model at \, the…
2026-09-12, attempt a-0080. Scripts written fresh for this review, not reusing major_arc_explicit_probe.py: major_arc_explicit_independent_check.py (item 1) and…
2026-09-08. Continuation from UPPER_BOUND.md at 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. This is one attempted replacement of the minor-arc supremum estimate: retain the amplitude…
Chou, Haag, Huryn and Ledoan (arXiv:2308.14888, J. Number Theory 2025) define, for the von Mangoldt pair count psi_2(N, k) = sum{n, n' <= N, n' - n = k} Lambda Lambda and the…
Base: b8bb28c4de357827be0bdad95a5e9b40d9c4e669 (author file at 3d5c666634766357e2c6484afb0e6fbd4c8f2540; review at §7 repair spec incorporated 2026-09-20). Date: 2026-09-20.
- Target: hunts/prime_pair_error/MOBIUS_PAIRING.md - Base Commit: 425e4f46355c1f68bce3ed064b818de7f265feb3 (repair of prior review dispatch; author files remain strictly read-only at…
2026-09-12. Base: SHARP_EXPONENT.md (commit 3b0fc2e, the two-sided statement and its budget , MAJOR_ARC_EXPLICIT.md (its sections 2, 3 and 5, the lemma , the case analysis of section 3 and…
2026-09-10. Builds on CORRECTED_RH_BRIDGE.md, SIEGEL_UNIFORMITY.md and LOCALIZED_MIXED_ENERGY.md as they stand on this branch, and directly answers the question CANDIDATE_ENERGY.md left…
This document answers one question, precisely scoped: RANK3_ROUTE_D.md §6 shows that the direct, per-arc transfer bound used in its equation — the generalization of UPPER_BOUND.md's from \…
This document checks, against citable primary sources rather than by re-derivation, a specific hypothesis H that would be needed to push RANK3_MEAN_VALUE_TOOLS.md Section 3's…
This document answers the task assigned to it: whether RANK3_CROSS_TERM_CANCELLATION.md's identity \, proved there only for prime \, extends to composite squarefree \ with \ distinct prime…
2026-09-11. This document finishes the estimate that RANK3_COMPOSITE_CROSS_TERM.md section 5 left as its one remaining step: carry the exact conductor-weighted identity over the complete…
This document answers the task assigned to it: whether \(\Sigma{\rm cross} in RANK3_ROUTE_D.md's exact identity can be proven, not merely assumed or measured, to be small relative to…
RANK3_ROUTE_D.md's exact identity splits the coprime-driven part of \, summed over the reduced residues \(a\bmod q\), into a diagonal piece \(\Sigma{\rm diag} and a cross term \ \Sigma{\rm…
This document answers the question RANK3_MEAN_VALUE_TOOLS.md Section 5 and RANK3_BDH_VERIFY.md leave open: does an "integrated" Barban-Davenport- Halberstam-type theorem exist, or can one…
This document investigates, as RANK3_SCOPE.md Section 2 asks, whether some unconditional tool other than the three named in UPPER_BOUND.md -- the Siegel-Walfisz major-arc approximation…
This is an investigation, not a proof attempt, of one sub-question RANK3_SCOPE.md leaves open. RANK3_SCOPE.md Section 2 shows that none of the three tools UPPER_BOUND.md assembles…
This document answers the task assigned to it: search the unconditional analytic number theory literature for a "t-integrated" analogue of the Barban-Davenport-Halberstam /…
Scope and a note on method. This document answers the literature question RANK3_QUARTIC_TOOLS.md Section 3 leaves open (its own "wall"): is there a named, unconditional theorem bounding \…
Scope and relation to prior documents. This document's task is the one RANK3_QUARTIC_TOOLS.md closes with as unfinished (its §4, "What would settle this precisely"): search further for a…
A note on sources. This attempt's assignment describes a file RANK3_TOOLS.md (Section 3: a second-moment identity for \, which does not apply to \, verified in rank3_identity_check.py) and…
RANK3_SCOPE.md's Route A asks for an unconditional, uniform-in-\ estimate for \, strong enough to make \ S^2\sum{b\bmod q}^T, \qquad T^2, \tag{S}\ for \(R_0=\lfloor Q/L\rfloor\)…
This document carries out RANK3_SCOPE.md's Route D: the exact analogue, for general modulus \ and reduced residue \(a\bmod q\), of UPPER_BOUND.md's Parseval identity and its arc-transfer…
This is a scoping document, not a proof attempt. It does not estimate the quantities below; it says precisely what they are, why UPPER_BOUND.md leaves them unestimated, what closing them…
2026-09-11, corrected the same day (section 4 rewritten around a cited theorem; the first version carried a reversed density-exponent condition and an overstated zero-free-region saving…
This is a preservation record, not a new mathematical result or a change of research assignment. The current prime-pair continuation remains FRONTIER_2026_09_12.md, with its independent…
Editorial note, 2026-09-06: the absolute path of the reviewer's worktree was replaced with "an isolated local worktree" to satisfy tests/test_repo_hygiene.py, which bars machine-local paths…
All numbers below are in results.json, written by probe.py on 2026-09-06 (run cost in RUNS.md). Notation as in Chou, Haag, Huryn, Ledoan : psi_2(N, k) is the von Mangoldt pair count with…
Estimate written before the large run. decompose at N = 10^6 took 1.2 s and the whole script 3.1 s; the FFT is N log N, so 10^7 was priced at about 15 to 20 s for the decomposition plus the…
2026-09-10. Reuses probe.py's FFT-autocorrelation route for \ unchanged, and the character/sieve helpers in artifacts/siegel_uniformity/check.py for \.
2026-09-10. Builds on CANDIDATE_ENERGY.md, CORRECTED_RH_BRIDGE.md, LOCALIZED_MIXED_ENERGY.md and ENDPOINT_BOUND.md as they stand on this branch.
Frontier correction, 2026-09-12. The negative conclusion of section 1.2 is withdrawn. Its AP-variance calculation omitted the centered principal character, undercounted induced characters…
2026-09-12, attempt a-0082. Two scripts written fresh for this review, not reusing sharp_exponent_probe.py: review_a0082_sharp_exponent_check.py (numerical checks of section 5's two items…
2026-09-09. Base: 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. The completed attempts in PRs #209-#211 are unchanged.
Base: zeta-lab commit 3b0fc2e3c97b46cc1fde6af0ff3dd856898d95fb. Date: 2026-09-12. Handwritten derivations for independent review; no novelty claim.
delta_sq_sw_bind.py evaluates Section 7's proved statement \^2\ll_H N^3L^{-2H}\) (\(L=\log N\)) under an explicit, labeled convention -- assumed implied constant \ -- because the proof…
This checks one specific question: can the Siegel-Walfisz major-arc argument of UPPER_BOUND.md Section 5, equations — proved uniformly for denominators \(q\le Q'=\lfloor L^B\rfloor\), any…
This is a derivation check on a polylog-sized range of denominators, not a proof attempt and not a claim about RH.
Scope correction, 2026-09-12. The proposed absolutely convergent zero expansion in section 3 is not established: its coefficient \ decays as \, not its square.
2026-09-06. This attempt obtains \ E\ll_C N^3(\log N)^{-C}\qquad\text{for every fixed }C>0, \tag{1} \ unconditionally, for all sufficiently large integer \, with ineffective constants.
2026-09-06. This is an attempted proof mechanism, its failure analysis, and a constructive stress test.
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06. Status: mathematical proof draft with executed finite/symbolic checks. No independent referee review, formal verification, novelty claim, or improved bound on total E is…
This file records the complete research lineage that led to the frontier drafts in this directory.
This directory preserves the frontier work produced during the 2026-09-06 continuation of hunts/prime_pair_error before the next agent phase.
Date: 2026-09-06. Status: self-contained written proof draft, with an executed finite checker. No independent referee, novelty claim, formal verification, or improvement to the total…
Continuation of the 2026-09-06 factorial-certificate investigation.
Snapshot ID zeta-adaptive-freeze-v1. This directory is storage. Thomas paused the research and asked for the evidence to be preserved; nothing here was reviewed, promoted or extended by the…
Thomas has paused the research. Finish one clean repository checkpoint, then stop. Do not resume mathematical exploration in this task.
Snapshot ID: zeta-adaptive-freeze-v1 Research lineage: continuation of the 2026-09-06 Zeta Lab investigation.
A preservation checkpoint through the adaptive 23-correction block. Read FREEZE.md for the detailed claim/status ledger and the exact unresolved question.
Session 2026-09-07. Companion to RESULTS.md. Everything in Sections 1 and 2 is proved (elementary, finite, checkable by barrier_lemmas.py and tests/test_certificate_lp_barrier.py).
Session 2026-09-07 . Input: main 880ec07. Scope: the attainable-quotient problem T of hunts/quotient_certificate/RESULTS.md (PR #203), kept separate from the all-cell problem V.
Question. For support bound y and cutoff N, what is the smallest excess B - psi any factorial certificate can have?
Correction and continuation, 2026-09-07: Section 4.2's dimension-count argument is false: N=27,y=9 has eight constrained cells but minimum excess log, by an exact row relation and attaining…
All on the operator's laptop (16 GB M4) under a foreign load average of 60 to 140 from another session's agent fleet, so wall times are inflated several-fold.
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Reviewer: a Claude Code session working from the repository, not the session that produced the package.
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06. Status: elementary deduction plus two computed seed instances, checked by exact integer arithmetic and rational logarithm enclosures.
Snapshot date: 2026-09-06. Purpose: preserve and document the existing record, not begin another mathematical pass.
2026-09-06. Preservation only; no new mathematical result or agent run.
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06. Status: elementary deduction plus two computed seed instances, checked by exact integer arithmetic and rational logarithm enclosures.
Date: 2026-09-06. Executed in this chat. Not committed to Zeta Lab.
Reviewed 2026-09-06, in a fresh worktree, by a session that did not write the pilot.
Comparison, 2026-09-06, the third objective on the pilot's seed family. It is separate from ../factorial_full_cost/, whose record and conclusions are left unchanged, and from the preserved…
Experiment, 2026-09-06, a follow-up to the preserved pilot in ../factorial_certificate_pilot/ (read PILOT.md, pilot.py and REVIEW.md there first).
Date: 2026-09-06.
Date: 2026-09-06. Reviewer: a Claude Code session working from the repository, not the session that produced the candidate.
Date: 2026-09-06 (local investigation date).
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06.
Date: 2026-09-06, local conversation date. A continuation of the saved joint-support analysis.
Status: drafted 2026-08-16, not posted. Posting is an operator action; this hunt may not open issues on its own behalf, and this file is the artifact, not the act.
Opened 2026-08-16. Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
DRAFT. Nothing in this file has been posted. Posting to OEIS is an operator action, explicitly outside this hunt's permissions (MISSION.md, agents_may_not).
Written 2026-08-16, after an adjudication that the prior art owns the core of this hunt. The verdict is settled and this file does not relitigate it.
Run of 2026-08-16. Instruments: decide.py and theorem_inputs.py (decided constants), controls.py , witness.py ; raw numbers in decided.json, theorem_inputs.json, controls_results.json…
This file pins the texts the hunt attacks and the literature it leans on, so that every later step works against the served words rather than a paraphrase.
Hunt: prime_zeta_rightmost. Written 2026-08-16. This file states and proves the replacement for the two conjectures in OEIS A107311, against the verbatim text pinned in SOURCE.md section 2.
Continuation of PR #207 from 02e6780. The consumed definition is Fable's PR #208, Section 8 and fold_family.py at f4ae24f027f07916037ca8fe6c56c95a29cbf4d7.
Continue PR #207 from 02e6780d6c81e91d5151f93a89fb14ec13664cca. Consume Fable's latest fold definition from PR #208 at f4ae24f027f07916037ca8fe6c56c95a29cbf4d7, especially Section 8 and…
Continuation of PR #207 from d79fe15. The other lane's current input is PR #208, Section 9 at 0eb39186334612b3e55db315758c49ab87a29763, including Rule C and its reported failure at cell 33.
Continue PR #207 from d79fe15ae0feabf0f0529332526e1812e16e0312. Consume Rule C in Fable's PR #208 at 0eb39186334612b3e55db315758c49ab87a29763 without editing its files.
Input: 880ec07ae605d93f4c49e4464d8b4526457cfb65. This is a continuation after #203, #205 and #206, preserving their artifacts and corrections.
Input: main 880ec07ae605d93f4c49e4464d8b4526457cfb65, after PRs
Continuation of PR #207 from cce45bd. The rational upper certificate is supplied by the coordinator and recorded in fold_upper_input.json.
Continue PR #207 from cce45bd2bb3a9c1715ef2d4ad6269481dda5ed42. Input comparison: Fable's PR #208 at a343fed9b396bfa32b7f415576842e8c051458b5. Leave both PRs open.
Continuation of PR #207 from 3099c7a. The consumed input from Fable's PR #208 is pinned at 600ff8044ed9f5e30b9dd9ddc5f488faf1af329a. Both PRs remain open.
Continue PR #207 from 3099c7ac01eeeb1542bf40478fd73d1d58e794d3. The coordinator selected the class with N>=10000, y=floor, coverage on every Q_N cell and B_c<=2N.
Continue the factorial-certificate investigation from main d393e1a. The previous LP imposes positivity at every integer cell through N, although its prime sum evaluates the certificate only…
2026-09-07. Three finite ceilings improve after dropping constraints at unattainable cells. Rational coefficients satisfy every retained constraint in exact integer arithmetic.
Input baseline: main d393e1a, GitHub Actions tests run 34088036566 and checks run 34088036541 both passed.
Continuation of PR #207 from 45b3d9b. The construction consumed here is Fable's PR #208, Section 6, pinned at 3d8aa03034d5207cdab3129eb78534c0f77d2384.
Continue PR #207 from 45b3d9b2625dcf7695a7fbc811e3e2678af6fb27. The height-kernel assignment is complete; do not minimize variance.
Two runs. Run 1 (16585a2a-04a0-4eda-925f-1a79df23d758, branch hunt/r-0339c1, budget 60 minutes) proved the Chebyshev half and the double-counting first step, and named the wall: Mathlib has…
Outcome: settled. The Hardy–Ramanujan theorem is proved, kernel-checked with zero sorrys: ZetaLean.HardyRamanujan.hardy_ramanujan establishes the density form of Turán's argument, with…
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…
The previous census proved that the choices of one supported monochromatic perfect matching in each of three colours fall into 31 orbits. That does not quotient the full polynomial system.
Status: exact support census settled; algebraic sieve open. No 8x3 branch has been closed and no complex witness has been found.
id: r_044dd2-pilot hunt: r_044dd2 started: 2026-08-22T00:15:38-05:00 finished: 2026-08-22T00:18:35-05:00 ran: - orbit 0 with repeated bounded support minimization and 48 lazy cuts per round…
harness.review.standing_reasons returns, for the claim urms2-0.51 in harness/departments/review_ledger.py:
Outcome: the attack ran, the claim is not withdrawn, and it found three things about the record that a reader leaning on this claim should know.
Second instance of the reproduction procedure outside mathematics, paired with issue #140 (soundcalc / zkVM).
Read 2026-08-24. SWE-bench/experiments pinned at commit 1faa91cade0562ba62b66c1c99e71f7b72d96f13; split ids from princeton-nlp/SWE-bench_Verified at dataset sha…
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH .
lean/ZetaLean/HardyRamanujantheorem.lean landed the Hardy–Ramanujan theorem in its density form, with zero sorrys, on top of ZetaLean.Mertens.mertens_second_theorem.
Status: settled. Both threads closed, zero sorrys, axioms unchanged, no statement weakened.
Question. hunts/frontier_math/o9_leaf.py states a LEAF CAVEAT: its transcendental leaves come from Arb at 300 bits rounded outward with a 4-ulp pad, BandCert/Leaves.lean builds them from…
Settled. Issue #23's claim holds, and the outstanding item it named now has a number. o9_leaf.py's LEAF CAVEAT is false as a safety argument, its 344 is low by 38%, and the corrected 1-D…
harness/departments/guard_ledger.py records the guard scripts/make_context.py --check with the known miss:
Question. Does scripts/make_context.py --check detect public functions added under meta/, and what is the exact boundary of this blind region?
DeepMind's alphaevolve_repository_of_problems marks Problem 42 (the sum-difference problem) world_record in status.json.
Verdict: option 1 of the three the brief names. Penman and Wells reach a strictly higher value of exactly the quantity DeepMind's Problem 42 defines, and they do it with an explicit finite…
Two directories in this laboratory carry a table of the same quantity and disagree from i = 2 onward, with conflicting diagnoses of why:
Verdict: settled. An independent recomputation, written for this adjudication and importing neither disputant, reproduces hunts/higher_xi/C2_EXACT.json exactly at all eleven indices, and…
CONTINUATION of R-322DAE Source: operator Reference: prize:krenn-gu:n8-d3-orbit-reduced-system
The 6x3 system was evaluated on the 8-variable H x S2 quotient. Groebner basis completed in 0.44s and returned 1, confirming the no-complex-witness verdict.
The 3000 euro Krenn-Gu conjecture asks whether there exists an edge-weighted graph whose monochromatic matching polynomial satisfies specific quantum interference conditions.
This hunt settles the orbit-census layer for the Krenn-Gu 8x3 instance ($n=8$ vertices, $d=3$ colors).
tests/test_hunt_probe_discipline.py::test_no_hunt_claims_the_reserved_word is the lexical guard that scans hunts/ to ensure probe files do not claim the certainty regime reserved for…
Status: settled. The guard tests/test_hunt_probe_discipline.py::test_no_hunt_claims_the_reserved_word enforces an explicit suffix whitelist: path.suffix.lower() in {".py", ".md", ".json"}.
Mathlib's wanted-theorems tracking records Mertens's theorems (Wikidata Q1196729) as wanted and unbuilt.
Continuation run 05c755d3-1e75-4596-98b3-34ca2c084175, building on run ed50af7f (Hunt #30), which landed the first theorem and route-mapped the second.
One new file, lean/ZetaLean/Mertensstheorems.lean (409 lines), plus its import line in lean/ZetaLean.lean.
hunts/frontier_math/k2_closure.py::zone_trade maximises, over integer zone multiplicities with sum m <= 10, the adversary's zone trade
2026-08-17. Hunt r_401bbf, run 2b9b08aa. Instrument: probe.py, data: results.json, pins: test_prune_discharge.py. Reads: hunts/frontier_math/k2_closure.py, hunts/r_a97060/RESULTS.md §4.
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?
Source: teal-sea/zeta-lab issue #140. Started 2026-08-24.
Read 2026-08-24. ethereum/soundcalc pinned at commit d9078d64c9c3ae15b0931f6d249b2dc073194f15 . Vendor sources read at the commits and tags the TOMLs name, and again at each vendor's…
ZetaLean.HardyRamanujan.sum_sq_dev_le carries Turan's variance bound with the explicit constant 5855.
Settled. The variance constant moved from 5855 to 275, a factor of 21.3, with every statement's shape preserved, no hypothesis added, no sorry, and a green lake build.
Date: 2026-08-22
Target repo: teal-sea/zeta-lab · Branch: hunt/r-662b12 Source: operator · Reference: prize:aimo-interpretability-2026:baseline Task ID: 31e8a4f2-2c99-4bb6-953c-63f332cc07c4
Target repo: teal-sea/zeta-lab · Branch: hunt/r-662b12 Task reference: prize:aimo-interpretability-2026:baseline Telemetry Run ID: 31e8a4f2-2c99-4bb6-953c-63f332cc07c4
Run 4df2ee65-1c9a-4e3b-8f7d-2a6b9c4e0f11, branch hunt/r-6c7d6a-4df2ee65, budget 75 minutes, no operator supervision.
Run 4df2ee65-1c9a-4e3b-8f7d-2a6b9c4e0f11, 2026-08-17. Target: the numerator-side boxParts fields of the O9 two-dimensional checker, in hunts/frontier_math/zeta23ext/Zeta23Ext/EForm3/.
Run bc87fba6-95d1-4ce0-a9ef-c7e364c95bcb, branch hunt/r-6f088d-bc87fba6, budget 30 minutes, no operator supervision.
Run bc87fba6-95d1-4ce0-a9ef-c7e364c95bcb, 2026-08-18. Hunt #49.
Fourth instance of the lab's ceiling procedure (issue #110: reproduce a published certificate, read its verifier for soundness, measure where the method's own ceiling is, then push the…
Everything below is float grade (rung 1, "measured"). No interval arithmetic is used anywhere in probe.py, so no statement here climbs past measured except where it reproduces a value that…
harness/departments/guard_ledger.py records the guard scripts/make_context.py --check with the known miss:
Question. Does scripts/make_context.py --check detect in-place length-neutral private helper renames in modules with all, and what is the exact boundary?
Fifth instance of the ceiling procedure: convex-program certificates for Erdos's minimum overlap problem. Opened from issue #111, run 2026-08-23, budget 30 minutes, no operator supervision.
Fifth instance of the ceiling procedure: convex-program certificates for Erdos's minimum overlap problem (issue #111. Run f0bbb14a-833d-456a-befa-2e4f74ba6947, 2026-08-23, budget 30 minutes.
DeepMind's AlphaEvolve mathematics report claims C_3 <= 1.4557 for the "third autocorrelation inequality", improving a prior 1.4581.
Run 9698c990-e812-4890-94d8-f30a65b820af, 2026-08-23. Issue teal-sea/zeta-lab#123. Reproduce with python3 hunts/r_8539dc/probe.py (standard library only).
Run: 40c2efbc-2ed1-4de3-a762-fc57524791f6 · Case log: Hunt #47
Both halves landed, zero sorrys, standard axioms only. The two dead-weight seam lemmas are retired at no reproof cost, and the two-mode arithmetic is proved and instantiated at a recorded…
This is a mapping run, not a proving run. It buys coordinates. It does not attempt Erdős–Kac and it must not: starting to prove the theorem is a declared kill condition, not a stretch goal.
Status: settled. Both routes are mapped, both are priced, and they are not close. The moment method is roughly 2,400 to 3,700 lines of Lean and every one of its obligations is a thing…
docs/25 §4.3 defect 2 and commit 44d3133 record the same defect from two sides. The rung-3 grid sites carry a pred_beta drawn from mpmath point evaluations at the achievable bound, so the…
Status: settled, with one prediction in docs/25 refuted.
Run bbe76b9a-ccf3-4d53-bfe9-6480334f4648, opened 2026-08-17.
Run bbe76b9a-ccf3-4d53-bfe9-6480334f4648, 2026-08-17. Hunt #44.
hunts/frontier_math/K2-TWO-SPECIES.md section 2 records a depth-extended landscape table whose last row is starred as a correction:
2026-08-23. Run e09a7f8a. Reads: hunts/frontier_math/K2-TWO-SPECIES.md section 2, two_species.py, Zeta23Ext/EForm3/FarField.lean, Zeta23Ext/EForm3/Counting.lean.
hunts/frontier_math/k2_closure.py closes the k = 2, equal-depth case of blocker 2 over 6600 tau-cells on 0,132, and closes it at measured grade: every supremum in that table is a…
2026-08-17. Hunt r_a97060, run 78b4ce8e. Instrument: probe.py (+ ball_field.py), data: results.json. Reads: K2-TWO-SPECIES.md §3 and §6, hunts/frontier_math/k2_closure.py.
Opened 2026-08-18.
The question investigated is whether the first positivity failure of the Connes–van Suijlekom / Connes–Consani–Moscovici Galerkin truncation of the Weil quadratic form on the…
Run 37fb06a9-44a6-42d5-abc3-4c1342b1287b, 2026-08-18. Reads hunts/frontier_math/K2-TWO-SPECIES.md (section 5, the T1/T2 split), hunts/frontier_math/two_species.py…
Hunt r_b9552d, run 37fb06a9-44a6-42d5-abc3-4c1342b1287b, 2026-08-18. Instrument: probe.py (runs end to end in ~6 minutes; --quick in ~10 s). Data: results.json.
Hunt r_b9552d, run 2, run id 113786a8-1f1c-4220-b772-15160a0274fa, 2026-08-20. Instrument: probe.py (--quick in seconds, full in a few minutes). Data: results.json (and results_quick.json).
harness/departments/guard_ledger.py records the guard scripts/make_context.py --check with the known miss:
Status: settled. The guard scripts/make_context.py --check does not detect test files whose names do not match test.py (such as tests/mutant_helper.py, tests/conftest.py, or…
harness/departments/guard_ledger.py records the guard tests/test_docs_numbering.py::test_no_two_docs_share_a_number with the known miss:
Status: settled. The guard tests/test_docs_numbering.py::test_no_two_docs_share_a_number does not detect a document renamed without its number changing when citations use bare references…
Run 872d7dce-5f49-4e7c-8fcf-f470fd066e6f, opened 2026-08-24. Parent: hunts/r_b9552d run 37fb06a9 (RESULTS-37fb06a9.md §5, loose thread 2), which recorded the route as assessed and not…
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.
Question. Does scripts/make_context.py --check detect public functions, classes, constants, or module additions under compiler/, and what is the exact sensitivity boundary?
Question. Does scripts/make_context.py --check detect public functions, classes, constants, or module additions under compiler/, and what is the exact sensitivity boundary?
A standing limitation on every claim compiler/ makes. Recording it publicly because it bounds what those verdicts mean.
This hunt establishes, measures, and records the exact scope caveats bounding all claims made by the compiler/ department.
claude/riemann-hypothesis-research-ofds8s ran a wide-portfolio RH-adjacent campaign on 2026-08-17/18 and never landed.
Status: settled. Four arms landed, one held back on purpose, 29/29 acceptance checks pass, and one real defect was found in the material while checking it.
Publishes the artifact queued by issue #21: a partial computation established that three commonly-cited structural properties of ζ are satisfied by every RH-violating look-alike in…
Status: settled for the five properties issue #21 queued; the sixth was already settled by earlier hunts in this tree, and what this run adds to it is the number that says why it is…
claim 'urms2-0.51' has no recorded blind attack: the review is not standing until one runs
What modification of the world would preserve the appearance of this result while making its interpretation false?
Test AGY conversation context and handback 8.
Status: settled.
Assembled 2026-08-17 by eleven parallel literature surveys; each entry carries the URL its statement was checked against, or is marked memory-unverified.
Scores are the surveying arm's (importance, novelty probability, tractability, verifiability, computational leverage, each /10; sat = literature saturation, high is bad).
This hunt was worked on claude/riemann-hypothesis-research-ofds8s between 2026-08-17 and 2026-08-18 and never landed. Hunt R-F00E48 landed part of it.
Opened 2026-08-17 on branch claude/riemann-hypothesis-research-ofds8s.
All commands run from the repo root with the project venv . The Arb backend must be live: .venv/bin/python -c "from zeta import rigor; print" should print python-flint.
Sub-study of hunts/rogue_frontier/. Opened 2026-08-18.
Running log. Appended as things happen, because a session can be killed at any moment and a result held only in a chat window is a result that is lost.
Opened 2026-08-18. A scope extension of rogue_frontier, recorded here rather than assumed: the campaign's HuntSpec question is about the RH-adjacent frontier, and this sub-study is not…
Sub-study of hunt #38 (hunts/rogue_frontier/MISSION.md carries the governing HuntSpec). Opened 2026-08-17.
Session of 2026-08-17. Grade: measured, with enclosure-checked arithmetic (every headline d_N^2 is an arb ball that rigorously contains the exact value of the stated finite-dimensional…
Every formula this study implements was read in at least one primary source during the session of 2026-08-17; the two load-bearing statements (Vasyunin's formula, the BCF asymptotic) were…
Status: ACTIVE. Opened 2026-08-17. Nothing here is a result until it survives the campaign's destruction stages; grades follow the repository ladder.
Status: probe output of the sine_gram hunt. Everything below is a statement about the CUE band-Gram model at band ratio lambda = d/N (equivalently, in the limit, the sine process of unit…
A sub-study of hunts/rogue_frontier/ (its MISSION.md and HuntSpec govern here). Opened 2026-08-17.
Study of 2026-08-17, hunts/rogue_frontier/weil_trunc/. Sources, exact construction and claim inventory: SOURCE.md.
Step-0 verification record, written before any implementation. All PDFs were fetched 2026-08-17 and read; page/equation citations below are from those copies (stored in the session…
Goal: first (c, N) where the DH truncated Weil form acquires a negative eigenvalue, enclosure-checked, with zeta control and localization evidence.
Exploratory study under hunts/rogue_frontier/. Per hunts/README.md, nothing here is a promoted result; every number below carries its rung on the repo's certainty ladder, stated inline and…
Session scratch log, updated incrementally. Nothing here is a result until it reaches RESULTS.md section 9 with a grade.
Bounded question, set by the parent run 0897a5a7 / Hunt #91 : reconstruct the Erdős–Turán 1934 proof in modern notation, isolate every place the factor 2 per prime is lost, and test whether…
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Support run 5418c63e, 2026-08-24, for run 872d7dce . Instrument: probe_arm_b.py (runs end to end in ~7 s; --quick in <1 s). Data: results.json. Nothing here bears on RH .
Support run for 0897a5a7, answering one bounded question for a live parent: improve the hunts/r_186989 computation so that it ranges over choices of $S$ instead of freezing the first $k$…
Hunt, not a result. Nothing here is evidence for or against RH .
Support run 78c499b4-bc7d-4e1a-9efa-47571547b826, 2026-08-24. Serving run 872d7dce (hunt r_c7f779), which asked one bounded literature question and is still alive to receive the answer.
Support run 78c499b4, 2026-08-24, for run 872d7dce . This is the prior-art page the brief called arm_e/PRIOR-ART.md.
Support run for 0897a5a7 / hunts/r_186989. One bounded question:
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing here is a result, and nothing here bears on RH .
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH .
Support arm for run 0897a5a7. Bounded question, one lane:
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH . Support run for 0897a5a7. Arm label: sunit-equations.
A support run, not an open hunt. Another run asked one bounded question and is waiting on the answer, so this directory records the answer and the evidence behind it, and then it is closed.
The answer: yes. At dps=60,
What this is. An adversarial audit of hunts/r_186989/RESULTS.md (Erdős Problem #126, Hunt #91). Every claim in that file was treated as hostile input: re-proved, re-computed independently…
Hunt, not a result. Nothing here is evidence for or against RH .
Support run for 0897a5a7. Bounded question: ignore the three lanes of the earlier brief, design a proof program for Erdős #126 (log g = o from the statement and the original theorem, rank…
Hunt, not a result. Nothing here is evidence for or against RH .
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: exact-rational evidence package for independent review. This file strengthens the ambient variational result in RESULTS-xiprime-global-optimality.md.
Snapshot: 8b10ede734258e9e966f6b889176d81a4d59964d Verdict: Outcome A. The full Hilbert-space window optimization is a coercive quadratic minimization, and its unique optimizing ray has a…
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.
Hunt #75 closed the note-to-colour question and, in its aftermath, the operator asked for something bolder.
The reading path, derived line by line. Laid out in order on the reading page; listed here for completeness.
Zeta Lab is a computational and formal workbench for studying the Riemann zeta function, attempting original mathematics toward the Riemann Hypothesis , and establishing useful intermediate…
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.
The mathematical tools in this repository have proved many useful statements. Their current estimates do not by themselves establish RH.
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.
Disposition of the cheapest informative slice of meta/asymmetry-experiment.md. Run 2026-08-20, four checkers. Grade: measured, one run each.
Hunt #61 produced, so far as the literature search recorded in hunts/lambda_dh_bounds/NOVELTY.md reaches, the first quantitative bounds, from either side, on the de Bruijn-Newman constant…
A reading-course page about a threshold this laboratory did not discover. The threshold that governs the rightmost zeros of the prime zeta function is not this laboratory's result: it is…
Hunt #65 adjudicated two contradicting kappa = 2 tables in this repository and, in doing so, located the error that produced the disagreement. It is not in either table's code.
21 August 2026. On 18 August 2026 the Lean FRO and ICARM opened Palomar, a registry of Lean-verified mathematics, described by its own documentation as the analogue of a preprint server for…
Hunt #75 . Verdict: PRETTY BUT TRIVIAL for the note-to-hue question; the reformulation in section 9 is the one worth keeping.
Hunt #76 . Verdict: INTERESTING STRUCTURE, classical in substance. Measured in steps-per-octave, the Riemann zeros avoid the equal temperaments that tune prime-power harmonics and ignore…
Hunt #110, hunts/outband_intake/. Read hunts/outband_intake/RESULTS.md for the measurements and the doors.
Moved off the front page on 2026-09-05. README.md is an index, and AGENTS.md says so in as many words: "Keep README.md an index, not a manual.
This is the cross-hunt index of method. hunts/README.md logs each hunt by outcome; nothing there says which trick a later hunt could pick up. This file does.
Thirty-eight numbered documents. The first five are a single argument and are meant to be read in order; everything after 14 is a record of a particular piece of work and can be read on its…
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.
This door is for people who want to clone Zeta Lab, run their own agents against a bounded question and return the result as a pull request.
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 added…
For you if you want to generate leads automatically, and, more usefully, to see what fraction of them survive.
For you if you want to see an LLM work against deterministic mathematical checks instead of an LLM judge.
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 you…
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.
How an outsider gets into this tree, and the reports that attack its own results: the red-team pass and the null controls. The standing rules a worker reads first were on this shelf until they were cut from the site; they are still in the repository.
Zeta Lab accepts agent-assisted contributions. Clone the repository, let your tools investigate a bounded question, and open a pull request with the evidence.
Date: 2026-09-03 Box: orca-agent-box (user thomaslincez) Status: All work committed, pushed to GitHub across all repositories, and PRs merged. Safe to power off VM.
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).
hunts/ainta_seven_point/lean-four-point requires Zeta23Bridge by path . Lake exposes every lean_lib of a required package to import resolution.
How the pieces are built and why, plus the annotated reading list and the records the other pages cite.
Ostoyae boards for this repository's hunts. A board is an execution plan: which work items a run may attempt, their checks, and the append-only record of every attempt made against them.
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…
Expose a small, reproducible RL/evaluation environment from Hunt #80 without publishing private operating material.
A model gets read-only access to Frank Wikström's published Bloch certificate verifier. It must reproduce two archived certificate values, reproduce the published near-branch target, and…
At runtime this package downloads Frank Wikström's public Zenodo archive, bloch-computations-1.0.0.zip, record 10.5281/zenodo.21975862, and refuses to execute it unless its SHA-256 is…
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.
Everything under history/ is archival evidence of what the laboratory previously wrote, attempted, measured, or believed. It is not an instruction layer and it is not a current frontier map.
These files are byte-for-byte copies from zeta-lab commit 4cb2230b0ba9f2e73121d0794ae81e08da84d3f5, before the owner's 2026-09-12 clarification of the research mandate.
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…
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 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…
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.
Surveyed 2026-08-31 against the Mathlib checked out at lean/.lake/packages/mathlib, pin v4.33.0-rc2 (lean/lake-manifest.json, toolchain leanprover/lean4:v4.33.0-rc2).
Problem. For r >= 3, must every r-colouring of the edges of K{r^2+1} contain r+1 vertices whose induced K{r+1} is missing a colour? Proved for r = 3, 4 (Erdős–Gyárfás 1999).
Target: hardyZ Status: Ready to draft Lean code Workspace: lean/ZetaLean/ Target Host: leanprover-community/mathlib4
Palomar is a registry of Lean-verified mathematics, incubated by the Lean FRO and ICARM and opened for submissions on 2026-08-18.
To set up your new GitHub repository, follow these steps:
Lean 4 declarations this laboratory formalized because it needed them, kept here rather than sent upstream.
Toolchain leanprover/lean4:v4.33.0-rc2, Mathlib v4.33.0-rc2 .
audit-v2-frozen.log in this directory is the #print axioms output for the Palomar V2 surface, committed so that the claim does not rest on a log that expires.
Ainta's simple-zero argument, assembled in Lean 4 as a theorem about Mathlib's riemannZeta and generalized to n points.
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/…
Mathlib keeps docs/1000.yaml: the Wikipedia list of famous theorems, each entry tagged with the Lean declaration that proves it.
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.