Invariant 20 has nine non-success paths, not the three P13-S18 recorded. Only
three are abstentions: agreement-Indeterminate, boundary-Indeterminate, and an
incomputable boundary delta. Two are delegated to invariant 10, two are vacuous,
one is inapplicable, one is P13-S19's pickup deferral. The entry had been
counting all of it as gap.
Delegation is proved, not asserted. Deleting invariant 10's per-measure arm
leaves the condition unreported by the entire workspace suite except by the two
tests that name it; the same holds for the instance-local-grid arm. A delegation
nobody discharges would have been an abstention with a better name.
Every abstention cell carries a paired positive control, because silence is the
same observation for all nine paths. Each test asserts zero violations on the
fixture that takes the claimed path, then changes only that path's dependency
and asserts the clause decides with the expected witness. The control has to
observe the clause the cell names: S8's first version restored the governing
search by moving prev, which broke prev<->x comparability and left the boundary
silent for a second reason, signing the cell by inference. Moving the grid edge
instead keeps both measures c4-comparable and the boundary clause itself fires.
S2 has no such option -- a WallClock delta is never computable -- so its control
legitimately observes prev's agreement, and that exception is S2's alone.
Three shapes claimed a clause pair no single measure exhibited: m0 carried a
resolving signature at index 0 and m1 carried None, so the pair was really
A4+B1 on one measure and A1+B4 on the other. A boolean over the whole invariant
cannot see that, which is how it survived the first pass.
No behaviour change. check_measure_meter_consistency's executable body is
byte-identical to f33673d at 4871 bytes, verified by brace-matching from the
signature rather than a sentinel; every red observation came from fixture data or
from invariant 10, never from invariant 20's own logic.
P11-C5 was never this residue's gate -- it is a re-anchoring proximity metric.
P13-S23 is filed for the real dependency: placing anchor pairs on a common
timeline and measuring musical distance wherever c1-c5 do not already yield
both. It owns two disjoint deficiencies, since c3 and c5 order without
supplying any delta.
Executed against spec/CONTRACT_P13S18_MATRIX.md, 18 cells and 10 mutations.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV
Levi Neuwirth
339269b3cf