MISSION: `rung3_ball_production`, pricing the kernel check of the Davenport-Heilbronn zero

Opened 2026-10-21. Hunt #145. This is the rung3-pilot lane of the campaign the owner directed on 2026-10-21 (route 3, "Rung 3: kernel-checked Davenport-Heilbronn zero"). It is a ledger hunt: it pilots, measures and asks for a production window. It does not run production. Nothing in this directory is a result until the case log in hunts/README.md says how it ended.

The task text proposed number #138. The workflow that launched this lane reserved #138 to #144 for landings it is renumbering, and assigned #145; on 2026-10-21 no ref under refs/heads or refs/remotes/origin used #145 in its hunts/README.md.

Grades used here: measured (one route), hardened (independent routes agree, or ball enclosures carry every step) and kernel-checked (Lean, zero sorry, only propext, Classical.choice and Quot.sound). The reserved enclosure word belongs to zeta/rigor.py and the Lean arm and appears nowhere in this directory.

The question

Does the 215-site ball certificate lean/cert/rung3_plan2.json compile at Lean v4.35.0-rc2 on the swarm box, at what measured cost per prime-tower atom, per composite atom and per module, and does the kernel refuse a planted fault in an emitted radius and in eps'?

Why it matters

davenport_heilbronn_statement (lean/ZetaLean/DavenportHeilbronn.lean, line 96) says that some entire function with the Davenport-Heilbronn Dirichlet series and functional equation has a zero off the critical line. Its analytic half (dh_analytic_half), the tail bounds, the ball arithmetic and the square criterion (the theorem at line 185 of lean/ZetaLean/DHZeroCriterion.lean, cited by line because its name carries the word this directory may not use) are kernel-checked. What is missing is the numeric half: about half a million literal obligations, one site theorem per point or box of plan v2, then one assembly module. This hunt prices the first part and names the second.

Starting point (as recorded on main at fb647bfc7; these are citations)

• Plan v2 (lean/cert/rung3_plan2.json): 215 sites, 110 big boxes, 104 grid points and the centre. Small square w = 3/64, eps' = 1/2000, big square w2 = 7/32, L = 16, M = 25499/10000.
• Mirror. scripts/65_rung3_full_validation.py runs every site through the bit-exact Fraction ball mirror (scripts/63_rung3_ball_mirror.py); the record says all 215 pass at plan v2's geometry. tests/test_rung3_mirror.py and tests/test_rung3_ball_assembly.py check the mirror against mpmath and against the Hurwitz route.
• Budget. scripts/67_rung3_ball_atom_budget.py counts 549,149 atoms (468,240 tower atoms, 80,909 others) and prices them at 175.0 core-hours, atom-only and serial, from 1.2504 CPU-s per tower atom and 0.55 CPU-s per composite atom. The tower figure was measured on 2026-09-17, when lean/lean-toolchain pinned v4.33.0-rc2, on a machine the record does not name. Both figures are pinned by tests/test_rung3_ball_atom_budget.py.
• Driver. scripts/72_rung3_ball_compile.py compiles a sharded site with lake env lean --root, checkpointing each module. The 2026-09-18 centre pilot stopped on an import that resolved beside the sources; commits 1e3f8505d (peak RSS and a site result file) and e52bbe896 (link each olean beside its source) on teal-sea/rung3-centre-pilot-sep18 fix that. This branch first cherry-picked them; they then landed on main through PR #323 with a follow-up, 571857a47, that keeps the root-olean link across resumes, and this branch merged origin/main (e08e801da), so the pilot runs main's driver.
• Not built anywhere. No script emits the assembly module that combines the 215 site theorems with norm_deriv_DH_le, DH_lower_on_hcell, DH_lower_on_vcell and the square criterion into theorem davenport_heilbronn : davenport_heilbronn_statement.

Scope

• In scope. Lean setup in this worktree's lean/ by a fresh Lake fetch; building only the ZetaLean modules the certificate imports; one staged prime tower (scripts/68); one small big-box site generated by scripts/60 --arith ball --shard --only <site> and compiled by scripts/72 --jobs 1 --module-jobs 1 into a directory outside the tree; planted faults in copies of the generated files; a cost table and a memo asking the owner for a production window.
• Out of scope. Any production shard, any site beyond the pilot, the assembly module, any edit to zeta/, ontology/, harness/ or the certificate's mathematics in lean/ZetaLean/, and any claim about RH.
• Compute. The swarm box (32 vCPU Haswell, 115 GiB, no swap), shared with other workflows. Under CLAUDE.md compute rule 6 as merged on main, Lean and numerics may run side by side while MemAvailable stays above 20 GiB; this lane waits while it is below 30 GiB before any process that may exceed 8 GB, runs pytest with -n0 or at most -n 4, caps parallel numeric jobs at 8 processes and waits while the 1-minute load average is above 64 before a heavy job. Rule 7: Lake runs only in a .lake it fetched itself, with every package's git toplevel checked.

id: rung3_ball_production
question: Does the 215-site ball certificate lean/cert/rung3_plan2.json compile at Lean v4.35.0-rc2 on the swarm box, at what measured cost per prime-tower atom, per composite atom and per module, and does the kernel refuse a planted fault in an emitted radius and in eps'?
frontier: the bit-exact ball mirror (scripts/65) is recorded as passing all 215 sites; scripts/67 prices 549,149 atoms at 175.0 core-hours atom-only from 1.2504 CPU-s per tower atom (measured under v4.33.0-rc2 on 2026-09-17 on a machine the record does not name) and 0.55 CPU-s per composite atom; no site has been compiled end to end under v4.35.0-rc2; no script emits the assembly module that proves davenport_heilbronn from the site theorems
proposed_attack: re-pilot one staged prime tower (scripts/68) and one K = 17 big-box site (scripts/60 --shard, compiled by scripts/72 with one process at a time), plant a radius fault and an eps' fault in copies of the emitted files, and price production from the measured per-module CPU, peak RSS and import overhead
dead_routes:
  - rectangle (ComplexInterval) term boxes, whose rotation waste failed the grid and the centre (docs/25 section 4.3)
  - one-shot norm_num evaluation of a whole term box, which exceeded the simp step limit (HANDOFF, negative result 2)
  - in-tactic square roots (mulA) in ball products, recorded at about 6.5 s per atom against 0.55 s with literal modulus bounds (scripts/66)
  - unsharded whole-site files, whose cost is recorded as nonlinear and whose centre caused memory pressure on a 32 GB machine (scripts/67)
required_oracles:
  - the Lean kernel at v4.35.0-rc2 against Mathlib 065356127b1d, with the axioms of the pilot site theorem printed
  - the bit-exact Fraction ball mirror scripts/63 and its full validation scripts/65
  - tests/test_rung3_mirror.py and tests/test_rung3_ball_assembly.py, which check the mirror against mpmath and the Hurwitz route
  - wait4 resource usage (user, system, peak RSS) as recorded by scripts/72
kill_conditions:
  - the pilot site does not compile at v4.35.0-rc2 from the shipped generator, recorded with the failing declaration
  - a planted radius fault or eps' fault compiles, which would mean the kernel is not checking what the certificate states
  - a literal the kernel accepts on the pilot site differs from the mirror's value
  - the projected production cost exceeds what this box can do in one week at 24 processes, recorded as an allocation pause and not as a mathematical no-go
agents_may:
  - read
  - code
  - generate one pilot site and one prime tower
  - compile with lake env lean under the swarm-box rules
  - plant faults in copies of generated files
  - measure
agents_may_not:
  - launch any production shard or compile any site beyond the pilot
  - edit zeta, ontology, harness or the certificate's mathematics in lean/ZetaLean
  - declare theorem status for davenport_heilbronn, which no file proves yet
  - declare novelty
  - promote their own claim
  - push, publish or contact outside parties

Deliverables

MISSION.md (this file), RUNS.md (estimates before spending and run manifests), PILOT.md (what ran, what the kernel did, the cost table), pilot.json (the raw measurements behind every number in PILOT.md), OWNER_MEMO.md (the request for a production window), a hunt test pinning those numbers, and a case-log entry in hunts/README.md. The instruments: pilot.py (every Lean run, gated and timed), report.py (pilot.json and the rendered tables, from the run log alone) and render_docs.py (writes those tables into the two documents).

Owner decision, 2026-10-26

The owner resumed this lane in place on 2026-10-26 and decided:

• The production window OWNER_MEMO.md requested is granted, on cloud compute. The shared box takes only pilots under one core-hour each.
• Production waits for funding. The Novita account had zero balance on 2026-10-26, so nothing in this lane launches production; PRODUCTION.md is the runbook for the day it is funded.
• Scope of the supersession. The text above stands as written, including the agents_may_not entry "launch any production shard or compile any site beyond the pilot" (line 109). This decision supersedes that entry for the future, funded production run only; until then it binds as before.
• Added to scope for the resumed lane: one decide +kernel re-pricing pilot of a scripts/68 tower (one process, under one core-hour); an emitter, in this directory, for the assembly module that would prove davenport_heilbronn from the 215 site theorems, with its own Lean sources here and none in lean/ZetaLean; and PRODUCTION.md.

Supersession record, 2026-10-26 (after the PR #353 review)

What the lane did after the owner decision above went beyond the text of this file. The record of who allowed each step:

• Production ran on GitHub Actions, not on funded cloud compute. The calibration and full requests were pushed after the coordinator's 'go' (RUNS.md, and the commit messages of c697df4f0, 0f42610de and 85cabd55b), and the coordinator placed the assembly on the shared box (RUNS.md, "the full run, and the assembly on this box"). This supersedes "Production waits for funding" and the agents_may_not entry "launch any production shard or compile any site beyond the pilot" for that run only.
• The landing declared theorem status and edited harness/. Commit a3bc93e53 added the review-ledger entry davenport-heilbronn-rung3 to harness/departments/review_ledger.py and the status lines in RESULTS.md and hunts/README.md, against the agents_may_not entries "edit zeta, ontology, harness ..." and "declare theorem status for davenport_heilbronn, which no file proves yet". The ledger entry asks for review; it promotes nothing.
• The PR #353 review found the headline statement weak. davenport_heilbronn_statement is also met by the trivial zero s = -1. On the coordinator's direction of 2026-10-26 the record fix added lean/ZetaLean/DHTrivialZero.lean (a new module under lean/ZetaLean, outside the sites' import closure, against "none in lean/ZetaLean" above), amended the ledger entry, and moved the headline to dh_separation_hundred and dh_zero_located with dh_analytic_half. No definition in lean/ZetaLean changed.
• Novelty is still not declared. The record says searched-and-absent (PRIOR_ART.md), not novel.

Supersession record, 2026-10-27 (door 1, Stage B on a fleet)

The operator's brief of 2026-10-27 asked for the independent con-ron --verified check of the whole assembled closure, split site by site across InstaBox VMs (primary) and Novita sandboxes (second provider), exported on the shared box one artifact zip at a time, under a hard cap of USD 40 (as run, a gate on new launches at a projected USD 36; nothing stopped VMs already running, see RUNS.md), a 12-hour dead-man over every VM of the run, and the box's memory and disk floors. That brief authorized, for this run only: paid cloud compute; export, compression and checking of all 215 sites and a top shard; a full re-collect and re-assembly on the box to rebuild the assembly oleans Stage A had deleted (they came back byte for byte); edits to RESULTS.md, RUNS.md, harness/departments/review_ledger.py, docs/47 section 1 and the README front page. The instruments are new files in this directory (conron_fleet.py, conron_shard.py, shard_manifest.py, lean/ExportShard.lean, test_stage_b.py); no definition in lean/ZetaLean changed and no Lake build ran in this worktree.