F-PROVE-007 asserts 297 compile-time proofs against a tree that generates 578, and never executes #2732

Assimilated from #2728 · child of #2706 (APR-PERF-GATE-001, the receipt rule)

Behaviour

f_prove_007_proof_count_is_exactly_297 asserts the tree contains exactly 297 compile-time proofs. The tree generates 578. The assertion has never fired, because the file it lives in is compiled out by default — and the only two targets that would compile it in report success unconditionally.

Two independent failures: it does not run, and it would fail if it did.

Reproduction

It does not run

$ cargo test -p aprender-core --test falsification_spec_v10_tests f_prove_007
rc=0
running 0 tests
test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

crates/aprender-core/tests/falsification_spec_v10_tests.rs:16 — #![cfg(feature = "model-tests")] gates all 138 tests in the file.

It would fail if it did

$ cargo test -p aprender-core --features model-tests --test falsification_spec_v10_tests f_prove_007
rc=101

thread 'f_prove_007_proof_count_is_exactly_297' panicked at
crates/aprender-core/tests/includes/falsification_spec_v10_contract_model.rs:259:5:
assertion `left == right` failed: F-PROVE-007: Expected 297 proofs, found 578
  left: 578
 right: 297

Ground truth, counted directly out of the build directory:

$ grep -c "const _: () = assert!" \
    /mnt/nvme-raid0/targets/aprender/release/build/aprender-core-*/out/model_families_generated.rs
578    # identical across all generated copies

Nothing that would run it can report failure

model-tests appears nowhere in .github/. It appears twice in the Makefile, and both targets exit 0 no matter what happens:

$ make test-spec
rc=0
🔬 Running spec structural tests...
✅ Spec tests complete          # ran zero tests

$ make test-model
rc=0
  ❌ f_ollama_001 FAILED
  ❌ f_ollama_002 FAILED
  ...  (all 10)
✅ Model tests complete

Two compounding causes:

1. Neither passes -p aprender-core (Makefile:113, Makefile:121). From the workspace root, cargo test --features model-tests resolves the feature against the root aprender facade, which does not define it:
   error: the package 'aprender' does not contain this feature: model-tests.
   No test is ever compiled, let alone run.
2. .ONESHELL: (Makefile:20) with no set -o pipefail and no set -e. The whole recipe runs as one bash script, so the recipe's exit status is its last command — which in both targets is a decorative @echo "✅ ...". The cargo … 2>&1 | grep "test result:" pipeline already discards cargo's rc=101 in favour of grep's status, and even grep's non-zero is then overwritten by the trailing echo.

make test-model additionally prints ❌ … FAILED ten times and still exits 0 — the failure is visible on stdout and invisible to the exit code.

This is the feedback_verification_discipline rule 1 and the pass-grep class, in the one lane that would have caught the stale constant.

Which number is wrong

Not established here, and the fix should not assume. CLAUDE.md and #2728's H0-064 both claim 297; build_codegen.rs emits 578. Either the generator gained proofs nobody re-baselined, or the constant was aspirational. Whichever it is, the constant must be derived or explicitly re-baselined with a dated note — not silently bumped to 578 to make the test green. Bumping it to match the current output reproduces the original defect one commit later.

RED-turning mutation to register

1. Un-dark it. Fix Makefile:113,121 to pass -p aprender-core, and make both recipes fail-closed: capture ${PIPESTATUS[0]} (or drop the pipe) and drop the unconditional trailing echo "✅", or add set -euo pipefail at the top of the ONESHELL recipe.
   Mutation: point the recipe at a test known to fail. make test-spec must exit non-zero. It currently exits 0 — so run this mutation first, against the current Makefile, to confirm the target is presently unable to red.
2. Re-baseline F-PROVE-007 to the decided value, with the derivation recorded next to the constant.
3. Mutation on the assertion: change the expected count by ±1. cargo test -p aprender-core --features model-tests --test falsification_spec_v10_tests f_prove_007 must go RED. Revert; confirm GREEN.
4. Discrimination: the corrected test must pass on an unmodified tree — a gate that flags everything is as broken as one that flags nothing.
5. Wire the structural (non-model, non-GPU) subset into a lane that actually runs. Note the standing trap: a suite gated only in the Makefile is invisible to ci.yml.

Why this belongs to #2706

F-PROVE-007 is a receipt for a claim the project publishes: "297 compile-time algebraic invariant proofs" (CLAUDE.md, #2728 H0-064, SHOWCASE-BRICK-001 §16). The receipt has never been checked, disagrees with the artifact by 281, and the lane that would check it ends in echo "✅". That is the epic's thesis in miniature.