proofs: honest prover gate — absent prover = fail, z3 expect-checked, Print Assumptions gated, Agda 4/4 --safe (4b–4d)

.github/workflows/proofs.yml

@@ -56,6 +56,11 @@ jobs:
           coq_makefile -f _CoqProject -o Makefile.all
           make -f Makefile.all -j"$(nproc)"
           echo "✓ Coq: 14/14 theories compiled (CNO + OND)"
+      - name: Print Assumptions gate (17 named theorems closed) + control
+        working-directory: proofs/coq
+        run: |
+          bash check-assumptions.sh
+          bash check-assumptions.sh --control
 
   agda:
     name: Agda — CNO + OND
@@ -79,13 +84,15 @@ jobs:
           mkdir -p "$HOME/.agda"
           echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries"
           echo "standard-library" > "$HOME/.agda/defaults"
-      - name: Type-check CNO + OND (--safe --without-K)
+      - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K)
         working-directory: proofs/agda
         run: |
           agda --version
           agda --safe --without-K CNO.agda
           agda --safe --without-K OND.agda
-          echo "✓ Agda: CNO + OND type-check"
+          agda --safe --without-K EchoBridgeScaffold.agda
+          agda --safe --without-K EchoBridgeCNO.agda
+          echo "✓ Agda: CNO + OND + EchoBridgeScaffold + EchoBridgeCNO type-check"
 
   z3:
     name: Z3 — CNO + OND bounded checks
@@ -97,9 +104,10 @@ jobs:
       - name: Run Z3 checks
         run: |
           z3 --version
-          sh proofs/z3/verify.sh || true
-          z3 proofs/z3/ond/OND_checks.smt2
-          echo "✓ Z3: OND bounded instances checked"
+          bash proofs/z3/verify.sh
+          echo "✓ Z3: every (check-sat) verdict matched its ; expect annotation"
+      - name: Gate self-test (stub provers + z3 mutants must turn the gate red)
+        run: bash proofs/tests/gate-selftest.sh
 
   lean:
     name: Lean — core CNO (6 modules + axiom audit)

Justfile

@@ -39,10 +39,10 @@ build-lean:
     @echo "Building Lean 4 proofs..."
     cd proofs/lean4 && lake build
 
-# Build Agda proofs (CNO + OND, --safe --without-K)
+# Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K)
 build-agda:
     @echo "Building Agda proofs..."
-    cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda
+    cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda && agda --safe --without-K EchoBridgeScaffold.agda && agda --safe --without-K EchoBridgeCNO.agda
 
 # Build Isabelle/HOL proofs (CNO + OND session)
 build-isabelle:
@@ -78,21 +78,21 @@ verify:
     @proofs/verify-all-provers.sh
 
 # Verify all proofs (per-prover targets; `just verify` is the canonical one-shot)
-verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris
+verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris verify-gate-selftest
     @echo "✓ All verifications complete"
 
-# Verify Coq proofs
+# Verify Coq proofs: build, then the Print Assumptions gate and its control
 verify-coq: build-coq
-    @echo "✓ Coq proofs verified"
+    bash proofs/coq/check-assumptions.sh
+    bash proofs/coq/check-assumptions.sh --control
+    @echo "✓ Coq proofs verified (17 named theorems closed under the global context)"
 
-# Verify Z3 SMT properties (CNO checks + OND bounded instances)
+# Verify Z3 SMT properties: every (check-sat) verdict must match its `; expect` annotation (no skip-as-pass)
 verify-z3:
     @echo "Verifying Z3 SMT properties..."
-    @if command -v z3 >/dev/null 2>&1; then \
-        sh proofs/z3/verify.sh && z3 proofs/z3/ond/OND_checks.smt2 && echo "✓ Z3 verification complete"; \
-    else \
-        echo "⚠ z3 not found, skipping Z3 verification"; \
-    fi
+    @command -v z3 >/dev/null 2>&1 || { echo "✗ z3 not found (required, not skipped)"; exit 1; }
+    bash proofs/z3/verify.sh
+    @echo "✓ Z3 verification complete"
 
 # Verify Lean 4 proofs
 verify-lean:
@@ -116,6 +116,10 @@ verify-isabelle: build-isabelle
 verify-mizar: build-mizar
     @echo "✓ Mizar proofs verified"
 
+# Self-test the prover gate: stubbed toolchains + z3 mutants must turn it red
+verify-gate-selftest:
+    bash proofs/tests/gate-selftest.sh
+
 # Verify the Idris 2 ABI package
 verify-idris: build-idris
     @echo "✓ Idris ABI verified"

PROOF-STATUS.adoc

@@ -17,6 +17,13 @@ All six provers are installed and were *reproduced in this environment*. A singl
 gate, `proofs/verify-all-provers.sh`, builds every prover and prints
 `ALL-PROVERS-GREEN`: *Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar*,
 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`). 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)
@@ -82,9 +89,15 @@ of these, each documented in-file with its blocker:
   `nat -> C` single-qubit model; faithful discharge is a separate formalisation.
 
 These are the analogue of the OND-6 research fork: openly labelled, not silently
-assumed. `Print Assumptions` on every headline theorem shows only Coq stdlib axioms
-(`ClassicalDedekindReals.*`, `functional_extensionality*`) plus, where relevant, the
-explicitly-tagged postulate above — never a hidden project axiom.
+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`, 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
+and/or the tagged parameters — see #171 for the census and the tag-grammar work.
 
 === Reversibility <-> CNO bridge (2026-07-16, the theorem MAA cites)
 
@@ -151,8 +164,11 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
 
 == Agda — VERIFIED (this environment)
 
-* `agda` 2.6.3, `--safe --without-K`: `CNO.agda`, `OND.agda`, `EchoBridgeCNO.agda`
-  type-check. The EchoBridge modules take **funext as an explicit hypothesis**
+* `agda` 2.6.3 (CI) / 2.6.4.3 (local), `--safe --without-K`: `CNO.agda`, `OND.agda`,
+  `EchoBridgeScaffold.agda`, `EchoBridgeCNO.agda` type-check; every file carries the
+  `{-# OPTIONS --safe --without-K #-}` pragma and CI (`proofs.yml`) checks all four. Until
+  2026-09-23 CI checked only the first two and `EchoBridgeCNO.agda` had no pragma of its
+  own. The EchoBridge modules take **funext as an explicit hypothesis**
   (not a global `postulate`); `OND.agda` uses zero postulates.
 
 == Lean 4 — VERIFIED (this environment)
@@ -225,3 +241,7 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
 * Remaining axioms are exactly: (a) tagged physical postulates (the honest metal
   boundary), and (b) the class-A items listed above (true, provable in principle,
   openly labelled). No headline theorem depends on a hidden project axiom.
+* Measured 2026-09-23: the 17 named theorems are closed under the global context
+  (CI-gated); of all 182 top-level theorems, 109 are closed and 73 rest on stdlib
+  classical axioms and/or the tagged parameters. The "exactly" in the bullet above is
+  not yet machine-checked — the tag grammar is unified under #171.

proofs/agda/EchoBridgeCNO.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --safe --without-K #-}
+
 -- Concrete Echo/CNO instantiation against CNO.Program and CNO.eval.
 --
 -- Primary bridge: use CNO.state-eq directly as the relation in EchoRel.

proofs/coq/audit/Assumptions.v

@@ -0,0 +1,30 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Print Assumptions audit over the theorems PROOF-STATUS.adoc names.
+
+   NOT listed in _CoqProject: proofs/coq/check-assumptions.sh compiles this file
+   after the theories are built and FAILS unless every line below prints
+   "Closed under the global context" (no stdlib axiom, no project axiom).
+   Add a line here whenever PROOF-STATUS starts naming a theorem; the checker
+   counts the "Print Assumptions" lines, so a theorem cannot be dropped silently.
+   Measured 2026-09-23: 17/17 closed (Coq 8.18). *)
+Require CNO.CNO.
+Require CNO.FilesystemCNO.
+Require CNO.LambdaCNO.
+Require CNO.OND.
+Print Assumptions CNO.CNO.cno_equiv_seq_empty_of_reverses.
+Print Assumptions CNO.FilesystemCNO.create_unlink_inverse.
+Print Assumptions CNO.LambdaCNO.eta_equivalence.
+Print Assumptions CNO.CNO.eval_app.
+Print Assumptions CNO.CNO.eval_deterministic.
+Print Assumptions CNO.FilesystemCNO.mkdir_idempotent.
+Print Assumptions CNO.FilesystemCNO.mkdir_not_identity.
+Print Assumptions CNO.FilesystemCNO.mkdir_rmdir_inverse.
+Print Assumptions CNO.FilesystemCNO.rename_inverse.
+Print Assumptions CNO.CNO.reverses_seq_computes_identity.
+Print Assumptions CNO.CNO.reversible_bridge_backward_upto.
+Print Assumptions CNO.CNO.reversible_bridge_forward.
+Print Assumptions CNO.CNO.reversible_iff_exists_reverses.
+Print Assumptions CNO.OND.skip_program_is_core_CNO.
+Print Assumptions CNO.FilesystemCNO.snapshot_restore_identity.
+Print Assumptions CNO.FilesystemCNO.transaction_cno.
+Print Assumptions CNO.OND.writer_program_not_core_CNO.

proofs/coq/check-assumptions.sh

@@ -0,0 +1,66 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Absolute Zero — Print Assumptions gate for the Coq pillar.
+#
+# Compiles audit/Assumptions.v (or the file given as $1) against the built
+# theories, using the -R roots from _CoqProject, and FAILS unless every
+# `Print Assumptions` line answers "Closed under the global context":
+#   - any "Axioms:" block            -> FAIL (the block is printed);
+#   - closed-count != line-count     -> FAIL (a theorem silently missing);
+#   - coqc exit != 0                 -> FAIL (a renamed/removed theorem);
+#   - a file with no Print Assumptions lines -> FAIL (vacuous gate).
+# `--control` proves the gate bites: it audits CNO.StatMech.landauer_limit_positive,
+# which rests on the tagged axiom PhysicsConstants.kB_positive, and requires
+# the gate to REJECT it naming that axiom.
+# Run after `coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all`.
+set -uo pipefail
+HERE="$(cd "$(dirname "$0")" && pwd)"
+
+command -v coqc >/dev/null || { echo "ASSUMPTIONS-CHECK FAILED: coqc not on PATH"; exit 1; }
+RFLAGS=()
+while read -r flag dir ns; do
+  [ "$flag" = "-R" ] && RFLAGS+=("-R" "$HERE/$dir" "$ns")
+done < "$HERE/_CoqProject"
+[ "${#RFLAGS[@]}" -gt 0 ] || { echo "ASSUMPTIONS-CHECK FAILED: no -R roots in _CoqProject"; exit 1; }
+
+# check_file <file.v>: compile an audit with at least one Print Assumptions command.
+# Print the Coq output and remove generated artefacts beside the audit file.
+# Succeed only if compilation succeeds, no axiom blocks appear, and the number
+# of closed results matches the number of Print Assumptions commands.
+check_file() {
+  local file=$1 base dir out rc expected closed axioms
+  base="$(basename "${file%.v}")"; dir="$(dirname "$file")"
+  expected=$(grep -c '^Print Assumptions' "$file")
+  if [ "$expected" -eq 0 ]; then
+    echo "ASSUMPTIONS-CHECK FAILED: $file has no 'Print Assumptions' lines (vacuous)"; return 1
+  fi
+  out="$(coqc "${RFLAGS[@]}" "$file" 2>&1)"; rc=$?
+  rm -f "$dir/$base.vo" "$dir/$base.vos" "$dir/$base.vok" "$dir/$base.glob" "$dir/.$base.aux"
+  printf '%s\n' "$out"
+  if [ "$rc" -ne 0 ]; then echo "ASSUMPTIONS-CHECK FAILED: coqc exit $rc on $file"; return 1; fi
+  closed=$(printf '%s\n' "$out" | grep -c '^Closed under the global context')
+  axioms=$(printf '%s\n' "$out" | grep -c '^Axioms:')
+  if [ "$axioms" -ne 0 ] || [ "$closed" -ne "$expected" ]; then
+    echo "ASSUMPTIONS-CHECK FAILED: $file — expected $expected closed, got closed=$closed axiom-blocks=$axioms"
+    return 1
+  fi
+  echo "ASSUMPTIONS-CHECK OK: $expected/$expected theorems closed under the global context ($file)"
+}
+
+if [ "${1:-}" = "--control" ]; then
+  tmp="$(mktemp -d "${TMPDIR:-/tmp}/az-assumptions-control.XXXXXX")"
+  trap 'rm -rf "$tmp"' EXIT
+  printf 'Require CNO.StatMech.\nPrint Assumptions CNO.StatMech.landauer_limit_positive.\n' > "$tmp/Control.v"
+  if check_file "$tmp/Control.v" > "$tmp/control.log" 2>&1; then
+    echo "ASSUMPTIONS-CONTROL FAILED: landauer_limit_positive (rests on kB_positive) PASSED the gate"
+    cat "$tmp/control.log"; exit 1
+  fi
+  if ! grep -q 'kB_positive' "$tmp/control.log"; then
+    echo "ASSUMPTIONS-CONTROL FAILED: the rejection did not name PhysicsConstants.kB_positive"
+    cat "$tmp/control.log"; exit 1
+  fi
+  echo "ASSUMPTIONS-CONTROL OK: landauer_limit_positive rejected, naming kB_positive (the gate bites)"
+  exit 0
+fi
+
+check_file "${1:-$HERE/audit/Assumptions.v}"