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
Filed ahead of execution so the contract is under version control before any
agent touches it. This session already learned the other way round: the G3b
contract sat untracked past a "clean" gate, because git diff --check cannot see
a file that never reached the index, which is why this contract's own section 5
mandates git diff --cached --check instead.
The rung it scopes is diagnostic. Invariant 20 has nine non-success paths, not
the three P13-S18 records; only three are abstentions. Two are delegated to
invariant 10, two are vacuous, one is inapplicable, one is P13-S19. The rung
builds an 18-cell outcome matrix, classifies every path, corrects the ledger and
two drifted citations in the G3b contract, and files P13-S23 for the capability
everything defers to. No behaviour change: the gate requires
check_measure_meter_consistency's executable body to stay byte-identical, and a
finding that suggests changing which graphs violate invariant 20 stops the rung
rather than being implemented in it.
Six review rounds are recorded in the pins as corrections, not smoothed away.
Successive drafts scoped the residue at five paths then nine; called the
Measure-end claim false, then misattributed, before landing on conditionally
false; conflated two distinct WallClock shapes whose clauses fail differently;
and scoped P13-S23 twice too narrowly, the second time excluding B5 -- comparable
pairs that yield no delta -- which is a third of what it is filed to own.
Baseline 1541/0 confirmed at f33673d. The commits since cc49533 are spikes/-only,
a separate workspace, so the root count is unmoved and the section 0 readings
stand.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV
Levi Neuwirth