fix(ci+missions): close the verification-gate holes found in the 2026-09-18 audit

[DrMurphyIsIn]

The 2026-09-17/18 RH critical-path mathematics held up under adversarial audit. The machinery around it did not. This closes seven gate holes and records three more with reasons for leaving them.

Full findings: telperion/docs/VERIFICATION_GATES_AUDIT_2026-09-18.md.

Headline: two nodes were proved against Lean nothing ever compiled

ZeroFreePolylog.lean and ZeroFreeElementary.lean are terminal on the li_positivity island. Nothing imports them, they are not in defaultTargets, and they sat outside the axiom guard's import closure. Their oleans are absent from all three independently built worktrees while their neighbours are present. The nodes are RH_zero_free_gamma5 and RH_zero_free_polylog.

Importing ZeroFreePolylog into AxiomGuardLiPositivity.lean, which is a defaultTargets lean_lib, puts both modules under lake build and prints their axioms. If they do not compile, li-positivity-compiles now goes red. That is the intended outcome.

The rest

• Axiom guards for rvm_bridge and li_positivity failed only on sorryAx, so a new upstream axiom would have passed. Both now require every printed axiom line to be exactly the three standard axioms, run under set -euo pipefail because lake env lean | tee masked a crashed run, and fail if fewer lines printed than the guard has anchors. The idiom comes from telperion-production.yml, which already had it right.
• No CI job ran the missions battery. mission verify now runs inside the required unit job, covering all four campaigns in seconds.
• The grant gate proved nothing. It checked that an artifact contains a statement, never that it proves it, and normalize_lean strips a trailing := by sorry before comparing, so a stub matched more easily. Gate and battery now reject sorry/admit/native_decide in Lean code, comments and strings stripped first. Three tests. All campaigns still verify clean, so nothing currently proved was resting on a stub.
• proof-lean has been red on main since 2026-09-12. Cache restore missed, the cold rebuild was killed near 104 minutes, and the cache post step was skipped because the build failed, so the next run started cold too. Restore and save are now split, with the save on if: always(). This is the BG layer, not RH.
• mirrormere's manifest still described the pre-feat(rh): T=8000 via the height chain (7,830 zeros) + the 10^6 campaign orchestrator #506 state.

Left open on purpose

Island jobs are still not required checks. The lean workflow is path-filtered on telperion/**, so making them required would leave every docs-only PR permanently unmergeable, which this repo has already hit. Adding mission verify to the already-required unit job raises the floor where it can be raised today.

The registry DAG's depends_on edges are documentary rather than mechanical: no bridge imports another, so the critical path is three independent theorems, not a chain. The generated statement files are hash-locked, so this is recorded in the audit doc instead of hand-edited.

This PR does not run the grant pass. After #506 all 15 linked-but-ungranted artifacts are on main, so it is unblocked, but granting is ceremonial here and is left to the owner.

conjecture1_proved = False.

🤖 Generated with Claude Code