A computational laboratory for the Riemann zeta function and RH. Read README.md for the front door and docs/00-orientation.md for scope.
ROADMAP.md carries the project's decisions, deliberate non-goals, known gaps and the next planned build — read it before proposing or planning work.
This file is the single source of operating context for any coding agent working in this repository (Claude Code, Codex, Cursor, Aider, …). CLAUDE.md is a pointer to this file; do not duplicate content between them.
Setup (first run in a fresh clone)
python3 -m venv .venv
.venv/bin/pip install -r requirements.txt
.venv/bin/pip install -e .
.venv/bin/python -m pytest -q -m "not slow" # confirm green before changing anythingCheck the ball-arithmetic backend before you trust a green run:
.venv/bin/python -c "from zeta import rigor; print(rigor.BACKEND, rigor.available_backends())"
# want: python-flint ['mpmath.iv', 'python-flint']If python-flint is missing, rigor.py silently falls back to mpmath's iv context. That is by design and the fallback is correct — but it is roughly 1600× slower on the certified paths (one test_rigor.py case goes from 0.76 s to over twenty minutes, which reads as a hung fast tier, not a slow one), and the five skipif(not HAVE_FLINT) tests silently disappear. Three of those say "needs both backends installed": they are the Arb-vs-mpmath cross-check that is the whole reason rigor.py may claim the word certified. A suite that reports "5 skipped" here is not exercising that cross-check, so a fresh clone should install python-flint (it is pinned in requirements.txt) rather than treat the skips as normal.
The knowledge index
CONTEXT.md is a generated index of the public API, the document list, the script list and test counts — the facts. This file carries the judgment. Regenerate the facts rather than editing them:
.venv/bin/python scripts/make_context.py # rewrite CONTEXT.md
.venv/bin/python scripts/make_context.py --check # non-zero exit if stale
.venv/bin/python scripts/make_context.py --flat # + CONTEXT_FLAT.md, whole repo in one fileRegenerate it whenever you add or rename a public function, a doc or a script. llms.txt is the short curated map for tools that look for one.
Multiple agents / parallel sessions
Several agents or sessions may work this repository in parallel, on branches or worktrees. To prevent scope creep and collisions:
- Repo-wide rules: this file. Per-area scope: an active branch, worktree, or exploratory directory (e.g. under
hunts/) carries aMISSION.mdstating what that work is and is not allowed to touch — read it before acting there. - Namespacing: keep exploratory math out of
zeta/(core) andontology/(domain-agnostic); new exploratory work goes in its own subdirectory underhunts/. - Handoffs: communicate through the
conjectures/ledger rather than editing shared core files simultaneously. - Worktrees: avoid literally simultaneous runs against the same checkout; for parallel work use
git worktree addso each agent gets its own tree. - Verify first: confirm the suite is green (see Setup) before building on a tree.
Outside environments (read-only mounts, notebook agents)
Some sessions run this laboratory from an environment that is not this checkout: a notebook-style agent (Claude Science and anything like it) that mounts the repository read-only and brings its own Python. That suits the exploratory half of this tree — cells, background execution and interruption fit expensive mpmath work — but it breaks two assumptions the rest of this file is entitled to make, and both break silently.
Run the preflight as the first cell, before any mathematics:
python scripts/science_preflight.py # or --allow-fallbackIt reports the interpreter and dependency set, plus three things no outside session can infer from a snapshot: whether rigor.BACKEND is really Arb (a missing python-flint degrades to mpmath's iv — correct, ~1600× slower, and it removes the cross-check that is the only reason rigor.py may use the reserved word), whether a Lean build is possible at all, and the next free docs/ number. It exits non-zero when the environment cannot support the claims this tree knows how to make.
The standing rules for such a session:
- Guess no number and no name. Take the next free doc number from the preflight. Two documents once shared number 21 because a session working from a snapshot could not see the tree it was writing into;
tests/test_docs_numbering.pynow catches that, but only if you run it. - An artifact is not a commit. Say plainly that files were produced and not landed, and never describe a read-only tree as changed. Workspace storage is swept after idle gaps; the artifact is the durable copy until someone commits it.
- Write only where a hunt may write:
hunts/<name>/with itsMISSION.mdwritten first, one newdocs/NN-*.md, andfigures/. Notzeta/,ontology/orharness/without explicit permission. - The lexical rules are lexical. The reserved word is banned everywhere under
hunts/including inside a sentence disclaiming it. Intent does not exempt a file; the test reads the bytes. - Before handing anything back, run at least
tests/test_docs_numbering.py,tests/test_hunt_probe_discipline.py,tests/test_doors.py, andscripts/make_context.py --check.
Where the operating material lives
This repository is the public research record: mathematics, tests, proofs, evidence, and enough method that an outside reader can evaluate or reproduce a claim. That is why it is public, and it is the standard for what belongs here.
How the laboratory is operated lives in a separate private repository: operator strategy, hunt briefs and their generation, the prompt corpus, session launching, telemetry economics, and any future routing or allocation logic. Those have no bearing on whether a scientific claim here is correct, so they are not published.
The boundary, applied with judgment rather than by a rule engine:
If an outside observer needs it to evaluate or reproduce a public claim, it belongs here. If it teaches the lab how to allocate, route, prompt, or operate itself, it belongs there unless reproducibility needs it.
Preregistrations and protocols stay here even when unflattering — the harness gate record (harness/VERDICT.md, harness/gate-evidence/) is public precisely because a negative result about our own tooling is credibility, not capability.
A private operating repository does not make the research process private: this tree stays unusually open about criticism, corrections and claims that did not survive. Ownership and visibility are separate questions from transparency, and only the last one is a promise this repository makes.
The shape, so a session launched into this tree knows which side it is on: teal-sea is the parent, the operating repository directs pursuits, and this repository is a pursuit. The research is yours to do and commit here. Two things are not: if you find an infrastructure idea, do not reach across and edit the operating repository, report it as a Core candidate. If you find an interesting loose end outside your mission, do not pursue it, report it as a thread. Zeta is a worker target, not the operator's console, and it must not grow into an operating database.
Flag genuinely ambiguous cases to the operator. Do not build a framework to adjudicate them.
How the work is organised
Two working ideas and one objective. None is settled; all three are here rather than in a strategy document because you should meet them while working.
Core ↔ Pursuits. Core is work that improves the lab's reusable ability to work: infrastructure, tooling, telemetry, agent coordination, reusable method. Pursuits are what the lab is chasing outward: research questions, hunts, investigations. They are not a hierarchy and not an ancestry — they create each other in both directions. A hunt that needs a tool produces Core; Core work that trips over a phenomenon produces a Pursuit; a piece of Core can itself become the subject of a Pursuit (harness/ did exactly that, and lost). The distinction describes a thing's current role, not its rank or its origin. Do not rename directories to make the tree look like the metaphor.
Forage, don't roadmap. Explore several directions cheaply; when one produces credible signal, feed it more; when it stops, stop feeding it. Preserve the threads you are not pulling, so choosing one direction does not require forgetting the others — observations become issues, leads go to the roster with the operator. This is a working strategy, not a proven optimal policy.
The economic objective: maximize valuable output per monetary unit of input. This is not "minimize tokens". Money is the input and valuable output is the objective; models, tokens, extra agents, verification, formalization, infrastructure and operator time are all allocation choices. A more expensive approach is the right one whenever the extra output justifies the cost — and a cheap approach that yields low-value or unreliable output is not efficient, it is just cheap. We do not yet have a complete metric for "valuable output". Do not invent one and treat it as settled; it is an open research question, not a KPI.
Design discipline, learned the expensive way. Before adding any abstraction, answer: what live thing in this repository will use this immediately? If the answer is "future agents might", do not build it. Prefer real need → smallest implementation → actual use → measurement → only then generalization. Do not build infrastructure without a live consumer, do not generalize a workflow before the concrete workflow earns it, and do not build a meta-system to manage the meta-system. harness/VERDICT.md is what the alternative cost.
Read that verdict as a bet properly made and properly ended, not as a blunder. It was a reasonable thing to try, it was built well, it was tested against the practice it meant to improve, and it lost. Being able to kill something you funded, on evidence, is the habit worth keeping — a lab that cannot do that has preferences rather than a method. Retiring it is a success of the process and a failure of the thing, and the two are not the same judgement.
Observations, and the work roster
Two different things that were once one file, split by what kind of statement they are rather than by where they lived.
An observation is public. Something measured, noticed, broken or bounded is a fact about the subject or about this tree, and it is true whether or not anyone pursues it. Those go in the open, as a GitHub issue on this repository, or as a doc and a test when they are big enough to deserve one. Issue #21 is a measured result about which properties of ζ discriminate; issue #22 is a scope caveat that bounds every claim compiler/ makes; issue #20 is a defect. All three are checkable by a stranger, which is the point.
A lead is private. That we intend to chase something, in what order, with what budget, lives in the operator's roster. A backlog announces what the lab is about to work on, which is allocation, and allocation is operating material.
The line: an issue says "this is true and unresolved." The roster says "this one is next."
If you notice something and are not chasing it now, open an issue — do not start a backlog file here. Record the observation; leave the priority to the roster.
scripts/70_lab_state.py still derives live work from git — every branch ahead of origin/main, right by construction, needing nobody to maintain it.
Hard rules
- Python: ALWAYS
.venv/bin/python (from the repo root)— never barepython3. All dependencies live only in that venv (mpmath, numpy, scipy, matplotlib, sympy, pytest). - matplotlib: headless. Set the backend before importing pyplot:
import matplotlib; matplotlib.use("Agg").zeta/plots.pyalready does this; scripts that plot must too. - Precision: mpmath for anything precision-critical, with
mp.dpsset explicitly (house style:mp.workdps(...)context managers, guard digits internal, no global mpmath state left modified). numpy only for bulk statistics. - Any mathematical claim added to code or docs must be numerically checked by a test, or explicitly hedged at the point of use. This is the repo's central habit: every number in a docstring is pinned by
tests/; identities are exposed as measured defect functions (functional_equation_defect,theta_modular_defect, ...), not assumed. - Honest-scope rule & Phase II Objective: Zeta Lab is a computational and formal workbench. Phase II's explicit Research Objective is to produce one externally verified mathematical statement that humanity didn't previously know (e.g. a new theorem, counterexample, bound, equivalence, or robust conjecture). However, it still makes no claims to advance RH itself. Nothing here is evidence for RH (Littlewood's theorem,
docs/08). Never write language implying a computation settles or supports RH; the sanctioned framing for the sign-change verification is "proof for the finite range, modulo the correctness of the floating-point sign evaluations". - Original is not novel, and the lab may claim original (director's ruling, 2026-08-13). These are two different claims and conflating them was costing the laboratory its own output:
- Original is a claim about provenance: this laboratory produced this result, rather than re-deriving a target it was handed. It is answerable from the record — the git history, the ledgers, the working paper — and it is claimable. Say "original result", name it, and give its rung.
- Novel is a claim about the world: no one has established this before. It is a much larger assertion than originality and it needs evidence of a search.
ontology/knownness.pydefaults to "the literature was not consulted" so that an unrun check can never read as absence of prior art. That default describes the tool, not the laboratory: where a search has actually been run, say what was searched and what it found. The frontier results are positioned against a cited source paper whose theorems are used as published, with the improvement stated as a delta against it, andreferences/papers.mdtracks the sources. Backends exist for OEIS, arXiv and zbMATH. Do not describe engaged prior art as unsearched; that understates the work as badly as claiming novelty overstates it.
A result is not downgraded to nothing because its novelty is unsearched. A kernel-checked statement this lab produced is an original kernel-checked result, full stop, and the front of the house should say so. The certainty ladder below still governs how strongly it may be phrased; the ladder grades confidence, it does not decide authorship. Refutations count as output too — a route closed with a witness is a result, not an absence of one.
- The certainty ladder (amended 2026-08-12; replaces the blunt "an apparent settlement is a bug" heuristic, which treated a kernel-checked proof and an eyeballed number alike). When a computation appears to settle something open, the correct FIRST inference is still a bug -- the
hunts/frontier_mathledger records nine defects in two days caught by exactly that reflex -- but the inference is discharged by climbing the ladder, and a claim may then carry the strongest language its rung has earned: - measured -- one route, float grade. Say "measured", "observed".
- hardened -- independent routes agree and/or ball-arithmetic enclosures carry every step (
rigor.pygrade). Say "hardened", "enclosure-carrying". - kernel-checked -- Lean 4 + Mathlib, zero sorrys, standard axioms only. These are theorems; call them theorems, without apology. The ladder ends here, because this is where our certification ends (director's ruling, 2026-08-13). Outside review is a real and necessary step and it is not ours to award: it depends on someone else stepping up. It was previously carried as a vacant fourth rung, which read as a standing deficiency in the work rather than as an open invitation. It is now a footnote instead -- a published claim carries pending external verification until a qualified outside reader has walked the chain, and that footnote is small because the work is done and the waiting is somebody else's. A composite claim takes the grade of its WEAKEST step: a chain of theorems glued by one measured step is a candidate and is called one. The reserved words stay reserved ("certified" to
zeta/rigor.pyand the Lean arm; thehunts/lexical bans unchanged -- tests enforce them). This rule licenses confidence at every rung a claim has earned; it does not license rounding a rung upward for an audience. - House style: no em dashes in prose you write. Use a period, a colon, or a pair of commas; an em dash almost always marks a clause that wanted to be its own sentence. This is a style rule, not a moral one, and it applies to text you author: docstrings, comments, documents, commit messages, generated pages. It does not license repunctuating quoted material — a ledger entry, a document blurb, an adversary's recorded findings — because editing someone's recorded words to satisfy a style rule is editing evidence. The site generator enforces exactly that split for the public pages, in the repository it now lives in: the em dash count on a rendered page may not exceed the count in the artifacts it quotes.
- Derive conventions, never remember them. Where the literature disagrees on factor placement or a constant, the repo calibrates numerically and cross-checks: the Riemann–Weil explicit-formula convention in
zeta/weil.pywas validated by computing both sides independently for four test functions from three unrelated families; κ inzeta/epstein.pyis re-derived by a linear solve on every call, with the pinned string only a test reference. Follow that pattern for any new formula with a contested normalization. - The Lean arm counts nothing with a
sorry.lean/is the second certainty regime: theorems kernel-checked by Lean 4 + Mathlib, built withcd lean && PATH="$HOME/.elan/bin:$PATH" lake build. Nothing there counts until it compiles with zerosorrys — asorryis an uncertified step, tracked in the file, never hidden. Lean proofs andrigor.pyenclosures are the only two things in the repo that may use the word "certified", and they are different regimes (kernel-checked symbolic truth vs enclosure-carrying numerics); say which one you mean. - "Certified" is a reserved word. Only
zeta/rigor.pymay claim it, and only for a quantity every step of whose computation carried an enclosure. A dict that reportscertified: Trueis asserting a theorem; if any step silently falls back to floats, that is a critical defect, not a rounding detail. The safe failure mode is mandatory:proven_signreturns0for "not decided", uncertifiable steps are named inuncertified_steps, andcertifiedis False whenever that list is non-empty. Everything else in the repo is accurate, which is a different and weaker claim — say which one you mean. Non-rigorous cross-checks (mpmathnzeros,backlunds) must stay flagged as such in the returned dict. - The counterexample battery is a standing test. Any claimed structural property that "explains" RH must be run through
zeta.epstein.battery(ζ and the Davenport–Heilbronn function behind one interface): f satisfies the functional equation, has real coefficients and a real Hardy-style Z, and violates RH — a claim f also passes distinguishes nothing (docs/09, gate #3; docs/08 §4.1).
Layout
- Package:
zeta/(flat layout, pip-installed editable —pip install -e .). core.pyζ/η/Euler–Maclaurin, Jacobi θ, ξ, Ξ, Hardy Z, Mellin, defects.zeros.pysign-change hunting, Gram points, N(T),verify_rh_up_to.explicit.pyexplicit formula (ψ, π from zeros), prime spectrum.statistics.pyvectorized Riemann–Siegel, unfolding, GUE comparisons.moments.pyexternal LMFDB/Odlyzko zero-table ingestion plus finite critical-line moment estimates and a theorem-gated prediction scorecard. It preserves high ordinates as decimal base-plus-offset data, requires separately sourced|ζ|samples, and never computes zeros.heatflow.pyΦ, H_t, zero tracking, de Bruijn–Newman Λ.weil.pyRiemann–Weil explicit formula (both sides independently), Weil functional W(h), positivity probes, truncation-tail accounting.epstein.pythe Davenport–Heilbronn counterexample: κ derivation, Z_dh, box-vs-line zero counts, the off-line zero,battery.rigor.pyball arithmetic:enclose_Z,proven_sign,certified_zero_count,verify_rh_certified. Two backends (Arb via python-flint, mpmath'siv); every public function takesbackend=so the two can check each other. Nothing is ever silently upgraded to a certificate — see below. The two-backend cross-check only runs when both are installed; confirm withrigor.available_backends()(see Setup) before reading a green suite as evidence that it did.li.pyLi's criterion (λ_n, two independent routes) and Jensen polynomials / hyperbolicity (numeric and exact Sturm in ℚ[X]).finitefield.pycurves over F_p — the RH that is a theorem: point counts, Frobenius eigenvalues, Lefschetz vs brute force in F_{p²}, Sato–Tate.criteria.pyfour equivalence faces: Mertens/Möbius, Baez-Duarte, Robin/Lagarias, Speiser.plots.pythe twenty figures.zeta/__init__.pyre-exports the curated API; plots are loaded lazily (PEP 562__getattr__) — keep it that way,import zetamust not pull in matplotlib.- Package:
ontology/— the conjecture factory (phase 4).schema.py,registry.py,ledger.py,funnel.py,metrics.pyandhistorical_cases.pyare domain-agnostic and must stay that way: they name no quantity the laboratory computes, and seam tests enforce it (an AST import scan, a subprocess that assertszetanever enterssys.modules, and a lexical scan for subject-matter vocabulary). Everything that knows the subject lives inontology/domains/. Readontology/README.mdbefore touching any of it.ontologyis not part of the editable install, so a script that imports it must put the repo root onsys.path(derived from__file__— seescripts/13_discovery_run.py). The numbered scripts alongside the core (01_f1_geometry.py…16_adelic_acoustic_absorber.py) are the rogue-lab prototypes: historical exploratory operator hunts, kept becausedocs/17dissects four of them as case studies andtests/test_rogue_lab_controls.pypins their control results. They are outside the domain-agnostic seam, and no new work should be added there — new exploration goes underhunts/. - Package:
harness/— two things, and only one of them is live. Readharness/VERDICT.mdbefore doing anything here. - Live, ordinary lab bookkeeping — keep, use, extend as needed. The ledgers and their readers:
graveyard.py(dead ends recorded so they are not re-entered),guards.py(guards recorded so they can be attacked),review.py,independence.py, and the three ledgers underdepartments/(graveyard_ledger,guard_ledger,review_ledger). Their live consumer isscripts/70_lab_state.py, the research-state view. ~1,050 lines, with a real reader. - Demoted, 2026-08-13 — do not extend. The generalized battery/department/integrity framework:
protocol.py,integrity.py,promotion.py,preregistration.py,provenance.py,shams.py, and the six subject packs underdepartments/that exist to populate it. ~8,000 lines with zero live consumers. It was tested and did not earn core status: four preregistered experiments, three subjects, 74 agent runs, the harness arm never once beat the control, the control was 37/37, and where correctness was identical the harness cost 1.1–1.7× the tokens and 2.4–5.0× the tool calls. Meanwhile live hunts reimplemented the same four control roles by hand rather than import them. The evidence is inharness/gate-evidence/; the negative result stands and is not to be quietly relitigated. - What survived the demotion, because it is independently true: the four control roles are still good research practice — a claim that a structure-matched rival also satisfies has distinguished nothing, and
zeta.epstein.batteryenforces exactly that for ζ without any of this framework.compiler/semantics.pyrecords a measured fact worth keeping: exhaustive concrete testing over all 65,536 i8 inputs cannot see poison-class defects, with a planted fault pinning it. Scope discipline — stating what a verdict does not cover — earned its keep and costs nothing. - The lesson generalizes and is the reason for the rule two sections down: an abstraction with no live consumer is a liability, however elegant.
- Package:
dossier/— an experiment, not a department. It represents mathematical research state (intent, definition, rejected alternatives, semantic obligations, evidence) so an agent can resume work. Two ideas under test: intent is data, and "verified" is four independent things —status.pykeepsnumeric/certified/literature/formalapart, offers no aggregate, andSupport.__bool__raises soif support:cannot silently collapse them. Same three seam tests asontology/schema.py; subject matter only indossier/subjects/. One worked example (Hardy Z), one CLI (scripts/50_dossier.py). Deliberately registered in no department: a dossier has no negative controls of its own, and a department whose battery belongs to another department is not a department (docs/19-research-dossiers.md§6). hunts/— exploratory studies, not departments and not results. The one place a claim may be recorded before any control has been run against it. A hunt cannot become a department by growing, for the same reasondossier/cannot. Readhunts/README.mdbefore adding one.- Package:
meta/— the second laboratory: evidence about the research system rather than about ζ.ledger.pyis the intervention ledger — what a human had to do that the machinery could not, with the missing capability named, because the quantity under test is legitimate research output per unit of scarce human judgment and that needs a denominator. It is domain-agnostic under the same seam tests asontology/schema.py, and it is built to be hard to flatter: no__bool__, no autonomy score, a ratio that refuses to divide until the caller names its numerator, and anautomatedclaim that costs a named artifact.suspicions()reports the shapes a self-validating log takes.asymmetry-experiment.mdis the pre-registered design for the independent-vs- co-designed verification question.operator-functions.mddecomposes what is left of the operator's role once the automatable friction is subtracted, into severity calibration, scope discipline, skepticism routing and authority — and reframes the target: you do not automate judgment, you measure calibration, which theJudgmentrecord does. Its load-bearing guard is that the system may not resolve a disagreement it is party to. Nothing here is a mathematical result and nothing here trades against one; a session with no mathematics and a tidy ledger produced nothing. Readmeta/README.mdfirst. - Project:
lean/— the certified arm: a Lean 4 + Mathlib package (ZetaLean) formalizing, rung by rung, facts the laboratory measures.ZetaLean/GroundTruth.leanis rung 1 (ζ(2), ζ(0), ζ(4), the zero-free half-plane); rung 3 (Davenport–Heilbronn) is mathematics-complete and waiting on compute — its interval layers areRigor/IntervalExp/IntervalCExp, the analysis isDHAnalytic/DHTailBound/DHZeroCriterion, andDHDemois the worked instance. Do not add asorryto any of them to "make progress"; the remaining gap is a computation, not a lemma. The ladder and the next rung live inHANDOFF.md. Toolchain is elan-managed and pinned bylean/lean-toolchain;.lake/build artifacts are gitignored. - Package:
compiler/— the subject matter of harness department #3 (LLVM IR rewrite verification):catalog.py,semantics.py, fixtures, andFINDINGS.md— the incident record that "FINDINGS §N" citations inharness/andROADMAP.mdrefer to. Likeontologyandharness, not part of the editable install. scripts/numbered standalone demos (01–41, not contiguous),06_tour.py(~90 s full story),make_figures.py [--quick|--full].13_discovery_run.pyis the funnel's operator console (--dry-run,--report).docs/00–26: a reading course; keep cross-references consistent with actual filenames (doc 05 is05-de-bruijn-newman.md; a baredocs/08always means08-why-it-is-hard.md— the detector-strength findings that once shared the number are22-detector-strength-findings.md).docs/doors/holds the entry-point guides: one short page per audience (learn, refute, certify, discover, adopt) plus one page per department. Adding a purpose to the repo costs a guide page plus a test that the page's command still works; a purpose that will not pay that stays a document, not a directory. KeepREADME.mdan index, not a manual — do not let it grow back into a single 400-line front page for four different audiences.interactive_lab/— standalone browser visualizations; illustrations, not results (its README states the contract: single-file pages, values hard-coded from what the suite pins).tests/pytest;data/caches;figures/PNGs;references/papers.md;conjectures/the discovery ledger — gitignored, a private notebook of unreviewed leads (only.gitkeepis tracked). Nothing in it is evidence for anything; publishontology.metrics.render_text, never the log. An emptyconjectures/in a fresh clone is the rule working, not a bug — to share one ledger across your own machines runscripts/ledger_sync.sh initonce, thensync; it clones a separate private repo in place, and this public tree still never carries a record.
The naming trap: three different "theta"s
zeta.core.theta— Jacobi θ(x) = Σ_{n∈ℤ} e^{−πn²x} (the heat kernel; modular identity θ(1/x) = √x·θ(x)).zeta.core.rs_theta— Riemann–Siegel phase ϑ(t) in Z(t) = e^{iϑ(t)}ζ(½+it) (zeta.statistics.riemann_siegel_thetais the fast vectorized variant).zeta.explicit.theta_cheb— Chebyshev's prime sum θ(x) = Σ_{p≤x} log p.
Related trap: xi(s) is the completed zeta (entire, ξ(s) = ξ(1−s)); Xi(t) = xi(1/2 + it) is real for real t. Do not use Ξ for the function of s. In heatflow.py, H₀(z) = (1/8)·Ξ(z/2) — mind the factor 8 and the z/2.
And a fourth collision, this one in the import system: zeta.explicit.li is the logarithmic integral and is re-exported as zeta.li, but zeta/li.py is Li's criterion, so after any import zeta.li the package attribute is the module and zeta.li(x) raises TypeError. Documented in zeta/li.py and pinned by tests/test_li.py. Write zeta.explicit.li for the function and from zeta.li import … for the module; never from zeta import li. The Jensen coefficients also come in two normalisations: zeta/li.py uses GORZ's 8·ξ(½+z) = Σ γ(n) z^{2n}/n!, docs/12 §8.1 derives the heat-kernel one; they differ by 64·4ⁿ, which changes no hyperbolicity and no Turán ratio.
Cached data
Expensive results cache to data/ (.json zero tables are committed; .npz scans are gitignored and regenerate on first use). Cache keys encode parameters in filenames. If you change numerical internals, delete the affected cache files and re-run, or stale numbers will "pass".
How to run things
cd <repo root>
.venv/bin/python -m pytest -q # full suite (2189 tests, ~10-20 min)
.venv/bin/python -m pytest -q -m "not slow" # fast tier (2122 tests, ~3-8 min)
.venv/bin/python scripts/06_tour.py # end-to-end sanity + demo
.venv/bin/python scripts/make_figures.py --quick # all figures into figures/
cd lean && PATH="$HOME/.elan/bin:$PATH" lake build # the certified arm (0 sorrys)Tests run in parallel by default (-n auto, set in pyproject.toml) — the fast tier goes from ~320 s to ~115 s. Add -n0 when you need --pdb or clean per-test output — not -p no:xdist, which unloads the plugin that owns the -n auto already in addopts and dies with "unrecognized arguments: -n". Before optimising anything, run --durations=20: the cost concentrates in test_li.py, test_heatflow.py and test_weil.py (high-precision zero sums and quadrature).
Tests use mpmath's zetazero / siegelz / grampoint / nzeros as an independent oracle against the hand-rolled machinery — preserve that pattern when adding features: implement the mathematics, then cross-check.
Ground truth for quick assertions
- ζ(2) = π²/6 = 1.6449340668482264…, ζ(0) = −1/2, ζ(−1) = −1/12.
- γ₁ = 14.134725141734694, γ₂ = 21.022039638771555, γ₃ = 25.010857580145689.
- N(100) = 29 zeros with 0 < γ < 100. Ξ(0) = 0.4971207781…
- θ(1/x) = √x·θ(x) and ξ(s) = ξ(1−s) hold to working precision (measured defects ~1e-30 at dps=30).