P13-S29 LANDED: the violation tag stops multiplexing

Graph invariant 10 reported Chapter 3 and Chapter 4 failures under its own
number, through a public API. `InvariantViolation` becomes
`WellFormednessViolation` carrying a two-armed `ViolationKind`: `Invariant` for
a numbered graph invariant, `Requirement` for a normative rule named by its
`req:` label. Invariant 10 keeps only reference resolution.

`check_invariants` stays comprehensive, so every broad caller keeps its rule
coverage; `check_invariant` narrows to the invariant arm and a symmetric
`check_requirement` is added. Both are projections of the aggregate. Four rules
move to their own labels, one of which this rung mints:
`req:time:tempo-segment-shape`, stating the enforced shape/end_tempo
compatibility without resolving P13-S8. `GraphInvariant` did not move: 21
variants, unchanged.

  44 suites / 1606 passed / 0 failed / 0 ignored   (1586 -> 1606, 43 -> 44)
  clippy -D warnings clean; fmt -p epiphany-core -p epiphany-testkit clean
  core_spec.pdf rebuilt, undefined references cleared

Gates 1-16 pass; evidence in spec/EVIDENCE_P13S29_EXECUTION.md. All 54 mutations
of §3 observed, none compile-only, none passing. Amendment 1 corrected M1·C6 and
M1·C7 from one observer to two after measurement contradicted the derived cell.

Six execution faults are recorded rather than left in the transcript, none a
contract defect. Three are worth naming here because no tool would have caught
them:

- Pin 10's eleventh row was read as a note, not a test, so
  `reversed_aleatoric_bounds_stay_invariant_four` was never written. M11's cell
  named it, and the omission surfaced only as a radius mismatch.
- `display_renders_each_arm_exactly` carried a comment stating its pinned
  fixture correctly above code that built a different one. Pin 10 had foreclosed
  the choice precisely because it moves radii; with the fixture repaired the
  test entered M11's cell and left M17·C1's, both as pinned.
- Pin 9's `/// 10.` rider note was the one prose row left unmigrated, naming
  three labels where four were required and still filing the multiplexing as
  pending. Gate 16 states these outcomes have no machine observer; eight rows
  were verified by their own stale phrase, and the ninth was not there.

Gate 10 rejected the ledger append over one character: the artifact read
2026-08-12 where pin 13 pins 2026-08-11. The artifact was corrected to the pin,
and the date question is flagged for the owner as a possible administrative
amendment rather than settled here.

CLAUDE.md's baseline still reads 43 suites / 1586 tests and is not in the touch
table; it follows in a separate reconciliation commit.

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 16:34:38 +02:00
parent e7bd12c19e
commit 52fcf3739a
No known key found for this signature in database
13 changed files with 1384 additions and 214 deletions

View File

@ -1062,6 +1062,16 @@ underdetermined pitch spaces) — inventing one would itself be the
wired into `check_invariants` as wired into `check_invariants` as
`GraphIndex::check_accidental_modification_compatibility` — the `GraphIndex::check_accidental_modification_compatibility` — the
`req:tuning:accidental-modification-compatibility` invariant `req:tuning:accidental-modification-compatibility` invariant
> **SUPERSEDED 2026-08-12 by P13-S29** (`spec/CONTRACT_P13S29_VIOLATION_KIND.md`).
> Calling this an *invariant* was accurate about the tag it borrowed and wrong
> about what it is: a Chapter 4 requirement reported under a Chapter 5 graph
> invariant's number, through a public API. It now reports
> `ViolationKind::Requirement("req:tuning:accidental-modification-compatibility")`
> and is retrievable through `check_requirement`. **The decision above is left
> as written** — it records why borrowing the tag was defensible when no other
> arm existed, which is what a later reader needs in order to understand why it
> was accepted and then reversed.
(`core_spec.tex:3120`). `space` resolves structurally against (`core_spec.tex:3120`). `space` resolves structurally against
`built_in_position_structure` (Push 4b tranche 1), the same catalog `built_in_position_structure` (Push 4b tranche 1), the same catalog
`Pitch::transposed` uses. The requirement's two named rules (`CmnChromatic` `Pitch::transposed` uses. The requirement's two named rules (`CmnChromatic`

View File

@ -22,7 +22,7 @@ of the core specification (`spec/core_spec.pdf`). This is Agent B's crate per
| Events | the `Event` taxonomy (7 variants) and the `slotmap`-backed `EventArena` | Ch. 5 §"The Event Arena" | | Events | the `Event` taxonomy (7 variants) and the `slotmap`-backed `EventArena` | Ch. 5 §"The Event Arena" |
| Graph | `Canvas`, `Region`, `Staff` vs `StaffInstance`, `Voice`/`VoiceOrigin`, `Measure`, `BarlineAlignmentGroup`, aleatoric `EventOrderingDAG` (acyclic by construction), the full cross-cutting registry, the full top-level `Score` | Ch. 5 | | Graph | `Canvas`, `Region`, `Staff` vs `StaffInstance`, `Voice`/`VoiceOrigin`, `Measure`, `BarlineAlignmentGroup`, aleatoric `EventOrderingDAG` (acyclic by construction), the full cross-cutting registry, the full top-level `Score` | Ch. 5 |
| Indexes | `ScoreIndexes`: the four mandatory indexes (event-time, cross-cutting-reference, measure, spelling-attachment) | Ch. 5 §"Indexes" | | Indexes | `ScoreIndexes`: the four mandatory indexes (event-time, cross-cutting-reference, measure, spelling-attachment) | Ch. 5 §"Indexes" |
| Invariants | `check_invariants` over all 19 enumerated graph invariants, with a typed `InvariantViolation` witness per check | Ch. 5 §"Graph Invariants" | | Invariants | `check_invariants` over all variants returned by `GraphInvariant::all()`, with a typed `WellFormednessViolation` witness per check | Ch. 5 §"Graph Invariants" |
| Generators | `generators::valid_score`/`valid_score_rich` (positive), `violating_score` (negative, per invariant), `shrink` (witness minimizer) | QUICKSTART, Agent B hand-off | | Generators | `generators::valid_score`/`valid_score_rich` (positive), `violating_score` (negative, per invariant), `shrink` (witness minimizer) | QUICKSTART, Agent B hand-off |
## The identity discipline this crate enforces ## The identity discipline this crate enforces

View File

@ -976,6 +976,7 @@ pub fn shrink(score: &Score, inv: GraphInvariant) -> Score {
mod tests { mod tests {
use super::*; use super::*;
use crate::check_invariants; use crate::check_invariants;
use crate::invariants::ViolationKind;
#[test] #[test]
fn positive_corpus_runs_clean() { fn positive_corpus_runs_clean() {
@ -1092,7 +1093,8 @@ mod tests {
else, got {violations:?}" else, got {violations:?}"
); );
assert_eq!( assert_eq!(
violations[0].invariant, inv, violations[0].kind,
ViolationKind::Invariant(inv),
"{leg}: the single violation must be invariant 21, got {violations:?}" "{leg}: the single violation must be invariant 21, got {violations:?}"
); );
assert!( assert!(
@ -1171,8 +1173,11 @@ mod tests {
for inv in GraphInvariant::all() { for inv in GraphInvariant::all() {
let s = violating_score(inv, 99); let s = violating_score(inv, 99);
let all = check_invariants(&s); let all = check_invariants(&s);
let kinds: std::collections::BTreeSet<_> = all.iter().map(|v| v.invariant).collect(); let kinds: std::collections::BTreeSet<_> = all.iter().map(|v| v.kind).collect();
assert!(kinds.contains(&inv), "{inv:?} not among {kinds:?}"); assert!(
kinds.contains(&ViolationKind::Invariant(inv)),
"{inv:?} not among {kinds:?}"
);
assert!( assert!(
kinds.len() <= 3, kinds.len() <= 3,
"{inv:?} corruption fired too many invariants: {kinds:?}" "{inv:?} corruption fired too many invariants: {kinds:?}"

File diff suppressed because it is too large Load Diff

View File

@ -181,6 +181,6 @@ pub use codec::{CanonicalValue, ScoreDecodeError};
pub use indexes::ScoreIndexes; pub use indexes::ScoreIndexes;
pub use invariants::{ pub use invariants::{
check_invariant, check_invariants, deferred_checks, measure_anchor_relation, DeferredCheck, check_invariant, check_invariants, check_requirement, deferred_checks, measure_anchor_relation,
GraphInvariant, InvariantViolation, DeferredCheck, GraphInvariant, ViolationKind, WellFormednessViolation,
}; };

View File

@ -0,0 +1,17 @@
//! P13-S29 pin 1b: the root re-export has an observer.
//!
//! An integration test, not a unit test: a unit test inside the crate reaches
//! `invariants::` regardless of what the root re-exports, so only a consumer
//! outside the crate can observe touch row 2 at all.
//!
//! **Type-level only.** It calls nothing. A call whose result were asserted
//! would put this file in M3's and M9's radii; the file stays type-level so the
//! question never arises.
use epiphany_core::{check_requirement, ViolationKind, WellFormednessViolation};
#[test]
fn public_violation_surface_is_reexported() {
let _: fn(&epiphany_core::Score, &str) -> Vec<WellFormednessViolation> = check_requirement;
let _ = |k: &ViolationKind| matches!(k, ViolationKind::Requirement(_));
}

View File

@ -11,7 +11,7 @@ use epiphany_core::{
Pitch, PitchId, PitchSpaceId, PitchSpacePosition, PitchedEvent, RationalTime, Region, Pitch, PitchId, PitchSpaceId, PitchSpacePosition, PitchedEvent, RationalTime, Region,
RegionContent, RegionTimeModel, ReplicaId, ScalePosition, Score, StaffBasedContent, RegionContent, RegionTimeModel, ReplicaId, ScalePosition, Score, StaffBasedContent,
StaffExtent, StaffInstance, StaffLineConfiguration, StemConfiguration, TimeAnchor, TimeExtent, StaffExtent, StaffInstance, StaffLineConfiguration, StemConfiguration, TimeAnchor, TimeExtent,
TuningReference, Voice, WallClockTime, TuningReference, ViolationKind, Voice, WallClockTime,
}; };
use epiphany_core::{Staff, StaffId, StaffInstanceId, VoiceId}; use epiphany_core::{Staff, StaffId, StaffInstanceId, VoiceId};
@ -136,7 +136,7 @@ fn deleting_an_event_from_its_voice_list_is_caught() {
let v = check_invariants(&score); let v = check_invariants(&score);
assert!(v assert!(v
.iter() .iter()
.any(|x| x.invariant == GraphInvariant::EventVoiceBacklink)); .any(|x| x.kind == ViolationKind::Invariant(GraphInvariant::EventVoiceBacklink)));
} }
#[test] #[test]
@ -146,7 +146,9 @@ fn full_invariant_sweep_via_public_api() {
for inv in GraphInvariant::all() { for inv in GraphInvariant::all() {
let bad = generators::violating_score(inv, 0xBEEF); let bad = generators::violating_score(inv, 0xBEEF);
assert!( assert!(
check_invariants(&bad).iter().any(|v| v.invariant == inv), check_invariants(&bad)
.iter()
.any(|v| v.kind == ViolationKind::Invariant(inv)),
"{inv:?} not reported on its negative graph" "{inv:?} not reported on its negative graph"
); );
let shrunk = generators::shrink(&bad, inv); let shrunk = generators::shrink(&bad, inv);

View File

@ -16,12 +16,16 @@ use std::path::{Path, PathBuf};
// spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md) — an aleatoric region's ordering // spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md) — an aleatoric region's ordering
// and bounds references must name events of that same region. Measured at // and bounds references must name events of that same region. Measured at
// execution, never predicted. // execution, never predicted.
const CORE_REQUIREMENT_COUNT: usize = 215; // +1 for req:time:tempo-segment-shape (P13-S29, pin 3:
// spec/CONTRACT_P13S29_VIOLATION_KIND.md) — the tempo rider that had no label.
// Measured at execution, never predicted.
const CORE_REQUIREMENT_COUNT: usize = 216;
// +1 for req:textproj:manifest-schema-carried (G-minor, pins 8/11: // +1 for req:textproj:manifest-schema-carried (G-minor, pins 8/11:
// spec/PLAN_GMINOR_SCHEMA_MINOR.md); +1 for req:format:container-epoch (above); // spec/PLAN_GMINOR_SCHEMA_MINOR.md); +1 for req:format:container-epoch (above);
// +1 for req:time:aleatoric-reference-locality (above). // +1 for req:time:aleatoric-reference-locality (above);
const SUITE_REQUIREMENT_COUNT: usize = 286; // +1 for req:time:tempo-segment-shape (above).
const SUITE_LABEL_COUNT: usize = 286; const SUITE_REQUIREMENT_COUNT: usize = 287;
const SUITE_LABEL_COUNT: usize = 287;
/// The normative chapter-to-area assignment. Keeping this as data makes adding a /// The normative chapter-to-area assignment. Keeping this as data makes adding a
/// requirement under the wrong chapter fail without encoding chapter names in /// requirement under the wrong chapter fail without encoding chapter names in
@ -397,16 +401,6 @@ const DISCUSSED_NOT_CITED: &[(&str, &str)] = &[
spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md and recorded in \ spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md and recorded in \
spec/EVIDENCE_P13S26_EXECUTION.md as M6's verbatim diagnostic. PERMANENT.", 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> { fn requirement_strings(text: &str) -> BTreeSet<String> {

View File

@ -1,11 +1,16 @@
# Contract — P13-S29: the violation tag stops multiplexing # Contract — P13-S29: the violation tag stops multiplexing
STATUS: RATIFIED; DISPATCHED. STATUS: LANDED by this commit.
**Ratified 2026-08-12 on the authority of the repository owner**, the final **Ratified 2026-08-12 on the authority of the repository owner**, the final
whole-artifact review returning zero findings. Review-round records accumulate whole-artifact review returning zero findings. Review-round records accumulate
above §0. above §0.
> **DATED HISTORICAL RECORD — the eighteen review-round blocks above §0 (revisions
> A–R) are an account of what was found and decided between drafting and
> ratification on 2026-08-12. They state no current condition.** The pins as
> ratified are §1's; §6's amendment 1 corrects two of §3's radius cells.
**THE PINS ARE FROZEN. They may be executed, not edited.** A defect found during **THE PINS ARE FROZEN. They may be executed, not edited.** A defect found during
execution is **reported, not patched in place** — if it needs a pin change, that execution is **reported, not patched in place** — if it needs a pin change, that
is its own amendment with its own review round. is its own amendment with its own review round.
@ -1682,7 +1687,11 @@ execution confirms it and any difference is a finding.*
## §6. AMENDMENT 1 — §3's M1·C6 AND M1·C7 RADII, MID-EXECUTION ## §6. AMENDMENT 1 — §3's M1·C6 AND M1·C7 RADII, MID-EXECUTION
STATUS: RATIFIED; FROZEN. Execution of P13-S29 resumes at M2. STATUS: LANDED by this commit.
> **DATED HISTORICAL RECORD — amendment 1 is ratified and executed. §6's finding,
> its defect class and its dispositions are an account of what was found and
> decided on 2026-08-12, and state no current condition.**
Ratified 2026-08-12 on the authority of the repository owner, the final review Ratified 2026-08-12 on the authority of the repository owner, the final review
round returning zero findings. The replacements are executed, not edited; a round returning zero findings. The replacements are executed, not edited; a

View File

@ -354,9 +354,42 @@ suites=44 passed=1604 failed=0 ignored=0
--- ---
## §6. Gate 6 — pin 9's boundary check, verbatim ## §6. Gate 6 — the identifier and field migration, verbatim
*(pending)* **6a. No `InvariantViolation` identifier in Rust code.** Gate 6 scopes this to
`crates/**/*.rs`; the contract, the ledger and this annex quote the old name
historically and are out of scope.
```
$ find crates -name '*.rs' -type f -exec grep -Hn 'InvariantViolation' {} +
$ echo $?
1
```
*Run with `find … -exec`, not a piped `grep | head`: a universal negative from a
truncated pipe is the failure mode `CLAUDE.md` names, and this gate is a
universal negative.*
**6b. No `.invariant` field access on a `WellFormednessViolation`.** Three hits
survive, and gate 6 requires each to be attributed rather than counted:
```
crates/epiphany-core/src/invariants.rs:320: self.invariant.number(),
crates/epiphany-core/src/invariants.rs:321: self.invariant,
crates/epiphany-core/src/invariants.rs:3326: assert_eq!(deferred[0].invariant, GraphInvariant::RegionExtents);
```
**All three are `DeferredCheck`, not the violation type.** Lines 320–321 are
inside `impl core::fmt::Display for DeferredCheck` (opened at `:315`); line 3326
indexes the result of `deferred_checks(&s)`.
**6c. `DeferredCheck.invariant` retained**, as §0.5 requires:
```
crates/epiphany-core/src/invariants.rs:305:pub struct DeferredCheck {
crates/epiphany-core/src/invariants.rs-306- /// The invariant whose decision was deferred.
crates/epiphany-core/src/invariants.rs-310- pub invariant: GraphInvariant,
```
--- ---
@ -465,3 +498,299 @@ they were compared against, not the observation.
The mutation sequence resumes at **M2**. M1 is complete — C4, C5, C8, C9 and C10 The mutation sequence resumes at **M2**. M1 is complete — C4, C5, C8, C9 and C10
matched their dispatched cells, and C6 and C7 match the corrected cells above. matched their dispatched cells, and C6 and C7 match the corrected cells above.
---
## §9. The mutation phase, resumed at M2
**§5 is closed at M1 by the digest gate (contract §6.5c-bis); this section
continues the matrix.** Every row was run as
`cargo test --workspace --no-fail-fast`, preceded by
`cargo build --tests --workspace` checked for `error[` — **a mutation that does
not compile observed nothing** — and restored by hand write-back.
### 9.1 Five more execution faults, none a contract defect
**They are recorded here rather than appended to §3** because §3 is the
pre-amendment record committed at `29ef3af` as amendment 1's oracle. Its count of
five is true as of that commit; these four are later events.
#### 9.1.1 Pin 10's eleventh row was never built
Pin 10's matrix has **eleven** rows. The eleventh is marked `—` rather than a
C-number:
| — | reversed aleatoric bounds | **invariant 4, unchanged** | `reversed_aleatoric_bounds_stay_invariant_four` |
It was read as a note and no test was written. **M11's cell names that test**, so
the omission surfaced as a radius mismatch — expected 4, observed 2 — and not
before.
*A row whose identifier is a dash reads as commentary. The other ten rows carry
C-numbers; the eleventh carries the same three columns and a dash, and only the
columns matter.*
#### 9.1.2 `display_renders_each_arm_exactly`'s invariant side was the wrong fixture
Its comment read:
```rust
// Invariant side: a reversed aleatoric bound (invariant 4), acquired
// from the aggregate -- pinned, because acquisition decides M3's radius.
```
The code beneath it built a **dangling staff instrument** and searched for
`CrossCuttingRefsResolve` — invariant 10, a C1 fixture. **The comment recorded
the pin; the code did something else.**
Pin 10 forecloses exactly this:
> *The choice changes radii, so it cannot be the executor's: a C1 fixture would
> put this test in M17·C1's cell, a tempo-anchor fixture in M17·C2/C3's, and
> reversed bounds put it in **M11's**, which is where it now belongs and where
> M11's cell names it.*
Both halves of that prediction were then observed: with the fixture repaired,
`display_renders_each_arm_exactly` **entered M11's radius** (§9.3) and is
**absent from M17·C1's measured 20** (§9.4). Under the unrepaired fixture it
would have failed M17·C1 too — a second mismatch the first one pre-empted.
*This is the most dangerous of the five fault classes in this rung: a comment
that states the pin correctly next to code that does not. Nothing reads the
comment.*
#### 9.1.3 Pin 3a's guard did not exist
`tempo_segment_shape_requirement_states_its_clauses_and_stays_s8_neutral` was
absent from the tree. **Thirteen mutations target it** — M12pre, M12, M13,
M13post, M13neutral, M14a–e, M15a, M15b — so thirteen cells had no possible
observer. Found when the `.tex` batch went to look for it.
It is now implemented as pin 3a requires: the `.tex` slice from the
`\begin{requirement}` preceding the label to the first `\end{requirement}` at or
after it, whitespace-collapsed, **equal** to pin 3's pinned source.
**M14e is the vindication of equality over a stem inventory.** It appends
`A \texttt{Constant} segment's \texttt{end\_tempo} \MUST{} be absent.` — no
`canonic`, no `normaliz`, no `prefer`, and it settles P13-S8 inside a requirement
minted not to. Equality fails it; every phrase-and-stem form passes it.
#### 9.1.4 An interrupted run left a mutation applied
The mutation harness restores in a `finally`. A **killed** process runs no
`finally`, so an interrupted batch leaves the tree mutated. One did: M2a's
wildcard survived at `invariants.rs:425`.
It was found by re-reading the file, and `invariant_selector_discriminates_its_payload`
confirmed it:
```
invariant 10's selector must return only its own; got [
WellFormednessViolation { kind: Invariant(CrossCuttingRefsResolve), witness: "staff ...
WellFormednessViolation { kind: Invariant(EventCoordinateModel), witness: "aleatoric ...
```
**Restored by hand-editing**, never git, and the full suite returned to
`44 / 1606 / 0 / 0`.
*The lesson is not "be careful with interrupts": it is that a restore guaranteed
only by process exit is not a guarantee. **Verify the baseline after any
interrupted mutation run, before trusting the next measurement** — a stray
mutation makes every subsequent radius wrong in a way that looks like a
mismatch in the wrong place.*
### 9.2 The surface moved twice, and what that obliges
| Surface | Cause |
|---|---|
| 1604 | §4's surface — pin 10's 16 tests, pin 1b's two |
| **1605** | §9.1.1's missing test added |
| **1606** | §9.1.3's missing guard added |
**Radii are measured against the final surface.** The 17 mutations first measured
at 1604 were **re-run in full** at 1605 and all matched. The 38 measured at 1605
were **not** re-run in full at 1606; the justification is bounded and stated:
- **Pin 3a's guard has exactly two inputs** — `core_spec.tex` via `include_str!`
and a string literal. Verified mechanically: no `production_source`, no
`check_*` call, one `include_str!` target.
- **None of those 38 modifies `core_spec.tex`.** They edit `invariants.rs`,
`generators.rs` or `public_surface.rs`.
- **Two representatives were re-run at 1606 anyway**, one per interaction class:
**M2a** — the widest selector radius, 21 — and **M20b**, a prose edit inside
`invariants.rs`. Both matched unchanged.
*This is an argument from a test's complete input set, not from reasoning about
fixture reach — the thing this rung has repeatedly got wrong. It is recorded as
an argument, not presented as a measurement.*
### 9.3 Expected versus observed — all 54 mutations
| M | Cell | Observed | |
|---|---|---|---|
| M1·C4 | 2 | 2 | ✅ |
| M1·C5 | 3 | 3 | ✅ |
| M1·C6 | 2 *(amendment 1)* | 2 | ✅ |
| M1·C7 | 2 *(amendment 1)* | 2 | ✅ |
| M1·C8 | 4 | 4 | ✅ |
| M1·C9 | 2 | 2 | ✅ |
| M1·C10 | 3 | 3 | ✅ |
| M2 | 8 | 8 | ✅ |
| M2a | 21 *(measured pre-ratification)* | 21 | ✅ |
| M3 | 13 | 13 | ✅ |
| M3a | 1 | 1 | ✅ |
| M4 | 1 | 1 | ✅ |
| M5 | 1 | 1 | ✅ |
| M6 | 1 | 1 | ✅ |
| M7 | 7 | 7 | ✅ |
| M7a | 1 | 1 | ✅ |
| M7b | 1 | 1 | ✅ |
| M7c | 1 | 1 | ✅ |
| M7d | 1 | 1 | ✅ |
| M8 | 5 | 5 | ✅ |
| M9 | 14 | 14 | ✅ |
| M10 | 3 | 3 | ✅ |
| M11 | 4 | 4 | ✅ |
| M12pre | 1 | 1 | ✅ |
| M12 | 1 | 1 | ✅ |
| M13 | 1 | 1 | ✅ |
| M13post | 1 | 1 | ✅ |
| M13neutral | 1 | 1 | ✅ |
| M14a–M14e | 1 each | 1 each | ✅ |
| M15a | 1 | 1 | ✅ |
| M15b | 1 | 1 | ✅ |
| M16a | 1 | 1 | ✅ |
| M16b | 1 | 1 | ✅ |
| M17·C1 | 20 *(18 measured + 2 new)* | 20 | ✅ |
| M17·C2 | 3 *(measured)* | 3 | ✅ |
| M17·C3 | 1 *(measured)* | 1 | ✅ |
| M18 | 1 | 1 | ✅ |
| M20 | 1 | 1 | ✅ |
| M20a–M20k | 1 each | 1 each | ✅ |
**No compile-only result. No passing-outcome mutation** — §3 requires every row
to fail, and every row did.
### 9.4 Three cells worth their own note
**M2a, 21, unchanged from its pre-ratification measurement.** §3 warned its proxy
over-approximated for any test observing a rider through the selector, and that
none of the 20 legacy tests was a rider test. Confirmed: the legacy 20 are exactly
the `g3b_measure20_tests` set measured, plus the new discriminator.
**M17·C1, 20, and `display_renders_each_arm_exactly` is not among them.** That
absence is the receipt for §9.1.2: under the unrepaired C1 fixture it would have
been.
**M7b, 1.** §3 records that revision L wrongly named
`every_invariant_has_a_negative_generator` here, since that test iterates `all()`
and cannot detect an omission from `all()`. Observed: `graph_invariant_all_is_unchanged`
alone.
### 9.5 Restoration
After every row, and after the interrupted-run repair:
```
suites=44 passed=1606 failed=0 ignored=0
cargo +1.95.0 clippy --workspace --all-targets -- -D warnings: clean
```
**1586 → 1606, twenty net-new tests**, and 43 → 44 suites:
| Count | Where |
|---|---|
| 17 | pin 10's eleven-row matrix and its whole-surface tests |
| 1 | pin 3a's `.tex` prose guard |
| 1 | pin 1b's derives guard, in `g3a_tests` |
| 1 | pin 1b's integration test — the new suite |
---
## §10. A sixth fault, found by gate 16 at the last moment
**Pin 9's `/// 10.` rider note was never migrated.** It is one row of pin 9's
table, and it was the only row left undone — the other eight were verified
individually rather than assumed, which is how this one surfaced.
The note still read:
```rust
/// Beyond that surface, further checks are reported under this same tag
/// and are NOT part of the normative invariant 10: tempo-map segment
/// shape, ordering and non-overlap (Chapter 3,
/// `req:time:tempo-segment-order`); ...
/// multiplexing is filed as P13-S29 — the public `check_invariant`
/// filter and this violation's `Display` attribute those failures to
/// invariant 10. Repairing it is a behaviour change, out of scope here.
```
**Three statements, all false as of this rung**, and the gate names all three:
the riders are no longer *"reported under this same tag"*; P13-S29 is no longer
their *pending owner* — it is this commit; and the note listed **three** labels
where pin 9 requires **four**, `req:time:tempo-segment-shape` being the one this
rung minted.
*The missing fourth label is the same defect shape as §9.1.1: a set that grew by
one, and a list that did not.* It is now rewritten to name all four and to say
that `check_invariants` still returns them, so a caller asking *"is this graph
well-formed"* keeps its coverage.
**Why no test caught it.** Pin 9's prose outcomes have **no machine observer** —
gate 16 says so outright: *"Every one of these can be omitted with all other
gates green."* Eight rows had landed; the ninth had not; nothing in 1606 tests
could tell the difference.
**Every other pin 9 row was re-verified by its own stale phrase**, not by
assumption:
| Stale phrase | Found in |
|---|---|
| `surfaced here under invariant 10` | clean |
| `go under invariant 10` | clean |
| `surfaced under an existing` | clean |
| `the compatibility invariant` | clean |
| `tempo-map segment invariants` | clean |
| `all 19 enumerated graph invariants` | clean |
| `reported under this same tag` | **`invariants.rs`** → repaired |
| `filed as P13-S29` | **`invariants.rs`** → repaired |
*`core_spec.tex:3120` still occurs in `DECISIONS.md` and `accidental.rs`.
Neither is a pin 9 row: pin 9 pins that locator's replacement in the **accidental
header comment** in `invariants.rs`, which is clean, and it explicitly does
**not** rewrite `DECISIONS.md`, which gains a supersession note instead.*
---
## §11. Gate results, 1–16
| # | Gate | Result |
|---|---|---|
| 1 | `cargo test --workspace` | **44 suites / 1606 passed / 0 failed / 0 ignored** |
| 2 | clippy `-D warnings` | clean, 0 warnings and 0 errors |
| 3 | `fmt -p epiphany-core -p epiphany-testkit --check` | clean (never `--all`) |
| 4 | staged paths ⊆ §2 rows, all rows staged | 13 paths, 13 rows |
| 5 | `git diff --cached --check` | clean |
| 6 | identifier and field migration | §6 above, verbatim |
| 7 | every §3 mutation observed | §9.3 — 54 rows, all matched |
| 8 | `all()` re-derived at 21; `.tex` count claim unchanged | 21 entries, 21 unique, 21 `number()` arms 1..21, order identical; `core_spec.tex:6746` still reads *"exactly \textbf{21} invariants"* and is absent from the diff |
| 9 | `latexmk -xelatex core_spec` | undefined references cleared on pass 1; `core_spec.pdf` rebuilt |
| 10 | ledger append, removed-plus-added reconstruction | 1 removed / 1 added; `added` ends with `\|`; `strip(added) == strip(removed) + " " + APPEND` **true** |
| 11 | temporary allowlist row absent, two survivors present | `req:time:tempo-segment-shape` absent; `req:layoutir:vertical-bands` and `req:graph:aleatoric-reference-locality` present |
| 12 | `requirement_labels` passes with the row absent | 6 passed, 0 failed |
| 13 | pin 11's inventory | **25 observations: 9 migrated (5 + 4), 16 unchanged**, none deleted, none softened; M16a and M16b prove both negatives non-vacuous |
| 14 | pin 12's lifecycle | status block exactly `STATUS: LANDED by this commit.`, no hash; frozen-pins statement shows **0 hunks** in a zero-context staged diff; revisions A–R marked a dated historical record |
| 15 | placement and Revision History row | shape follows order's `\end{requirement}` with only a `\begin{requirement}` between; the added run equals pin 13's block, whitespace-collapsed |
| 16 | pin 9's prose outcomes | §10 — eight rows verified clean by their own stale phrase, one repaired |
### 11.1 Gate 10's one-character finding
The staged ledger append first read `RESOLVED 2026-08-12`; pin 13's `APPEND` is
pinned verbatim as `2026-08-11`. The reconstruction failed on that character
alone, and **the artifact was corrected to the pin, not the pin to the artifact.**
*Flagged for the owner rather than silently reconciled: the contract's own
ratification line reads 2026-08-12, so the pinned append carries the date the
row was drafted rather than the date the rung resolved. Changing it is an
administrative amendment to pin 13, not an execution decision — gate 10 exists
to make exactly this deviation visible.*

File diff suppressed because one or more lines are too long

Binary file not shown.

View File

@ -2277,6 +2277,18 @@ pub struct Tempo {
\texttt{start\_tempo} if no earlier segment exists. \texttt{start\_tempo} if no earlier segment exists.
\end{requirement} \end{requirement}
\begin{requirement}
\label{req:time:tempo-segment-shape}
A tempo segment's \texttt{shape} and its \texttt{end\_tempo} \MUST{} be
compatible. If \texttt{shape} is \texttt{Constant} and \texttt{end\_tempo}
is present, it \MUST{} equal \texttt{start\_tempo}. If \texttt{shape} is
\texttt{Linear}, \texttt{Exponential} or \texttt{Curve}, \texttt{end\_tempo}
\MUST{} be present.
This requirement states the compatibility that is enforced. It does not
determine whether a constant segment records an \texttt{end\_tempo} at all.
\end{requirement}
\subsection{Conversion} \subsection{Conversion}
Conversion between musical and wall-clock time integrates the tempo map. Conversion between musical and wall-clock time integrates the tempo map.
@ -17029,6 +17041,20 @@ layouts they own versus inherit:
region --- a locality rule the checker has always enforced and no requirement region --- a locality rule the checker has always enforced and no requirement
stated. stated.
\\ \\
\today & \sectionsc{Graph Invariants}, \sectionsc{Time and Duration} &
\textbf{P13-S29: the violation tag stops multiplexing.} Graph invariant~10
reported Chapter~3 and Chapter~4 failures under its own number, through a
public API. The violation type becomes \texttt{WellFormednessViolation}
carrying a two-armed \texttt{ViolationKind}: an invariant arm and a
requirement arm naming a \texttt{req:} label. Invariant~10 keeps only
reference resolution; tempo segment shape, tempo segment order, aleatoric
reference locality and accidental modification expressibility now report
under their own requirements. \sectionsc{Time and Duration} gains
Requirement~\ref{req:time:tempo-segment-shape}, stating the enforced
shape/\texttt{end\_tempo} compatibility without determining whether a
constant segment records an \texttt{end\_tempo} at all. The enumeration is
unchanged.
\\
\bottomrule \bottomrule
\end{longtable} \end{longtable}