`Proofs` is not a gate: `paths: proofs/**` filter, `z3 … || true`, Isabelle/Mizar skipped without failing, no assumption check in CI

[hyperpolymath]

Scope: the Coq/Agda/Z3/Isabelle/Mizar orchestration. The Lean leg (FilesystemCNO/LambdaCNO derive False; never run in CI) is #125; Coq axiom and Idris believe_me debt is #70; the Idris postulates are #27. None of that is duplicated here.

Measured (2026-09-22, main = 74202cb)

• .github/workflows/proofs.yml:20–26 paths: ['proofs/**'] on push and pull_request: a change to the workflow itself, to Justfile, or to any prover config outside proofs/ never runs the proofs. The workflow is absent from the last 12 runs on main.
• proofs.yml:94 sh proofs/z3/verify.sh || true: the Z3 CNO checks cannot fail the job. :95 z3 proofs/z3/ond/OND_checks.smt2 can, but only by exit code, never by asserting unsat/sat text.
• proofs/verify-all-provers.sh:41–53: Isabelle and Mizar print "(skipped)" when absent and do not set fail=1, so the script can say green on 4 of 6 provers. Z3, and Isabelle when present, do set fail=1.
• proofs.yml:80–82 type-checks only CNO.agda and OND.agda (the third file, EchoBridgeCNO.agda, is EchoBridgeCNO.agda has no --safe --without-K pragma and is not checked by proofs.yml, while PROOF-STATUS:154 says it type-checks under --safe #162).
• No Print Assumptions (Coq) or #print axioms (Lean) step exists anywhere in CI. The Coq side carries 37 live Axiom/Parameter declarations, 13 tagged METAL-BOUNDARY (proof-debt: triage matches proven#107 overly-cautious-OWED pattern — 17 Coq axioms + 5 Idris believe_me's discharge candidates #70 tracks the debt itself); "closed under the global context" is prose until a run prints the list.

Why it matters

A workflow that does not run on the commits that change it, cannot fail on the checks that matter, and never prints its assumptions is a green square with no predicate behind it.

Acceptance criteria

1. The paths: filter is removed, or widened to include .github/workflows/proofs.yml, Justfile, *.agda-lib, _CoqProject, lakefile*, so the workflow runs on every push to main. Watched-failing → green: it appears in gh run list -b main for the fix commit.
2. || true removed at :94; the Z3 step asserts the expected unsat/sat lines from verify.sh output, not just exit 0.
3. verify-all-provers.sh sets fail=1 when a prover is absent unless the caller sets an explicit SKIP_ISABELLE=1 / SKIP_MIZAR=1; CI sets neither. Mutant: with isabelle off PATH and no skip variable, the script exits non-zero.
4. An assumption step: coqchk plus Print Assumptions <headline theorem>. for each headline theorem, with the output asserted to list only the METAL-BOUNDARY axioms; the CI log shows the lists.
5. Ordering per owner ruling D-3 (2026-09-22): Lean FilesystemCNO and LambdaCNO each prove False; lake build reports success and CI never runs the Lean leg #125 is fixed first; this issue's items follow it (Phase 4b–4c of the residual-evidence-types family plan).

🤖 Generated with Claude Code

[hyperpolymath]

Additional consequence measured 2026-09-22T22:46Z while landing #165: because proofs.yml is path-filtered to proofs/**, absolute-zero-abi.ipkg and itself, none of its jobs (Coq — CNO + OND (14 theories), Agda — CNO + OND, Z3 — CNO + OND bounded checks) can ever be listed in ruleset 18110203's required_status_checks: a PR that touches nothing under proofs/ would never report the check, and the rule is strict_required_status_checks_policy: true, so it would block forever. Proofs has 0 runs on main among the last 12 workflow runs.

Acceptance criterion to add: the workflow triggers on every pull_request and push to main with no paths: filter; each job decides internally (a paths-filter-free git diff --name-only step or an always-true run) so that it reports success cheaply on non-proof PRs and runs the provers when proofs/** changed. Only then can the three prover jobs be added as required checks.

🤖 Generated with Claude Code