missions: close the statement-package import hole (15 never-elaborated statements; verify now gates the root import list)

[DrMurphyIsIn]

The hole

MISSIONS_DESIGN §2: "CI builds each statement package: a statement that does not elaborate cannot enter the graph." The mission-statements-compile job runs lake build in missions/<campaign>/lean, which compiles the import closure of the root Statements.lean and nothing else. mission add wrote the node file and Statements/<Slug>.lean but never touched the root, and nothing checked. Fifteen registered modules, thirteen of them status = "proved", had current provenance hashes and had never been elaborated by any job. One had no import line at all.

No status changes, no grants, no audits. conjecture1_proved = False.

The fifteen

campaign	node	status	regen hash
rh	RH_bl_closed_form_five_nonneg	proved	unchanged
rh	RH_dbn_H0_zero_strip	proved	unchanged
rh	RH_li_ladder_height	proved	unchanged
rh	RH_li_ladder_height_sharp	proved	unchanged
rh	RH_li_ladder_liLimit	proved	unchanged
rh	RH_li_ladder_liLimit_sharp	proved	unchanged
rh	RH_li_rungs_lt_five	proved	unchanged
rh	RH_li_rungs_of_height_4000	proved	unchanged
rh	RH_li_rungs_of_height_4000_sharp	proved	unchanged
rh	RH_zeta_zero_confined	proved	unchanged
rh	RH_zeta_zero_im_ge	proved	unchanged
mirrormere	MM_gaussian_positivity_small_lam_3e3	proved	unchanged
mirrormere	MM_leakage_composite_zero	proved	unchanged
mirrormere	MM_satake_degree_two_rejects_delta	draft	unchanged
mirrormere	MM_weil_positivity_window_tenth	draft	7b32a808ac3e6c1c -> 453fc3f023904fb0

Hash change, why: the window-tenth file was written with no import line. It was regenerated through regenerate_statement (the write_statement path) with import Mathlib + import Statements.MMDefs prepended; the theorem text is byte-identical. Recorded as a comment block in the node file, the way #606 recorded its re-specification hash. The other fourteen regenerate byte-identically.

Vocabulary mirrors needed: none. Every one of the fifteen elaborates against the existing RHDefs / MMDefs (archSide/finiteSide via the RvMBridge15.BombieriLagarias re-export, DBN.H, LiCriterion.taylorCoeff/riemannXi, RvMBridge15.liLimit, Zeta23.IsNontrivialZero, RvMBridge6.zeroSide/gaussTest, WeilExplicit.*). The mirror drift test is untouched and green.

Commits (one per deliverable)

1. Gate (69cb4fe): statements.py gains root_imports / ensure_root_import / missing_root_imports / import_header_error / regenerate_statement; write_statement appends the module to the root, so mission add (which did not do this) now wires new nodes; regen_diff reports a statement the root does not import alongside a stale hash; verify_campaign fails on an un-imported node statement, a stray Statements/*.lean no root names, a root import with no file, and a statement without the standard header (Mathlib or a campaign *Defs import). On this commit alone the live rh and mirrormere campaigns fail the battery, which is the point.

2. Fix (7d54bfe): the fifteen regenerated and imported from both roots; live-campaign root-import test added.

3. Staleness at the CLI (c46410b): mission verify exits 1 on a well-formed, current-hash statement the root does not name; scaffold_package (root regenerated from disk) and missing_root_imports agree.

4. Docs (41115a2): MISSIONS_DESIGN §6 row for add, §7 item 5, new §11 naming the fifteen and the date.

5. Sorted roots, merge discipline (93c8a34, after the team lead's heads-up on anduril: all zeta zeros to height 1000 on the critical line, kernel-checked with NO hypotheses (AND_ladder_h1000_kernel PROVED) #613/Route C: M1 PROVED (parametric de Bruijn, up-set, RH <=> all H_t real for t >= 0); P15 criterion wired; M6 gaps; M5 bricks + P15 eq (76) erratum #614/mirrormere: the full prime-free window (2L <= log 2) proved kernel-native, hypothesis-free, no Arb seam (draft; includes #606; grant after #607) #615): ensure_root_import inserts in sorted position, sort_root_imports re-sorts, and the four live roots are sorted (same import sets, verified). mission verify only WARNS on an unsorted root, so a held branch that appended by hand still passes.

MERGE NOTE for anyone touching lean/Statements.lean

Held PRs #613 (anduril), #614 (rh, 3 M1 nodes) and #615 (mirrormere) add root imports by hand and WILL conflict with this PR on the root files. Resolve by re-sorting the import list (one import per line, alphabetical), never by union-merge:

PYTHONPATH=telperion/src python -c "from telperion.missions.statements import sort_root_imports; sort_root_imports('telperion/missions/<campaign>')"

After resolving, mission verify must say OK for the campaign with no "not sorted" warning, and lake build in the package must be green.

Builds and tests

check	result
lake build rh statement package	green, 8765 jobs (was 8754, +11)
lake build mirrormere statement package	green, 8700 jobs (was 8696, +4)
non-sorry warnings/errors in either build	none
mission verify (anduril, bg, mirrormere, rh)	OK x4
pytest tests/test_missions_*.py	217 passed, 1 skipped (was 190 + 1; 27 new)
lake build anduril after re-sort	green, 8671 jobs

Builds were run locally on reflinked Mathlib caches at the campaigns' pinned toolchains (rh v4.34.0-rc1, mirrormere v4.32.0); the mission-statements-compile matrix on this PR is the CI confirmation.

Not done / caveats

• The header check accepts import Mathlib alone (23 live statements are self-contained that way); it does not require the campaign Defs module.
• bg and anduril were already fully wired; nothing changed there.

🤖 Generated with Claude Code

https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU