P13-S29 RATIFIED; pins frozen, dispatched

Graph invariant 10 reported Chapter 3 and Chapter 4 failures under its own
number, through a public API: check_invariant is pub and re-exported, and
Display rendered a tempo rule as "invariant 10 (CrossCuttingRefsResolve)
violated". Disposition (b), type-neutral: InvariantViolation becomes
WellFormednessViolation carrying a two-armed ViolationKind. check_invariants
stays comprehensive, so every broad caller keeps its rule coverage; the
deliberate behaviour change is that check_invariant narrows to the invariant
arm, with a symmetric check_requirement added. GraphInvariant does not move --
21 variants, unchanged, and no new negative generator or shrink obligation.

req:time:tempo-segment-shape is minted for the one rider that had no label,
stating the enforced shape/end_tempo compatibility without resolving P13-S8's
canonical-form question, so the label survives whichever spelling S8 ratifies.

Eighteen review rounds. Four mutation radii were measured against disposable
implementations rather than derived, and every one of the four differed from
what static reading predicted: M2a by ten false positives and seventeen
omissions, M17-C1 by naming seven where eighteen fail and including a test that
belongs to C2, M17-C2 and C3 by predicting observers that measurement put at one
and zero. Two of those measurements first produced a compile error reporting
zero failures -- a compile error observes nothing -- and one misread cargo test's
"error: test failed" as a compilation signal; only the third method is pinned.

Several defects were structural rather than arithmetic. Both selectors could
have matched their arm while ignoring their payload, satisfied by every fixture
presenting a single variant or label. A complete third ViolationKind arm, or a
fully implemented 22nd GraphInvariant omitted from all(), compiles and leaves
every gate green -- a variant nothing enumerates is a variant nothing observes.
The accidental tests identified their rule by a witness suffix this rung
deletes, so a selector-only migration would have left two negatives green and
vacuous. And invariants.rs:8 carries the old type name in retained header prose,
which would have made gate 6 unsatisfiable.

Prerequisite review scaffolding, applied earlier under a narrow authorization
and committed here because ratification is what changes its staging state: one
temporary DISCUSSED_NOT_CITED row for req:time:tempo-segment-shape, deleted by
pin 3 when the requirement lands, with landing gates for its absence and for the
baseline being green because the label is defined rather than still allowlisted.

Baseline unchanged at 43 suites, 1586 passing; no implementation target has been
modified.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
This commit is contained in:
Levi Neuwirth 2026-08-12 00:05:32 +02:00
parent 3fda93bc6b
commit cea21cd8f9
No known key found for this signature in database
2 changed files with 1687 additions and 0 deletions

View File

@ -397,6 +397,16 @@ const DISCUSSED_NOT_CITED: &[(&str, &str)] = &[
spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md and recorded in \
spec/EVIDENCE_P13S26_EXECUTION.md as M6's verbatim diagnostic. PERMANENT.",
),
(
"req:time:tempo-segment-shape",
"proposed by spec/CONTRACT_P13S29_VIOLATION_KIND.md; the requirement does not \
exist until that contract's pin 3 lands. TEMPORARY -- pin 3 REMOVES this row \
when it mints the requirement, because this row's own claim (discussed, never \
cited) becomes false at that moment. A stale row is inert, so nothing else \
will catch it; that contract's landing gate does. Remove by hand if S29 is \
abandoned or the label changes. Prerequisite review scaffolding, NOT dispatch: \
it licenses no other pin work.",
),
];
fn requirement_strings(text: &str) -> BTreeSet<String> {

File diff suppressed because it is too large Load Diff