`proof-runner-check` composite prints 'All detected proofs executed successfully' with every command commented out (vacuous gate)

[hyperpolymath]

Measured (2026-09-22, main = 3b4afaf)

• actions/proof-runner-check/action.yml, step Run Formal Proofs: :9 echo "Executing Formal Proofs..."; :12 if [ -f "*.ipkg" ] || [ -d "src" ] (a quoted glob tests the literal filename *.ipkg); :15 # idris2 --typecheck *.ipkg || exit 1 (commented out); :19 the Lean/Coq/Agda branch is a comment; :21 echo "All detected proofs executed successfully." unconditionally.
• Consumers: main-estate-audit.yml step 14, every estate repo that calls the audit, and the residual-evidence-types rescue branch's local copy of the same composite (which is why the residual family plan refused to merge it always-green).
• Estate vacuous-gate doctrine (2026-09-21): no gate may print a success line it did not earn.

Acceptance criteria

1. The composite detects the toolchains present (*.ipkg, lakefile*, *.agda-lib, _CoqProject, ROOT) and runs the real command for each, failing on non-zero. If none is present it prints "no proof toolchain detected" and reports a skip as a distinct, visible outcome, never "executed successfully".
2. Watched-failing → green: grep -c 'All detected proofs executed successfully' actions/proof-runner-check/action.yml is 1 today, 0 after.
3. Mutant: a caller with a deliberately failing module (residual-evidence-types has tests/reject/*.agda that must be rejected; wire one as if it were a positive module) turns the composite red. A passing self-test proves nothing until the mutant dies.
4. Or: the composite is deleted, step 14 removed from the audit, and the audit's gate count corrected.

🤖 Generated with Claude Code