Independent review of 25473a1 returned two blocking findings. A sweep
escalated one of them into a third. Both reported findings are the same
failure in different clothes: a requirement stated with nothing able to fail
it.
1. Pin 10a still deferred the label decision to execution -- twice reworded,
never decided. The facts were readable in the .tex source the whole time:
core_spec.tex:6529-:6648 is ONE requirement box carrying the single label
req:graph:score-graph-invariants, with exactly 20 \items inside it.
Invariant 21 is a 21st \item within that box, so pin 6 mints nothing. Pin
10 rewrites prose plus a Revision History row and version bump, so it mints
nothing either.
DECIDED: neither document mints a label; touch row 11 is UNUSED and must
not be staged; no counter moves. If execution finds otherwise that is a
finding against this contract, not a keyboard decision. The counter table
is retained for that case and for the next rung. Row 11 is kept rather than
deleted because CLAUDE.md names the file as a recurring escapee -- a row
reading "deliberately unused, and why" survives review; an absent row looks
like an oversight.
"Decide and report" reads like rigour and is its opposite: it makes the
staged set and counter expectations depend on a choice made at the
keyboard, so the touch table can be wrong in either direction and the
report will agree with whatever happened.
2. Pin 6a required each fixture to violate its own direction only, and nothing
could observe that. The prescribed model, m40, asserts only
check_invariants(&s).iter().any(...) -- any() cannot see a second unrelated
defect -- and gate 6 checked the target verdict and the opposite direction
but never the absence of invariants 1-20. So a fixture carrying an
unrelated second defect satisfied every stated gate and mutation outcome.
Each m41/m41b must now assert the EXACT violation set: exactly one
violation, StaffGroupMembershipAgreement, witness naming that direction's
staff and group ids, opposite direction asserted satisfied. Gate 6 reports
check_invariants' full return for both.
Borrowing a test's shape imports its blind spots along with its virtue. m40
was cited for its dispatch property, which is real and still applies;
nothing about invariant 20 ever turned on exactness.
3. Sweep: the same blind spot covers touch row 8's generator, and worse.
negative_generators_are_reasonably_targeted bounds kinds:
BTreeSet<GraphInvariant> at <= 3, but both directions of invariant 21 are
the SAME variant -- they collapse to one element, so no existing test can
observe direction at all; the other three all() loops assert only
!is_empty(). Row 8 now requires a dedicated permanent test that the
generator violates S->G and not G->S.
Also fixed: revision D's block was first inserted inside revision C's,
orphaning C's closing paragraphs after it. Reordered, and the cross-revision
pattern paragraph moved to the end and extended.
That paragraph now carries rev D's converse: the fix-every-site rule asks who
READS a corrected rule; rev D asks what OBSERVES each requirement. Findings 2
and 3 were invisible to every sweep that looks for restated text, because
nothing was restated. A rule with no consumer goes stale; a rule with no
observer was never enforced at all.
Still DRAFT, still unratified. No implementation work has begun.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
Levi Neuwirth
cae1d32794