PRODUCTION: runbook for the 215 sites of plan v2 and their assembly

Hunt #145, written 2026-10-26, revised the same day after the whole-tower re-pilot. The owner granted the production window on cloud compute that day (MISSION.md, "Owner decision, 2026-10-26"). The Novita account had zero balance, so nothing here has been launched. This page is what the coordinator runs once compute is funded. Every cost below is a projection from one pilot site (PILOT.md sections 4 and 9), not a measurement of production.

0. Decide before launch

1. Use --tower whole. The generator now has an opt-in whole-tower mode (scripts/60 --tower whole). Each prime tower is one decide +kernel of dirichletTermBallB ... = lit plus contains_dirichletTermBallB. The pilot site compiled in it end to end with both planted tower faults refused (PILOT.md section 9). Projected: 30 core-hours (29.8) against 416 core-hours for the default staged mode, and 14.8 to 16.0 GB of oleans against 123 to 146 GB.
2. Where. On these projections the sites fit GitHub Actions shards and the assembly fits one 32 GB machine (section 1). That is assessed, not tested. One single cloud machine is the simpler alternative.
3. One thread per process. scripts/72 runs lean at its default threads. -j1 buys predictable sharing and no saving (OWNER_MEMO.md, item 3).

1. Machine shape

Where production fits, in whole mode (PILOT.md section 9 gives the reasons):

• (a) The shared box: no, while the co-tenant holds its disk floor and the owner's decision keeps it to pilots. Its CPU and memory would suffice.
• (b) GitHub Actions shards of 4 vCPU, 16 GB, 14 GB disk and 6 h, with the assembly on one larger machine: yes, on these numbers. Use about 20 jobs of about 11 sites each, balanced by projected CPU (whole_projection.rows in pilot.json). That is about 1.5 core-hours and 0.8 GB of oleans per job. Each job uploads its $OUT oleans and its site records. The assembly machine needs at least 32 GB of RAM and 40 GB of disk; a 16 GB runner falls short. Not measured: a runner's speed, restoring the Mathlib cache within 14 GB, and whether the artifact quota holds 16 GB.
• (c) One cloud machine of 32 cores, 32 GB and 40 GB of disk does everything in about 1 to 2 hours. It is not required.

Never run Lake in a copied .lake (CLAUDE.md, compute rule 7).

2. The workflow: .github/workflows/rung3-production.yml

The sites run on GitHub Actions by the workflow, which production.py drives step by step (test_production.py pins both). It is triggered only by a push of RUN_REQUEST.json to hunt/rung3-ball-production, never by the workflow file, and only after the coordinator's 'go'. Limits: permissions: contents: read, a concurrency group, 350 minutes per job with compiles stopping themselves at 300, and at most 6 jobs at once.

• {"mode": "calibrate", ...}: one job compiling the centre (K = 361, the largest site) and B_right_06, one Lean process at a time. sites.json in its record artifact gives each site's CPU, wall, peak RSS and olean bytes on a runner. Those numbers replace this box's rates in the full run's sizing.
• {"mode": "full", "jobs": 20, "lean_jobs": 1, "fault_site": "B_right_06", "calibration": {...}, ...}: 20 site jobs, plus the job fault, whose kernel must refuse a one-unit radius fault at Prime_B_right_06_2.ev_whole. The calibration block must equal the recorded runner calibration (production.py calibration(); PILOT.md sections 10 and 12). With attempt 2's figures, each job is bounded at 1.32 to 1.37 hours: setup plus 1.5 times its runner-scaled CPU at one core. lean_jobs stays 1 because the centre peaked at 11.3 GB. The verdict job counts the run only if all 215 sites compiled, every site theorem rests on exactly propext, Classical.choice and Quot.sound, and the fault was refused.

Each job removes unused runner toolchains to free disk, then restores ~/.elan and ~/.cache/mathlib (Mathlib's downloaded archives, keyed on revision 065356127b1d). It builds a fresh lean/.lake with lake exe cache get and never restores a .lake. It checks that every package is its own git toplevel. It runs the fail-closed preflight: pinned toolchain, Mathlib revision, request shape, and the staged default's byte identity against the 2026-10-21 hashes. Then it builds the ZetaLean closure, generates its sites (scripts/60 --tower whole), compiles them (scripts/72) and audits the axioms. It uploads rung3-production-job<N>-attempt<A> (oleans, checkpoints, manifests, logs) and a small rung3-production-record-job<N>-attempt<A>. A re-run attempt downloads its job's earlier artifacts and resumes from their checkpoints.

The planted-fault path and the axiom audit ran on this box against the whole-mode pilot site before the workflow was pushed. The fault was refused at Prime_2.ev_whole, and at Prime_B_right_06_2.ev_whole after the rename of PILOT.md section 11. upper_B_right_06 printed exactly the three axioms. The calibrate mode then ran on a runner and succeeded (run 40340279740, PILOT.md section 10): the centre took 1,348 CPU-s and 557 s of wall at an 11.3 GB peak, with a 295 s setup. On runners, production is about 18.5 core-hours. The full mode has not run; it needs its own 'go'.

2a. Commands, for a single machine instead

From a fresh clone of the branch commit, on the production machine (or in each job):

python3 -m venv .venv && .venv/bin/pip install -r requirements.txt && .venv/bin/pip install -e .
cd lean && lake exe cache get          # production machine only, never on the shared box
for p in .lake/packages/*; do git -C "$p" rev-parse --show-toplevel; done   # each names itself
lake build ZetaLean.BallCertSupport ZetaLean.BallTerm   # the 15 ZetaLean modules the sites import
cd ..

Generate the sites. This is Python only: the census of all 215 sites in whole mode took 51 CPU-minutes, the centre 69 s and a grid point about 20 s. It parallelises per site with --only <id>:

GEN=/data/rung3/gen OUT=/data/rung3/out
.venv/bin/python scripts/60_rung3_generate.py lean/cert/rung3_plan2.json "$GEN" \
  --arith ball --shard --tower whole            # or --only <id>, once per site of a job
ls "$GEN"/*.manifest.json | wc -l      # 215 on one machine

Compile, resume-safe. --jobs (sites) times --module-jobs (modules per site) is the number of concurrent lean processes. Keep it at or below the cores (2 on a 16 GB runner), and keep MemAvailable above 20 GiB on a large machine:

nice -n 10 .venv/bin/python scripts/72_rung3_ball_compile.py --lean-project lean \
  --output-root "$OUT" --jobs 24 --module-jobs 1 "$GEN"/*.manifest.json

3. Checkpoints

• Per module: scripts/72 writes $OUT/checkpoints/<root>/... atomically after each module, with the source hash, CPU, peak RSS and return code. A restart with the same command skips verified modules and recompiles only what changed and its dependents.
• Per site: $OUT/results/C<id>.json, written whatever the outcome. Production is done when 215 records say ok.
• Records: before launch, write the estimate (one site timed, multiplied) in this hunt's RUNS.md. After it, write a runmanifest with the machine, the commit, the start and end times and the totals. The detached job has a watcher that records a terminal outcome (CLAUDE.md, compute rule 5).

Then the assembly, in one process, with every site root's olean on LEAN_PATH (they are linked beside their sources in $GEN):

A=/data/rung3/assembly
.venv/bin/python hunts/rung3_ball_production/assembly.py --out "$A" --check   # emits; the pin must match
H=hunts/rung3_ball_production/lean
cd lean
lake env lean --root=../$H -o "$A/Rung3Assembly/Support.olean" ../$H/Rung3Assembly/Support.lean
lake env sh -c "LEAN_PATH=$A:$GEN:\$LEAN_PATH lean --root=$A -o $A/Rung3Assembly/Assembly.olean $A/Rung3Assembly/Assembly.lean"

Assembly.lean and Separation.lean are emitted, not committed: they import the generator's site roots, which are not module files (PILOT.md section 8).

Separation.lean also needs hunt #137's olean closure (hunts/rh_height_lean/lean/build.sh --full, built against lean/vendor/zeta23's Mathlib at the same revision) on the same LEAN_PATH. That combination has never been run; if the two Mathlib builds conflict, record it and keep dh_separation_of, which takes RH to height 100 as a hypothesis.

4. Planted faults to re-run on production output

On one compiled big-box site (B_right_06, as in the pilot), with pilot.py's work directory set by RUNG3_PILOT_WORK. Each must be refused at the named declaration, and the clean site must still compile:

export RUNG3_PILOT_WORK=/data/rung3/faults
.venv/bin/python hunts/rung3_ball_production/pilot.py site --site B_right_06
.venv/bin/python hunts/rung3_ball_production/pilot.py fault --site B_right_06 --kind tower-rad   # a tower radius 1 unit of 2^-64 low
.venv/bin/python hunts/rung3_ball_production/pilot.py fault --site B_right_06 --kind tail-rad    # the tail radius just under its bound
.venv/bin/python hunts/rung3_ball_production/pilot.py fault --site B_right_06 --kind M           # M just under the enclosure's bound
.venv/bin/python hunts/rung3_ball_production/pilot.py centre-eps                                 # eps' refused at and below the bound

In whole mode, also re-run the two tower faults on that site (whole_pilot.py faults with RUNG3_WHOLE_WORK pointing at a whole-mode compile of B_right_06 made by whole_pilot.py site). Each must be refused at the faulted tower's ev_whole. The four pilot.py faults above run on the staged sources that pilot.py site generates. The tail-rad, M and centre faults sit in modules that whole mode leaves unchanged.

5. Axiom audit

• Every site theorem prints only propext, Classical.choice and Quot.sound: the check pilot.py axioms ran for B_right_06, which is one file per root holding import C<id> and #print axioms ZetaLean.DH.Cert.<upper_|beta_|centre_lt_><id>, compiled with $GEN on LEAN_PATH. pilot.py runs it only inside its own work layout, so for the 215 roots loop it over $GEN directly.
• The assembly: #print axioms ZetaLean.DH.Rung3Assembly.Plan2.davenport_heilbronn and #print axioms ZetaLean.DH.Rung3Assembly.Plan2.dh_zero_located' print exactly those three. The pilot's stub harness printed those three plus the 214 stubs (assembly_harness in pilot.json). With the real sites, the stubs must be gone.
• The sources: no sorry, axiom, native_decide, implemented_by or Lean.ofReduceBool in $GEN, lean/ZetaLean or hunts/rung3_ball_production/lean. decide +kernel adds no axiom; native_decide would, and is not used.

Only after that audit does davenport_heilbronn get a grade, through the hunt's case log and review (ALIGNMENT.md). It is a statement about the Davenport-Heilbronn function and says nothing about RH (docs/08).

6. The assembly: collect, check, import (the coordinator decides placement)

Prerequisite: whole-mode site oleans with site-qualified tower namespaces (Prime_<sid>_<p>, PILOT.md section 11), from a full run whose verdict job counted it. Output of the staged default, or of whole mode before that fix, cannot be imported two sites at a time.

Size, re-projected from the runner. The calibration's centre measured 343.5 MB of oleans, inside the projected 316 to 371 MB, so the projected 14.8 to 16.0 GB total stands until the full run's records give the exact sum. Importing the runner-built centre raised peak RSS by 0.708 bytes per olean byte over the 6.57 GB of the support imports (import_probe_centre). By that ratio the 215-root import needs 10.4 to 11.3 GB above the support modules, about 17.0 to 17.9 GB in all, nearly all of it mapped olean pages. Still untested: one process importing all 215 roots. The two-site harness (section 8 of PILOT.md) is the largest real import so far.

Collect and check. On the assembly machine, from this checkout:

D=/dev/shm/rung3-assembly       # or a directory on the cloud machine's disk
.venv/bin/python hunts/rung3_ball_production/production.py collect \
  --request hunts/rung3_ball_production/RUN_REQUEST.json --run <full run id> --dest "$D"

collect takes each job's latest-attempt rung3-production-job<N>-attempt<A>. It downloads the zip through the API and checks its SHA-256 against GitHub's recorded digest, refusing on any mismatch. It unzips into $D, deletes the zip before the next one (so the peak is the oleans plus one zip), and checks that every site the job owns has its root olean and its root checkpoint. It writes $D/collected.json with every artifact's hash. Then:

• confirm rung3-production-record-* says every site ok and every axiom audit clean. The verdict job already did this; re-run production.py verdict --records <dir> on the downloaded records to see it locally;
• optionally, regenerate the sources (scripts/60 --tower whole, about 51 CPU-minutes) and compare their SHA-256 with the sha256 in each out/checkpoints/C<id>/*.ok.json. This ties every olean to the generator at the tested commit.

The oleans are trusted as the runners' kernel left them; the import does not re-check their proofs. For an independent re-check, run the toolchain's leanchecker over the assembly's environment. That replays every declaration in the kernel, at a cost of about the sites' compile CPU; it is not yet sized.

Import. Emit and compile, with $D/out (all jobs' outputs merged, file names disjoint by site) on LEAN_PATH:

.venv/bin/python hunts/rung3_ball_production/assembly.py --out "$D/asm" --check
cd lean
lake env lean --root=../hunts/rung3_ball_production/lean -o "$D/asm/Rung3Assembly/Support.olean" \
  ../hunts/rung3_ball_production/lean/Rung3Assembly/Support.lean
lake env sh -c "LEAN_PATH=$D/asm:$D/out:\$LEAN_PATH lean --root=$D/asm \
  -o $D/asm/Rung3Assembly/Assembly.olean $D/asm/Rung3Assembly/Assembly.lean"

Then run the axiom audit of section 5 on ZetaLean.DH.Rung3Assembly.Plan2.davenport_heilbronn.

Placement options, against about 17 to 18 GB of resident memory and about 16 GB of oleans:

1. The shared box, with the oleans on a RAM-backed tmpfs. Its disk sits below the co-tenant's floor, so $D is /dev/shm/rung3-assembly, which is already a 58 GB tmpfs and needs no sudo. This checkout's existing lean/.lake serves Mathlib, so no new Mathlib is fetched. The mapped oleans are the tmpfs pages themselves and are not counted twice. The total is about 16 GB of tmpfs, Mathlib and support oleans in page cache (about 7 GB, mostly resident already) and a few GB of anonymous memory.
2. Start only while MemAvailable is above 45 GiB (the 20 GiB guard plus about 25 GiB) and the 1-minute load is at most 64.
3. Guard: read MemAvailable every 10 s. Below 20 GiB, stop the Lean process and rm -rf /dev/shm/rung3-assembly. A tmpfs is lost on reboot, so the artifacts stay on GitHub (30 days) until Assembly.olean exists.
4. Cost: the harness's import took 127 CPU-s with two real sites; the full import is projected under 30 core-minutes, within this box's one core-hour cap.
5. Decision: the 2026-10-26 owner decision reserves the box for pilots, so placing the assembly here is the coordinator's or owner's call.
6. A funded cloud machine with at least 32 GB of RAM and 40 GB of disk, using a fresh lake exe cache get. It has no co-tenant risk, but it waits for funding.

The calibration's centre olean bytes already checked the projection once. The full run's olean_gb in its verdict summary checks it again before the import starts.