spec: J3 checked over every build of four files, not argued (#179)

[lex00]

Closes #179, by a different instrument than it proposed. Reasoning below — redirect me if you disagree.

The gap it names

The J3 proposition is the one place the project asserts instead of gating […] it currently contains two defects in nine lines.

That's right. Coverage is checked both directions, UNCOVERED.md is shrink-only, corpus.test.ts has three anti-vacuity assertions. J3's proposition had prose, and #180 found two defects in it by reading.

Not Alloy

#179 proposed an Alloy model. The method is the thing, not the tool — as the issue itself puts it, "Alloy does not read proofs, it checks claims". Bounded exhaustive enumeration does exactly that, runs in the suite everything else runs in, and adds no Java toolchain to CI.

Scope, stated the way F-Depth's bounds are: every build of four files — every import relation excluding self-imports, every capture relation inside it, every assignment of J2 tentative verdicts. 8,503,056 builds, verified as exactly 3^(n²−n) × 2^n. A cycle, a diamond, and a chain of three with a capture across it all fit inside four. Runs in 3.4s.

What is checked

• T(B) is closed under Succ
• a running file never leaves a folded file below it — the forward edge
• a capturer never outlives what it captured from — the backward edge
• no running file holds a second object of a folded file's entity — the proposition in case 1's form

Four vacuity guards

The instance #179 asks for by name. A file that imports a running module and never references the binding still folds. Taint flows from a tainted file to what it imports, never to its importers — so this must exist, and case 2 of the sketch asserted the opposite (#180's second defect). A model that cannot produce it isn't modelling this specification.

Each edge is load-bearing. Delete the forward edge and a check fails; delete the backward edge and a different one fails. Neither is decorative.

The lemma is load-bearing. f ⇝ g implies f → g is stated in taint.md and never checked. The model exhibits the build it excludes: a capture that is not an import, where the capturer runs and reconstructs the entity while the captured-from file still folds and holds its own. Two objects for one entity, which is what the proposition forbids.

One implementation note

The first version called expect() inside the enumeration and took longer than a 10-minute timeout. Relations are bitmasks now and each check collects counterexamples for a single assertion — three seconds instead of minutes. Worth knowing if anyone widens the scope later.

taint.md gains three lines pointing at the check and its scope.

Verification

121 tests in 19 files, typecheck clean, voice gate clean, prose lint 51 with no regressions, npm run docs:build clean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AzfJnYw9p6rAxhJqXK3CPv