epiphany/spec/CONTRACT_P13S18_MATRIX.md

# Contract — P13-S18: the invariant-20 outcome matrix

**Status:** RATIFIED.

**Rung type:** diagnostic and bookkeeping. **No behaviour change.** No graph that
violates invariant 20 today may stop violating it, and no graph that passes today
may start violating it. If the work suggests otherwise, **stop** (§1 pin 6).

---

## §0. What was verified before drafting

Every claim below was read out of the working tree at `cc49533`, not recalled,
and re-confirmed unaffected at `f33673d` (see §4).

1. **`check_measure_meter_consistency` has nine non-success paths**, not the five
   an earlier scoping note claimed. Enumerated with line numbers in pin 1.
2. **Only three are abstentions.** The other six are one inapplicability, two
   delegations, two vacuities, and one separately-filed deferral (pin 2).
3. **Invariant 10 really does own the two delegated paths.**
   `invariants.rs:1220`ff checks that time-signature references resolve *"at
   every level a `MeterChange` can appear"* and its loops cover **per-measure**
   (`si.measures`, emitting `"measure {:?} time signature {:?} is not
   declared"`), **instance-local grids** (`si.local_metric_grid`), the
   **region-default grid**, and the **metric time model's own meter sequence**.
4. **P13-S18's "`Measure` *end* anchor" claim is wrong only in its "any", and
   two successive scoping notes each overcorrected it.** The first called the
   claim simply false; the second called it merely misattributed. The precise
   position has three parts, all read out of `measure20_comparable_order`:
   - **Same id, same position — `End`↔`End` is comparable *when its offsets
     compare*.** c2 requires `ia == ib && pa == pb` and then delegates to
     `measure20_offset_order`, which returns `None` for `Musical`↔`WallClock`
     (`:2428`–`:2429`). So "any `Measure` end anchor" is false as written, but
     the counter-example is conditional and must be stated that way.
   - **Distinct ids — `End` anchors remain incomparable**, because c3 returns
     `None` unless `*pa == MeasurePosition::Start` with both offsets `Zero`. A
     vector index orders measure *reference points*, not arbitrary points near
     them. Distinct-id `End` anchors therefore genuinely do reach **A4, B4 and
     B5**, and are a real residue shape.
   - **The resolver citation describes the missing duration machinery, not
     invariant 20's execution path.** `resolve_anchor`'s `Measure` arm
     (`invariants.rs:503`–`:516`) returns `None` for any `position !=
     MeasurePosition::Start` because a measure's length "needs the deferred
     decomposition/tempo machinery" — a true statement about *why* the duration
     is unavailable. **Invariant 20 never calls it: zero occurrences in
     `:2636`–`:2725`.** The citation explains the underlying gap; it does not
     describe how invariant 20 reaches its abstentions.

   The `invariants.rs:400` line number is separately stale (§0.7).
5. **P11-C5 is not P13-S18's gate.** `PASS11_WORKLIST.md:159` defines it as the
   *"nearest surviving anchor" stand-in* — a re-anchoring proximity metric that
   *"resolves when the graph-mutation phase tracks resolved positions"*. The G3b
   contract cites it correctly but **narrowly**, for the two-distinct-`Event`s
   case, via `PositionOutsideRegion`'s Reserved note (`effect.rs:139`–`:142`).
   The capability P13-S18 waits on — placing on a common timeline **any pair
   c1–c5 cannot order, and any pair it orders without yielding a usable musical
   delta** — is strictly broader and is owned by **no filed candidate**. Pin 10
   is the authoritative scoping; this item must not restate it more narrowly.
6. **Step 0 is per measure reference.** `measure20_governing_by_anchor` is
   called once per measure with that measure's own `start`, and
   `measure20_comparable_order` is a property of the *pair*. An incomparable
   meter change therefore disables agreement for every measure whose start is
   incomparable **to it** — not for every measure in the instance, when the
   instance's measures carry heterogeneous anchor shapes. An earlier scoping
   note said "every measure in that instance"; that was wrong and pin 7 locks
   the correction behaviourally rather than in prose.
7. **The G3b contract's `invariants.rs:400`ff citation (`:206`) has drifted.**
   The resolver it describes now begins at `invariants.rs:466`, with the
   `Measure` arm at `:503`–`:516`. The paragraph's own narrower claim — that
   cross-boundary comparison stays unverifiable without the boundary's
   duration — remains **correct** and is not touched (pin 9).

---

## §1. Pins

**Pin 1 — the nine paths, and their sites.** These are exhaustive over
`check_measure_meter_consistency` (`invariants.rs:2636`). Any tenth found during
execution is a finding, reported before proceeding.

| Id | Clause | Path | Site |
|---|---|---|---|
| A1 | agreement | `m.time_signature` is `None` | `:2661` |
| A2 | agreement | declared signature does not resolve | `:2662` |
| A3 | agreement | `Governing20::None` | `:2675` |
| A4 | agreement | `Governing20::Indeterminate` | `:2677` |
| B1 | boundary | first measure (`i == 0`) | `:2683` |
| B2 | boundary | governing signature does not resolve | `:2689`–`:2693` |
| B3 | boundary | `Governing20::None` | `:2717` |
| B4 | boundary | `Governing20::Indeterminate` | `:2719` |
| B5 | boundary | musical delta not computable | `:2713` |

**Pin 2 — the classification, ratified.** Six labels. Every path takes exactly
one.

| Id | Class | Why |
|---|---|---|
| A1 | **inapplicable** | no declared signature can disagree with anything; pin 9b makes `None` avoid *only* this clause, never the boundary clause |
| A2 | **delegated** | invariant 10, per-measure arm (§0.3) |
| A3 | **vacuous** | no governing signature exists to disagree with (pin 6c case 1) |
| A4 | **genuine abstention** | the relation cannot place a candidate |
| B1 | **P13-S19** | the pickup/anacrusis deferral, already filed |
| B2 | **delegated** | invariant 10, grid-level arms (§0.3) |
| B3 | **vacuous** | pin 6c case 1 |
| B4 | **genuine abstention** | as A4 |
| B5 | **genuine abstention** | order without distance |

**Exactly three genuine abstentions: A4, B4, B5.** This is the whole point of
the rung — P13-S18 currently presents all nine as one undifferentiated residue,
which both overstates the gap and hides which part of it is real.

**Pin 3 — delegation must be verified, not asserted.** A2 and B2 are classed
`delegated` only if some *other* invariant actually reports the condition. The
matrix must show, for each, that invariant 10 emits a violation on the same
graph — and M7/M8 must show that removing invariant 10's arm makes the condition
go **unreported by the whole suite**, not merely by invariant 20. A delegation
nobody discharges is an abstention wearing a better name.

**Pin 4 — the outcome matrix.** Rows are representative anchor shapes, columns
are the two clauses, each cell names the path id that fired and its class.
Minimum shapes:

| Shape | Description |
|---|---|
| S1 | `WallClock` start, `WallClock`-anchored meter changes |
| S2 | `WallClock` start, `Region`-anchored meter changes |
| S3 | `Region` same id, same edge, `Musical` offsets — fully decidable |
| S4 | `Measure` **same id, `pos: End` on both sides**, `Musical` offsets (c2) |
| S5 | `Measure` distinct ids, `Start`, `Zero` (c3) |
| S6 | `Event` same id, **live** event, `Musical` offsets (c1) |
| S7 | `Event` distinct ids, otherwise identical to S6 |
| S8 | matching referent, **differing** `pos`/`edge` selector |
| S9 | one instance, **heterogeneous** measure anchors (pin 7) |

**S6 and S7 are a positive/negative pair and neither may be dropped.**
`Measure.start` and `MeterChange.anchor` are unrestricted `TimeAnchor`s, so
`Event`-anchored measures are valid rather than hypothetical. S6 proves such a
measure genuinely reaches c1. S7 changes **only the referent identity** and
isolates the distinct-`Event` fall-through — which is precisely the case the
retained P11-C5 citation at `CONTRACT_GENESIS_G3B_MEASURE.md:223` exists for.
Both use live events and `Musical` offsets.

**S4 is the row that falsifies "any `End`", and it must do so by observation.**
It is deliberately an `End`↔`End` pair on the **same** measure id with `Musical`
offsets — c2's exact shape — and its meter changes carry the same anchor form,
so both clauses reach a decision. It is therefore `D`/`D` and, per the rule
below, deliberately wrong. S5 supplies the contrast on distinct ids. A contract
that only *stated* "same-id `End` is fine" would be repeating the mistake this
pin exists to correct.

**Every cell holds either a path id (A1–B5) or `D`.** A fully comparable shape
takes *none* of the nine paths — it decides — and a cell left blank because
"nothing fired" is indistinguishable from a cell nobody looked at. **Every `D`
fixture must be deliberately wrong**, so that the emitted violation is what
proves the clause decided. S3 and S6 are `D` in both columns; an S6 that emits
nothing has demonstrated nothing.

Every cell must be **observed**, never derived. A cell filled in by reading the
match arms and reasoning about which one wins is unsigned.

**Pin 5 — the `WallClock` finding, and the split an earlier draft got wrong.**
`valuegen::measure` (`ops/src/valuegen.rs:447`) anchors starts to
`TimeAnchor::WallClock`. An earlier draft of this contract said that shape makes
**both** clauses abstain. It does not, and the difference is the meter changes'
anchors, not the measures':

- **S1 — `WallClock` measures, `WallClock` meter changes.** The anchors are
  mutually comparable under c5, so step 0 passes and a unique maximum is found:
  **agreement decides.** But `measure20_musical_delta` never returns a
  `WallClock` delta (`:2527`, `AnchorOffset::WallClock(_) => None`), so the
  boundary clause takes **B5**.
- **S2 — `WallClock` measures, `Region` meter changes.** `comparable_order`
  falls through to `_ => None`, so step 0 returns `Indeterminate`: agreement
  takes **A4** and the boundary clause takes **B4** — *not* B5, because the
  `Governing20` match short-circuits before the delta is ever computed.

**A `WallClock` start does not by itself disable both clauses.** The report must
state the split, must **not** claim `WallClock` is the dominant shape in real
scores (measure starts are author-supplied), and may claim only that it is the
shape this repository's fixture generator emits.

**Pin 6 — the hard stop.** No widening of `measure20_comparable_order` or
`measure20_musical_delta`. No new violation. No change to which graphs violate
invariant 20. The G3b contract holds that defining a new comparability relation
*"is a specification question this rung has no authority over"*, and that is
unchanged. **If the classification work suggests a behaviour change — including
"A3 should really be a violation" or "B2 should be reported here rather than by
10" — stop, report, and let it be split into a separately ratified semantic
rung.** Do not implement it here, and do not soften a class label to avoid
raising it.

**Pin 7 — step-0 scope, locked behaviourally.** S9 must contain one instance
whose measures carry heterogeneous anchor shapes, such that **one measure's
agreement clause abstains via A4 while another measure's agreement clause in the
same instance reaches a decision**. Prose asserting this is not enough; the row
is what forbids the "one incomparable change disables the whole instance"
overstatement from reappearing.

**Pin 8 — the P13-S18 correction.** Five defects, all of them mine:
1. three abstention shapes → **nine paths**, classified;
2. **correct**, not delete, the "`Measure` *end* anchor" claim, to all three
   parts of §0.4: same-id `End`↔`End` is comparable under c2 **when its offsets
   compare** — `measure20_offset_order` rejects `Musical`↔`WallClock` — so
   "any" is false but conditionally so; distinct-id `End` anchors **are**
   incomparable and do reach A4/B4/B5; and the resolver citation names the
   missing duration machinery rather than invariant 20's execution path;
3. re-gate: not P11-C5, but the broader capability filed as P13-S23 (pin 10);
4. name A2/B2 as delegated to invariant 10 with its line, so the entry stops
   counting them as gap;
5. state the S1 finding.
The entry stays **open** — A4, B4 and B5 remain real — but open at its true size.

**Pin 9 — the G3b contract corrections, two of them and both narrow.**

1. **`:347`** says the residue's closure needs "P11-C5 resolved positions". That
   is the overbroad claim. Correct it to name P13-S23 as the owner of the
   general case.
2. **`:206`** cites `invariants.rs:400`ff for the prototype anchor resolver. The
   resolver now begins at `:466` with its `Measure` arm at `:503`–`:516`.
   **Correct the line number only.** The paragraph's claim — that cross-boundary
   comparison stays unverifiable without the boundary's own duration — is
   correct, is narrower than P13-S18's use of it, and must survive verbatim.

**`:223`'s citation is correct and stays.** It cites P11-C5 for the
two-distinct-`Event`s case specifically, which is genuinely what
`PositionOutsideRegion`'s Reserved note (`effect.rs:139`–`:142`) covers.
**The contract is RATIFIED and its pins are not reopened**; both edits are
citation repairs, and neither changes a ratified claim.

**Pin 10 — P13-S23.** File the unowned capability: *placing anchor pairs on a
common timeline and measuring musical distance along it, wherever **c1–c5 do not
already yield both**.* Two disjoint deficiencies, and the candidate owns both:

1. **No ordering.** The pair is not comparable at all. The failure may be in the
   **referent** (distinct `Event` ids, distinct `Measure` ids outside c3's
   `Start`+`Zero` restriction), the **variant or selector** (`Event`↔`Measure`,
   `Measure`↔`Region`, differing `pos`/`edge`), or the **clock**
   (`Musical`↔`WallClock`, including inside `measure20_offset_order`). This is
   what A4 and B4 are made of.
2. **Ordering without a usable delta.** The pair *is* comparable and still
   yields no musical distance: **c3** supplies a vector index, which is an order
   and never a distance; **c5** compares two `WallClock`s, and
   `measure20_musical_delta` never returns a `WallClock` delta (`:2527`). This
   is what **B5** is made of.

**Scoping this as "not directly comparable under c1–c5" would have excluded B5
entirely** — S5 is c3-comparable and S1 is c5-comparable, and both reach B5 — so
the candidate would have disowned a third of the residue it is filed to own. An
earlier draft also said "anchors of differing shapes", which additionally
excluded the same-variant cases (distinct `Event`s, distinct `Measure`s).

Explicitly **broader than P11-C5**, with the distinction stated: P11-C5 is a
re-anchoring proximity metric that waits on resolved positions; P13-S23 is the
timeline itself. Name its dependents: invariant 20's A4/B4/B5, and
`PositionOutsideRegion`'s Reserved status. Filed **open**; no code owed.

---

## §2. Touch table

| # | File | Change |
|---|---|---|
| 1 | `crates/epiphany-core/src/invariants.rs` | **tests only**, plus a doc-comment classification on `check_measure_meter_consistency` naming each of the nine paths and its class. The doc comment is not normative and changes no behaviour. **No production logic edit of any kind.** |
| 2 | `spec/PASS13_CANDIDATES.md` | P13-S18 corrected per pin 8; **P13-S23** filed per pin 10 |
| 3 | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` | `:347` (overbroad P11-C5 claim) and `:206` (stale resolver line number), per pin 9. `:223` untouched |
| 4 | this contract | DRAFT → RATIFIED |

**No `.tex` change and no PDF.** The classification describes existing
behaviour; it makes no normative claim. **If the classification turns out to
contradict `core_spec.tex`'s invariant-20 text, that is a finding — stop and
report it** (pin 6), because a spec correction is a semantic rung.

**No `DECISIONS.md` entry.** Consistent with the P13-S15 ruling: test coverage
and ledger bookkeeping, not a semantic ruling.

---

## §3. Mutation plan

Every mutation is a specific edit to a specific site, each **observed** red and
restored by hand-editing back. Never `git checkout`, never `git stash`.

| M | Edit | Row it signs |
|---|---|---|
| M1 | make A4's graph comparable (swap the incomparable meter change's anchor to the measure's own shape) | A4 is an abstention, not a pass: the agreement violation **appears** |
| M2 | as M1 for B4 | B4 is an abstention |
| M3 | swap S5's two measure starts to `Region` same-id `Musical` offsets | B5 is an abstention: the delta becomes computable and the boundary violation appears |
| M4 | give A1's measure a resolving `time_signature` that disagrees | A1 is inapplicable, not concealing: the violation appears |
| M5 | make **S2**'s meter-change anchors `WallClock`, matching its measures | pin 5's split: S2's cell pair moves **A4/B4 → D/B5** — agreement stops abstaining and decides, and the boundary clause moves from indeterminate selection to incomputable delta. Writing this as "A4/B4 → B5" is wrong: A4 is an agreement path and cannot appear in the boundary column. **S2 is the target, not S1** — S1's agreement clause already decides, so no mutation of S1 could show it begin to |
| M6 | in S9, give the second measure the first's incomparable anchor shape | pin 7: its agreement clause stops deciding — and **only** then |
| M7 | delete invariant 10's per-measure time-signature arm (`:1250`ff) | A2 is delegated: the condition becomes **unreported by the whole suite** |
| M8 | delete invariant 10's instance-local-grid arm | B2 is delegated, same standard |
| M9 | make B1's measure a non-first measure | B1 is the P13-S19 deferral, not a silent pass |
| M10 | remove B3's emptying filter so a governing signature exists and disagrees | B3 is vacuity, not concealment |

**Ten mutations.** Report the observed count; any deviation is a finding.

**Anti-traps, all earned in this session.** A mutation that does not compile
signs nothing. A mutation in an operation that runs *before* the asserted state
cannot reach it. A guard written against an index that structurally cannot hold
the referent is born green. Transaction-block members reduce atomically at the
*first* member's canonical position. Envelope counter gaps make operations
permanently pending, which makes fixtures silently vacuous. **And the one this
rung is most exposed to: a matrix cell that agrees with the prediction is the
easiest place in the world to stop looking.** Each cell must fail loudly if the
path it names is not the path taken — assert the *outcome*, and construct the
graph so no other path could have produced it.

---

## §4. Gate

- `cargo test --workspace` — baseline **1541 / 0**, confirmed at `f33673d`
  (the commits between `cc49533` and it are `spikes/`-only, a separate
  workspace, so the root count is unmoved); delta explained.
- `cargo clippy --workspace --all-targets` — zero warnings.
- `cargo fmt -p epiphany-core -- --check` — clean. **Never `cargo fmt --all`**;
  it crosses into the `spikes/` workspace through path dependencies.
- All **10** mutations observed red and hand-restored.
- **A diff check that `check_measure_meter_consistency`'s executable body is
  byte-identical to `cc49533`** — the doc comment may grow; not one line of
  logic may move. This is the rung's central claim and must be mechanically
  demonstrated, not asserted.
- `git diff --cached --check` clean; nothing from `spikes/` or `.claude/`
  staged.

## §5. Whitespace and staging

1. Stage the touch-table files explicitly. **Never `git add -A`.**
2. `git diff --cached --check` — catches staged and formerly-untracked files.
3. Commit.
4. `git diff --check <parent>..HEAD -- crates/ spec/` — path-scoped.

**A concurrent session commits to this repository.** Re-check `HEAD` before
committing, and never run `git reset`, `git restore --staged`, `git checkout`,
or `git stash` against the shared index.

## §6. Boundary — unchanged and absolute

MUST NOT be read, written, or staged: `spec/PLAN_EDITOR_APP.md`,
`spec/CONTRACT_EDITOR_*.md`, `spec/ANALYSIS_GENESIS_PERSISTENCE.md`,
`spec/ANALYSIS_TEXT_RUN_PRIMITIVES.md`, `spec/DRAFT_T4_FIXTURE_RECIPE.md`,
`crates/epiphany-editor-gui/goldens/*.png`, `crates/epiphany-render-svg/**`,
`crates/epiphany-glyphs/**`,
`crates/epiphany-testkit/benches/editor_pipeline.rs`, the entire `spikes/`
tree, the root `Cargo.toml` change, `.claude/worktrees/`.

## §7. Report requirements

- The **full matrix — nine shapes × two clauses, 18 cells** — every cell
  observed, each holding a path id or `D`, with the test name that observed it.
- All **10** mutations with their observed failing test names.
- Explicit confirmation that `check_measure_meter_consistency`'s logic is
  byte-identical, with the command that showed it.
- Explicit confirmation that **no new violation** is emitted anywhere, and that
  the workspace count moved only by the tests added.
- For A2 and B2: the invariant-10 violation text observed, and the M7/M8 result
  showing the condition otherwise goes unreported.
- **Anything the contract did not anticipate** — a tenth path, a cell that
  contradicts pin 2, or anything suggesting a behaviour change. Report it and
  **stop**; do not implement it.