verify-all-provers: run the Print Assumptions audit and its control inside the canonical gate

`just verify` -> proofs/verify-all-provers.sh built Coq and printed ALL-PROVERS-GREEN
without ever running proofs/coq/check-assumptions.sh, so the canonical gate could say
GREEN on a theorem resting on an axiom: the same "guard asks a different question"
defect this PR cures elsewhere (CodeRabbit's Major on the first commit).

- verify-all-provers.sh: after a successful Coq build, run check-assumptions.sh and
  check-assumptions.sh --control; either failing sets fail=1 with its own reason line.
- gate-selftest.sh: the coqc stub now answers `Print Assumptions` faithfully (Closed
  for every audited theorem, `Axioms: kB_positive` for the control's target), so case A
  exercises the audit; cases O (every theorem reports an axiom) and P (the control's
  target reports closed) prove the gate turns red for each. 16/16 locally; with the
  previous gate exactly O and P fail (meta-mutant), and I still passes after them.
- PROOF-STATUS: 14 -> 16 cases; the audit is named as part of the canonical gate.

Real prover, Coq 8.20.1: `just verify-coq` -> ASSUMPTIONS-CHECK OK 17/17,
ASSUMPTIONS-CONTROL OK (landauer_limit_positive rejected naming kB_positive).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57

Author: hyperpolymath

PROOF-STATUS.adoc

@@ -20,8 +20,10 @@ plus the *Idris 2* ABI. Both the CNO and OND pillars are covered.
 An absent prover is a *failure*, never a skip (since 2026-09-23 — before that Isabelle
 and Mizar printed "skipped" and the gate could say GREEN on four of six), and Z3
 verdicts are compared with the `; expect sat|unsat` annotation on every `(check-sat)`
-(`proofs/z3/verify.sh`). `proofs/tests/gate-selftest.sh` proves both gates turn red for
-each absent or failing prover and for each verdict mutant (14 cases, run in CI).
+(`proofs/z3/verify.sh`). Since 2026-09-23 the gate also runs the Coq `Print Assumptions` audit and
+its `--control` after the build, so a theorem resting on an axiom, or an audit that can no
+longer say no, turns it red. `proofs/tests/gate-selftest.sh` proves both gates turn red for
+each absent or failing prover, for each verdict mutant and for both audit mutants (16 cases, run in CI).
 ====
 
 == Coq — VERIFIED (this environment)
@@ -90,7 +92,8 @@ These are the analogue of the OND-6 research fork: openly labelled, not silently
 assumed. `Print Assumptions` on each of the 17 theorems this document names in backticks
 prints `Closed under the global context` — no stdlib axiom and no project axiom (measured
 2026-09-23, Coq 8.18). That is CI-gated: `proofs/coq/audit/Assumptions.v` lists the 17 and
-`proofs/coq/check-assumptions.sh` (Coq job of `proofs.yml`) fails on any `Axioms:` block or a
+`proofs/coq/check-assumptions.sh` (Coq job of `proofs.yml`, and the canonical
+`proofs/verify-all-provers.sh` gate since 2026-09-23) fails on any `Axioms:` block or a
 missing line; its `--control` mode proves the gate bites by requiring that
 `landauer_limit_positive`, which rests on `kB_positive`, is rejected. The wider tree is not
 closed — 109 of 182 top-level theorems are; the other 73 rest on stdlib classical axioms

proofs/tests/gate-selftest.sh

@@ -31,6 +31,26 @@ for t in coqc coq_makefile make agda lake isabelle accom verifier idris2; do mks
 # z3_stub <verdicts>: replace the z3 stub with the supplied solver output.
 z3_stub() { mkstub z3 "case \"\${1:-}\" in --version) echo \"Z3 version stub\";; *) printf '$1';; esac"; }
 z3_stub 'sat\nunsat\nsat\n'
+# coqc must answer `Print Assumptions` faithfully, or the audit inside the gate
+# (proofs/coq/check-assumptions.sh) cannot be exercised: one "Closed under the
+# global context" per Print Assumptions line, except the control's target
+# (landauer_limit_positive), which rests on the tagged axiom kB_positive.
+# COQC_STUB_MODE=axioms  -> every theorem reports an axiom (case O)
+# COQC_STUB_MODE=closed  -> every theorem reports closed, control included (case P)
+cat > "$STUB/coqc" <<'COQC'
+#!/bin/sh
+f=""; for a in "$@"; do case "$a" in *.v) f=$a;; esac; done
+[ -n "$f" ] && [ -r "$f" ] || exit 0
+grep '^Print Assumptions' "$f" | while IFS= read -r line; do
+  id=${line#Print Assumptions }; id=${id%.}
+  case "${COQC_STUB_MODE:-}:$id" in
+    axioms:*|:*landauer_limit_positive*) printf 'Axioms:\nPhysicsConstants.kB_positive : (0 < kB)%%R\n';;
+    *) echo "Closed under the global context";;
+  esac
+done
+exit 0
+COQC
+chmod +x "$STUB/coqc"
 for s in "$STUB"/*; do sh -n "$s" || { echo "FAIL: stub $s does not parse"; exit 1; }; done
 
 OUT=""; RC=0
@@ -69,6 +89,13 @@ expect "G z3 unknown verdict -> fail" 1 "verdicts differ from annotations" "ALL-
 z3_stub 'sat\nunsat\nsat\n'
 # H. a prover that runs but fails must FAIL
 mkstub idris2 'exit 3'; run_gate; expect "H idris2 exit 3 -> fail" 1 "IDRIS FAILED" "ALL-PROVERS-GREEN"; mkstub idris2
+# O. Coq builds but a theorem rests on an axiom: the audit must turn the gate red
+#    (pre-2026-09-23 the canonical gate never ran the audit, so this was green)
+export COQC_STUB_MODE=axioms; run_gate; unset COQC_STUB_MODE
+expect "O coq audit sees Axioms: -> fail" 1 "COQ ASSUMPTIONS FAILED" "ALL-PROVERS-GREEN"
+# P. an audit that calls EVERYTHING closed, the control's target included, must FAIL
+export COQC_STUB_MODE=closed; run_gate; unset COQC_STUB_MODE
+expect "P coq control passes wrongly -> fail" 1 "COQ ASSUMPTIONS-CONTROL FAILED" "ALL-PROVERS-GREEN"
 # I. after the mutants, the positive control is green again (no state leaked)
 run_gate; expect "I positive control repeats green" 0 "ALL-PROVERS-GREEN" "SOME PROVERS FAILED"
 

proofs/verify-all-provers.sh

@@ -17,8 +17,13 @@ say() { printf '\n\033[1m== %s ==\033[0m\n' "$1"; }
 # ---- Coq (both pillars) --------------------------------------------------
 say "Coq — CNO + OND"
 if command -v coqc >/dev/null; then
-  ( cd "$HERE/coq" && coq_makefile -f _CoqProject -o Makefile.all >/dev/null 2>&1 \
-      && make -f Makefile.all -j"$(nproc)" ) || { echo "COQ FAILED"; fail=1; }
+  if ( cd "$HERE/coq" && coq_makefile -f _CoqProject -o Makefile.all >/dev/null 2>&1 \
+      && make -f Makefile.all -j"$(nproc)" ); then
+    # The build alone is not the gate: the 17 named theorems must be closed under
+    # the global context, and the control must prove the audit can say no.
+    bash "$HERE/coq/check-assumptions.sh" || { echo "COQ ASSUMPTIONS FAILED"; fail=1; }
+    bash "$HERE/coq/check-assumptions.sh" --control || { echo "COQ ASSUMPTIONS-CONTROL FAILED"; fail=1; }
+  else echo "COQ FAILED"; fail=1; fi
 else echo "coqc missing"; fail=1; fi
 
 # ---- Agda (CNO + OND) ----------------------------------------------------