# Five of seven INV falsifiers did not falsify anything

_2026-09-22 · booth_

The U4 contract carried seven invariants, each with a *Falsifiable:* line, and
each had a test. **The code-review panel showed that five of the seven tests
would still pass under a change that defeats the invariant they name.** Gróa's
"per INV entry, what would still pass" section is the single most useful thing
either panel produced on this unit.

| INV | what the test asserted | what still passed |
|---|---|---|
| 1 (no new arithmetic) | the clock moved after a view | special-casing `.viewed` inside `_newest_mtime` — the exact new arithmetic INV-1 forbids |
| 3 (`is_held` is pure) | the right answer, once | `is_held` doing I/O, or `return True` unconditionally |
| 4 (every surface says why) | a substring on `GET /` | dropping the line from the booth header, the marks page, or the board branch |
| 5 (a view cannot fail a request) | `record_view` did not raise | a second `touch` outside the guard, 500ing all three routes |
| 6 (unreadable marks hold) | the corrupt booth survived | a sweeper that deletes nothing at all (no doomed sibling in the fixture) |
| 7 (machine reads do not hold) | `.viewed` was absent | a handler writing any other non-dot file, holding the booth open just as well |

**The shape of the error is the same every time: the test asserted the OUTCOME
the author was thinking about, not the DISCRIMINATOR the invariant names.** A
green test proved the happy path and nothing about the invariant. Writing the
falsifiable line in the contract did not produce a falsifying test — it produced
a test that *cited* one.

Fixed by rewriting each to fail under the change that defeats it: same-mtime
equivalence with an arbitrary non-lock dotfile (plus a `.lock` that must NOT
count); `is_held` called with marks belonging to a booth that does not exist on
disk; one test per rendered surface, each rendering only its own; the three
routes GET against a chmod'd booth; a doomed sibling; the AGE asserted rather
than the marker. **The board-header pair was verified RED against the pre-fix
template rather than assumed** — which is the step that makes "fixed, not
amended" trustworthy.

**The method to keep: for each invariant, name a change that defeats it and ask
whether the test goes red.** If you cannot name one, the invariant is not
falsifiable yet. Regin and Kimi independently proposed this as a contract-time
"vacuity pass"; heid rates this round the strongest evidence for it so far, and
it is a `/heid*` skill proposal sitting with the operator, not a change to this
repo.