diff --git a/spec/CONTRACT_P13S29_VIOLATION_KIND.md b/spec/CONTRACT_P13S29_VIOLATION_KIND.md index 6daa604..4afa220 100644 --- a/spec/CONTRACT_P13S29_VIOLATION_KIND.md +++ b/spec/CONTRACT_P13S29_VIOLATION_KIND.md @@ -1675,3 +1675,425 @@ execution confirms it and any difference is a finding.* - **The recurring citation-gate collision** — a contract proposing a label breaks the gate the moment it is written, now four times. That belongs in `CLAUDE.md` as a standing note, on its own terms, not here. + +--- + +## §6. AMENDMENT 1 — §3's M1·C6 AND M1·C7 RADII, MID-EXECUTION + +STATUS: RATIFIED; FROZEN. Execution of P13-S29 resumes at M2. + +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 +further defect is its own amendment with its own review round. + +**§3 was frozen and dispatched at `cea21cd`.** Ratification **authorizes and +freezes** this amendment; execution applies the replacements. §6.9 pins the +landed form and the order of the remaining steps. + +**Scope — the complete write surface, all four parts.** A description of the +normative correction is not a description of what gets written, and an earlier +draft of this head said *"two radius cells and nothing else"* while prescribing +three further edits below it: + +| | Edit | Where | Touch row | +|---|---|---|---| +| 1 | M1 row replacement | §3 (this file) | 9 | +| 2 | Preamble append | §3 (this file) | 9 | +| 3 | This amendment's own lifecycle transitions | §6 (this file) | 9 | +| 4 | Resolution/resumption append | `spec/EVIDENCE_P13S29_EXECUTION.md` | 10 | + +**"Two edits, both in §3" describes edits 1 and 2 — the normative §3 correction +— and nothing else.** Edits 3 and 4 are lifecycle and record. + +**One further act belongs to ratification rather than to execution:** the +ratification commit stages `spec/EVIDENCE_P13S29_EXECUTION.md` in its +**pre-amendment** state, under the same touch row 10, to serve as §6.5c-bis's +oracle. *It is listed here and not in the table because it is not an edit this +amendment makes — it is the act that gives the amendment something durable to be +checked against, and it must happen before edit 4.* + +**What does not move:** no pin, no test, no fixture, no behaviour, no other §3 +cell. It does not create, retire or renumber a mutation, and it **rewrites no +existing evidence** — §6.5d is the standing prohibition. + +### 6.1 The defect + +§3's M1 row closes: + +> **C6 and C7 fail their pin-10 test alone**: the legacy `f4` assertion is one +> fixture tripping *both*, so re-tagging one leaves the other still reporting the +> same label and the legacy assertion still passes + +**Measured, the radius of each is two, not one.** Transcripts: annex §5.3, §5.4. + +| M | §3's cell | Measured | +|---|---|---| +| M1·C6 | `tempo_out_of_order_reports_order` | that test **and** `tempo_overlap_reports_order` | +| M1·C7 | `tempo_overlap_reports_order` | that test **and** `tempo_out_of_order_reports_order` | + +### 6.2 Why — and what in the quoted sentence survives + +**The sentence's claim about `f4` is correct and is retained.** `f4` is in +neither radius, for exactly the reason given: it holds one fixture tripping both +conditions and asserts on the label, which the surviving sibling keeps supplying. +Measurement confirms it. + +**What the sentence omits is that pin 10's own C6 and C7 tests stand in the same +relation to each other.** Pin 10 pins four assertions per row; the fourth is +*the aggregate's invariant arm is empty*. Pin 10 also states, in terms: + +> C6's natural fixture — `seg(2,3)` then `seg(1,2)` — is *also* overlapping, so +> it emits C6 **and** C7 under the same label. + +Both tests are built by `two_segments(seed, (2, 3), (1, 2))`, differing only in +the seed. Re-tagging **either** condition therefore places an `Invariant` +violation in **both** fixtures, and the sibling's fourth assertion fails on it. + +**The cell reasoned about the legacy observer and stopped there.** Having +established the shared-fixture property one clause earlier, it did not ask the +same question of the tests this contract itself writes. + +### 6.3 What must NOT change in response + +- **Not the fixtures.** The only shape isolating C6 is an end-before-start + segment, which pin 10 **rejects** as *"unnatural and tests a shape the checker + should never see."* +- **Not pin 10's fourth assertion.** §3's M2a derivation depends on it: it is + what keeps the seven C4–C10 tests out of M2a's radius *structurally rather than + by assumption*. +- **Not any other M1 cell.** C4, C5, C8, C9 and C10 were measured in the same + pass and **matched exactly** — 2, 3, 4, 2 and 3 respectively. + +### 6.4 The correction is a strengthening, not a relaxation + +**The amendment adds no observer.** Pin 10's tests already supplied both — its +own `(kind, witness)` pair assertion and the sibling's invariant-arm assertion +have detected each re-tagging since the moment those tests were written. What +changes is the **accounted and required** radius: §3 credited the mutation with +one observer and would have read the second as a mismatch, so the amendment +**recognizes** an observation the contract was under-counting. + +That is a strengthening because the required radius is now two: a future +implementation that silenced the sibling assertion would fail this gate, where +under the dispatched cell it would have passed. + +### 6.5 The replacements — edits 1, 2 and 4 of the scope table + +**Touch rows 9 and 10 already cover both files this amendment writes to** +(`CONTRACT_P13S29_VIOLATION_KIND.md`, `EVIDENCE_P13S29_EXECUTION.md`). No touch +row is added. + +#### 6.5a — §3's M1 row + +Replace the sentence quoted in §6.1 with: + +> **C6 and C7 each fail *both* pin-10 order tests, and the legacy `f4` assertion +> fails for neither.** `f4` holds one fixture tripping both conditions and +> asserts on the label, so the surviving sibling keeps supplying it — but pin +> 10's C6 and C7 tests stand in that same relation to *each other*: both are +> `two_segments(seed, (2, 3), (1, 2))`, which pin 10 establishes emits C6 **and** +> C7. Re-tagging either puts an `Invariant` violation into both fixtures, so the +> sibling's **fourth** assertion — *the aggregate's invariant arm is empty* — +> fails alongside the mutated condition's own pair assertion. **Measured, not +> derived; the fixtures are shared by pin 10's deliberate choice and cannot be +> separated without the end-before-start segment pin 10 rejects.** + +#### 6.5b — §3's preamble count + +§3's preamble opens a paragraph with: + +> **Four cells were measured, not derived, and the difference matters.** + +**Six are now measured**, and a count left standing beside what it counts is +itself one of the ledger's recurring defects. **Do not edit that sentence** — it +is an accurate statement about what was measured *before ratification*, and +rewriting it would destroy a true historical claim to fix a staleness. Instead +**append to the end of that same paragraph**: + +> **Execution measured a fifth and sixth cell, M1·C6 and M1·C7; amendment 1 +> records them and authorizes their corrected radii.** They are not among the +> four because they reach only tests this contract writes — the criterion that +> sent the other four to measurement was *reaching tests the contract did not +> write*, and that criterion was wrong. **The operative property is whether a +> fixture is shared, not who authored the test.** + +*This is deliberately an append, not a rewrite: the paragraph's subject is the +pre-ratification derivation and its failures, and the amendment is a later event +in the same record.* + +#### 6.5c — the annex append, pinned as a source template + +`spec/EVIDENCE_P13S29_EXECUTION.md` gains a new final section **§8**. **It is +pinned as source, not described by its contents** — a content description admits +a truncated or differently scoped record that still satisfies every "carries X" +clause, which is what an earlier draft of this subsection did. **Exactly one +slot, `{RATIFICATION_HASH}`**; everything else verbatim. + +~~~ +## §8. Amendment 1: resolution and resumption + +Amendment 1 is ratified at `{RATIFICATION_HASH}` and landed by this commit. It +corrects two radius cells in the contract's §3 and changes no pin, test, fixture +or behaviour. + +**§5 and §7 above are the dated execution record and are not edited.** They +state what was expected, what was observed, and why execution stopped. The +mismatch they record is the reason this amendment exists; reconciling them would +remove it. + +### 8.1 The corrected radii + +| M | Dispatched cell (§5) | Corrected cell, measured | +|---|---|---| +| M1·C6 | `tempo_out_of_order_reports_order` | that test **and** `tempo_overlap_reports_order` | +| M1·C7 | `tempo_overlap_reports_order` | that test **and** `tempo_out_of_order_reports_order` | + +Both were observed before the halt. The transcripts in §5.3 and §5.4 stand as +the observation and **were not re-run**: the amendment corrects the expectation +they were compared against, not the observation. + +### 8.2 Resumption + +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. +~~~ + +**Extraction endpoint — the same boundary rule as §6.5c-bis.** §8 runs from its +`## §8.` heading to the **last line before the next `## §` heading, or EOF if +none**. Normalize with §6.5c-bis's canonical serialization, then compare for +**equality**. Not "contains", not "mentions". + +**Later evidence sections are expressly permitted and do not disturb A4.** M2 +onward still needs its transcripts, and they land as **§9 and beyond**. *Had §8 +been defined as "heading to EOF", the very next evidence section would have +invalidated A4 — a gate that the work it gates is guaranteed to break.* + +**§5 is closed at M1 and must not be extended.** It is digest-frozen by +§6.5c-bis, so appending M2's rows to the expected-versus-observed matrix — the +obvious place for them — **would break A4(b).** §9 continues the matrix under +its own heading and carries M2 onward. *This is a consequence of freezing an +open section, and it is stated here because nothing else would warn the +executor before the gate failed.* + +**`landed by this commit`, never a landing hash** — the annex lands *in* that +commit, and pin 12 already states why: *a commit cannot carry its own id.* + +**§5 and §7 are NOT edited.** §5's table keeps its dispatched cells, its two ❌ +marks and its *"the phase is halted at M1"* opening; §7 keeps the finding in the +tense it was found in. §6.5c-bis pins the oracle. + +#### 6.5c-bis — the oracle for §5 and §7 + +**"Byte-identical to their pre-amendment state" needs something durable to +compare against, and the annex is untracked.** Once §8 is appended there is +nothing left to diff. Two measures, both required: + +**1. The ratification act commits the pre-amendment annex.** Ratification stages +`spec/EVIDENCE_P13S29_EXECUTION.md` exactly as it stands at the halt — §1–§7, +**no §8** — under touch row 10. **That commit's blob is the named oracle**, and +A4 is checked with `git show :spec/EVIDENCE_P13S29_EXECUTION.md`. +*This is also what makes the amendment reviewable at all: an untracked evidence +file cannot be cited by a frozen document.* + +**2. Digests, pinned here, as the oracle's oracle.** + +**The canonical byte serialization, pinned exactly — a digest with an inferred +serialization is a digest nobody else can reproduce.** In order: + +1. Read the file as bytes and **decode UTF-8**. The annex is **LF-only**; a CRLF + copy is out of scope and will not reproduce these hashes. +2. Find section starts by `^## §\d+\.` (multiline). A slice runs from its own + heading — **the heading line is included** — to the byte before the next such + heading, or to EOF for the last. +3. Split the slice into lines and **right-strip each line** (trailing spaces and + tabs). +4. **Repeat while the last retained line is empty *or* is exactly `---`: drop + it.** *One loop, not three passes — a `---` and the blank lines around it are + removed together however they interleave.* +5. **Join the retained lines with `\n`, and emit NO terminal newline.** +6. **SHA-256 over the UTF-8 bytes of that string.** + +**Step 5 is the one that actually needs pinning.** An ordinary +`"\n".join(lines) + "\n"` — the natural way to write a file back out — yields +`53b32278…` for §5 and `eb704854…` for §7 instead of the pinned values. *The +digests reproduce only because there is no terminal newline, and nothing in an +earlier draft said so.* + +*Steps 2–3 use `^## §\d+\.` and any line splitter that agrees with LF splitting; +verified that `str.splitlines()` and `split("\n")` produce identical digests for +both slices, the annex containing no form feed, vertical tab or U+2028.* + +| Slice | SHA-256 | Lines | +|---|---|---| +| annex §5 | `40ce82a70339159024c69dd5e280d8bd6846efbeb1eecd5b7971a2737826f74b` | 134 | +| annex §7 | `cdd9bfd91da5091174201b1bc16aea6a5f162cc5f6d8553f6d58d7c56aacccd8` | 76 | + +**The slice rule is what makes the §7 digest stable across the append.** §7 +currently ends at EOF and will end at §8's heading; the rule ends it at the last +non-blank line either way, so **appending §8 must not move either digest.** +*A rule defined as "to EOF" would have made §7's digest change by construction +and the gate unfalsifiable.* + +#### 6.5d — the prohibition on rewriting evidence + +**An earlier draft's gate A4 would have rewritten §5's cells and removed the +halt notice. That is prohibited, and the prohibition is the reason this +subsection exists.** + +§5 and §7 are the **dated record of what was expected, what was observed, and +why execution stopped.** Overwriting the expectation with the corrected one +would leave an annex in which the observed radius matches the recorded cell +everywhere — **an annex that no longer contains the reason this amendment +exists.** The mismatch *is* the evidence. + +**The rule, stated generally:** an execution record is appended to, never +reconciled. A correction is a later event in the record, not a revision of an +earlier one. *This is the same discipline `PASS13_CANDIDATES.md` status cells +already carry — appended to, not rewritten — and the same reason §6.5b appends +to §3's preamble rather than editing its count.* + +### 6.6 The generalization this amendment explicitly declines to make + +**It would be wrong to conclude that same-label conditions always cross-talk.** +The same pass measured the other two shared-label pairs and found no cross-talk +in either: + +- **C4/C5**, sharing `req:time:tempo-segment-shape`: `Constant`-with-mismatch and + non-constant-missing-`end_tempo` are mutually exclusive shapes. +- **C8/C9**, sharing `req:time:aleatoric-reference-locality`: distinct fixtures, + each aggregate carrying exactly one violation. + +**The property that matters is fixture identity, not label identity**, and only +C6/C7 share a fixture shape. + +### 6.7 The defect class, for the ledger + +**The one-hop correction**, the recurring shape: a fact established in one pin +is not carried into the section that depends on it — here within a single table +cell, which cites the shared-fixture property about `f4` in one clause and +overlooks it about pin 10's own tests in the next. + +§3's preamble already records that **all four** of its measured cells differed +from static reading, and measured them because they reached tests the contract +did not write. **C6 and C7 reach tests the contract *did* write — which is why +they were derived rather than measured.** Authorship of a test is not knowledge +of its fixture's reach. + +### 6.8 Gate + +- **A1.** §3's M1 row carries §6.5a's replacement text, and §3's preamble + paragraph carries §6.5b's appended sentences with its opening + *"Four cells were measured"* sentence **unedited**. The superseded sentence + survives in the file **exactly once**, inside §6.1's blockquote, where it is a + dated quotation of what was corrected — **not "absent from the file", which + this amendment makes permanently unsatisfiable by quoting it.** Checked by + stripping blockquote markers and counting: **one** occurrence, and it is + §6.1's. +- **A2.** M1·C6 and M1·C7 each observed, each failing **exactly** + `tempo_out_of_order_reports_order` and `tempo_overlap_reports_order`, with the + failing assertions verbatim in the annex — and each restoring to + `44 / 1604 / 0 / 0`. +- **A3.** **Measured against the halt checkpoint, not against `cea21cd`.** The + ratification commit predates every pin-10 test, so "no test differs from + `cea21cd`" is unsatisfiable by construction — the tests P13-S29 exists to add + necessarily differ from it. The checkpoint is the working tree at the M1 halt: + `44 suites / 1604 passed / 0 failed / 0 ignored`, annex §4. Against it: + **no implementation, test or fixture change is attributable to amendment 1**, + and **no staged hunk in `crates/` belongs to it.** Amendment 1's diff touches + exactly two files, `spec/CONTRACT_P13S29_VIOLATION_KIND.md` and + `spec/EVIDENCE_P13S29_EXECUTION.md`. +- **A4.** Two checks, both mechanical: + + **(a) The append.** The annex's §8, normalized per §6.5c, **equals** §6.5c's + template with `{RATIFICATION_HASH}` filled — including the literal + `landed by this commit`. Whole-section equality, not presence of topics. + + **(b) The preserved record.** Annex §5 and §7, sliced and normalized per + §6.5c-bis, hash to `40ce82a7…f74b` and `cdd9bfd9…ccd8`, and are byte-identical + to the same slices in `git show :spec/EVIDENCE_P13S29_EXECUTION.md`. + Halt notice and ❌ marks intact. **This check is also what observes the + ratification act**: if the ratification commit does not contain the + pre-amendment annex, the `git show` does not resolve and A4(b) cannot pass. + + *A4 observes an append; it must never observe a reconciliation (§6.5d).* +- **A5.** §6's status block carries §6.9's exact ratified form, and — at landing + — its exact landed form and the historical marking. + + **The contract's own top status has two permitted values, and A5 accepts + whichever the landing commit makes true:** + + | Landing | Contract's top status must read | + |---|---| + | Amendment 1 lands **alone**, contract still mid-flight | `STATUS: RATIFIED; DISPATCHED.` — unchanged | + | Amendment 1 lands **in the same commit as P13-S29** | pin 12's exact landed transition, `STATUS: LANDED by this commit.` | + + *An earlier draft required the first unconditionally, which **rejected + compliance with pin 12** in the same-commit case §6.9 explicitly permits — a + gate contradicting a lifecycle the same amendment allows.* **What A5 forbids + in both branches is unchanged: no pin-12 transition attributable to amendment + 1 itself.** *Without A5 the scope table's edit 3 would be a prescribed edit no + gate observes.* + +### 6.9 This amendment's own lifecycle + +**Mirrors pin 12's form for the contract, with the transitions an amendment +needs and a contract does not.** + +- **On ratification:** §6's status block reads exactly + + `STATUS: RATIFIED; FROZEN. Execution of P13-S29 resumes at M2.` + + and the **frozen-amendment statement** is added: + + > The replacements are executed, not edited; a further defect is its own + > amendment with its own review round. + + **This adapts P13-S26's formula and does not reproduce it word for word.** + The precedent reads *"The amended pins are executed, not edited; a further + defect is its own amendment with its own review round."* + (`CONTRACT_P13S26_INVARIANT10_SURFACE.md:1656`). **Amendment 1 amends no pin** + — it replaces two radius cells — so quoting the precedent exactly would assert + something false about this amendment. The second clause is verbatim; the first + substitutes *replacements* for *amended pins*. *An earlier draft claimed exact + reuse while paraphrasing; the claim, not the wording, was the defect.* + +- **Ratification resumes execution, and Amendment 1's own execution comes + first.** The order is pinned: + + 1. **Ratify** — §6's status block takes the form above; the pre-amendment + annex is committed as §6.5c-bis's oracle. + 2. **Apply edits 1, 2 and 4** — the M1 row replacement, the §3 preamble + append, and the annex §8 append. + 3. **Pass A1–A5.** + 4. **Resume the mutation sequence at M2.** + + *"Ratification resumes execution at M2" must not be read as skipping steps 2 + and 3: the amendment has its own execution, and M2 follows it.* + + The resumption point is **M2** — not M1. + M1·C6 and M1·C7 were **already observed** (annex §5.3, §5.4); the amendment + corrects the expectation they were compared against, not the observation. The + tree is unchanged between those runs and this amendment — A3's checkpoint is + what establishes that — so **A2 is discharged by the existing dated + transcripts and requires no re-run.** *Re-running would produce a second, + identical transcript and a record implying the first was doubted.* + +- **On landing:** exactly + + `STATUS: LANDED by this commit.` + + — **no hash**; a commit cannot carry its own id. + +- **On landing**, §6's review-round record is marked a **dated historical + record**, in the form P13-S26 §9 uses: *§6's findings and dispositions are an + account of what was found and decided, and state no current condition.* + +- **P13-S29's own §0-and-above review blocks are NOT marked historical by this + amendment.** Pin 12 marks them **on the contract's landing**, which has not + happened — execution is mid-flight. *Marking them here would date a record + whose subject is still live.* + +**This amendment does not alter pin 12.** The contract's own status block still +reads `STATUS: RATIFIED; DISPATCHED.` and transitions to `LANDED` on the +contract's landing commit, which may be the same commit that lands this +amendment or a later one. diff --git a/spec/EVIDENCE_P13S29_EXECUTION.md b/spec/EVIDENCE_P13S29_EXECUTION.md new file mode 100644 index 0000000..0809ff6 --- /dev/null +++ b/spec/EVIDENCE_P13S29_EXECUTION.md @@ -0,0 +1,438 @@ +# Evidence — P13-S29 execution + +**Not part of the candidate's normative content.** The destination gates 6 and 7 +require: every mutation transcript and boundary-gate output, recorded verbatim +rather than summarised. + +Contract ratified at `cea21cd`. Executed 2026-08-12. + +--- + +## §1. Pin 3's count movement, measured + +Pin 3 requires the requirement to be added **first**, the counts measured, then +the temporary allowlist row removed. Observed on the first run after the +requirement landed and before any constant was touched: + +``` +thread 'requirement_labels_follow_the_grammar' panicked at +crates/epiphany-testkit/tests/requirement_labels.rs:299:5: +assertion `left == right` failed + left: 287 + right: 286 +``` + +`CORE_REQUIREMENT_COUNT` 215 → **216**; `SUITE_REQUIREMENT_COUNT` 286 → **287**; +`SUITE_LABEL_COUNT` 286 → **287**. + +**The citation gate is green for the correct reason**, which gate 12 requires +distinguishing from green-because-still-allowlisted: + +- the temporary `req:time:tempo-segment-shape` row is **absent** from + `DISCUSSED_NOT_CITED`, whose surviving rows are exactly + `req:layoutir:vertical-bands` and `req:graph:aleatoric-reference-locality`; +- `\label{req:time:tempo-segment-shape}` is **present** in `spec/core_spec.tex`, + so the label is *defined*, not excused. + +--- + +## §2. Pin 11's migration, and what failed before it + +After the emission split and before pin 11's migration, the workspace stood at +**1582 passed / 4 failed**, and the four were exactly the migrated positives pin +11 names: + +``` +invariants::accidental_compatibility_tests::cmn_chromatic_accidental_in_edo_31_fires +invariants::review_fix_tests_4::f3_aleatoric_bounds_key_absent_and_reversed_window_fire +invariants::review_fix_tests_4::f3_aleatoric_dag_referencing_absent_event_fires +invariants::review_fix_tests_4::f4_tempo_segment_structural_defects_fire +``` + +**The two accidental negatives did not fail** — they stayed green and vacuous, +exactly as pin 11b predicts, which is why that pin replaces their *predicates* +rather than only their selector. A migration repairing only the loud failures +would have left them passing for a reason unrelated to what they test. + +All nine observations were migrated: five in `review_fix_tests_4`, four in +`accidental_compatibility_tests`. The ghost-region anchor assertion in +`f4_tempo_segment_structural_defects_fire` and the `EventCoordinateModel` +assertion in `f3_aleatoric_bounds_key_absent_and_reversed_window_fire` were +**left as invariant assertions**, per pin 11a. + +--- + +## §3. Five execution faults, recorded rather than left in the transcript + +None is a contract defect; none reached a commit. All are recorded because they +were self-inflicted by *how* the edits were made, because the first is a repeat +of one this rung's family has already paid for, and because the fifth is the +only one no tool would have reported. + +### 3.1 A span replacement deleted `struct DeferredCheck` + +Rewriting the `Display` impl by splicing from +`impl core::fmt::Display for WellFormednessViolation` to the **next** `impl` +swallowed the `pub struct DeferredCheck` declaration, which sat between the two. +Observed as: + +``` +error[E0432]: unresolved imports `invariants::DeferredCheck`, `invariants::InvariantViolation` +error[E0425]: cannot find type `DeferredCheck` in this scope +``` + +**Restored** with its fields and doc comment intact, including the note that +§0.5 excludes it from this rung deliberately. + +**This is the second occurrence of the same defect in this rung's family.** The +first removed mutation **M18** from the P13-S26 contract's §3 during revision M, +also by replacing a span whose endpoints straddled an unrelated neighbour. A +span replacement is silent when it takes something extra: nothing fails, the +text simply no longer exists. + +### 3.2 Line-number targeting edited the wrong module + +Six assertions were rewritten by line number after a grep. Two of them — +reported at `4243` and `4261` — lay in **`review_fix_tests_3`**, not +`review_fix_tests_4`, which begins at `4266`. Both were reverted to their +original `CrossCuttingRefsResolve` form, and the genuine C9 site was located +symbolically at `f3_aleatoric_bounds_key_absent_and_reversed_window_fire`. + +**The rule the contracts already state for locators applies to edits too.** +P13-S16 §7 and P13-S26 §0.6 require symbolic anchors because line numbers drift; +these edits drifted *within a single session*, between one grep and the +replacement that consumed it. **All remaining edits in this execution use +symbolic anchors.** + +### 3.3 Two fixture faults, corrected by reading rather than guessing + +Neither is a contract defect; both were invented shapes that the tree disproves. + +**A C1 fixture assumed `valid_score` carries spanners.** It pushed a ghost staff +onto `cross_cutting.spanners[0]` and panicked: *"index out of bounds: the len is +0 but the index is 0"*. The generator produces no spanners. The fixture now uses +a **dangling staff instrument** — the same `check_cross_cutting_refs` surface, +and stable across generator changes in a way an index into an optional +collection is not. + +**An `AleatoricTimeModel` literal named a field that does not exist** +(`discipline`), failing to compile. Rather than guess the shape, C8 and C9 were +rebuilt on the pattern +`f3_aleatoric_dag_referencing_absent_event_fires` already proves: locate the +aleatoric region by `matches!` on its time model, take its instance-0 voice-0 +events, and install an `EventOrderingDAG` or a `bounds` key naming a ghost. + +*Both faults share the shape of §3.1 and §3.2: a construct written from +expectation instead of from the tree. The difference is that the compiler and a +panic caught these two immediately, where a span replacement and a stale line +number are silent.* + +### 3.4 Two source helpers, deliberately + +`production_source()` now exists twice: privately inside `g3a_tests`, and again +inside `s29_violation_kind_tests`. **This is scoping, not duplication drift.** +Pin 1b requires its derives guard to live in `g3a_tests` **because** that +module's helper is private to it; pin 10's tests are a different module and +cannot reach it. Widening the original's visibility was declined — it would add +surface to satisfy a placement the contract already settled. + +### 3.5 Shared kind bindings made a pinned mutation inapplicable + +`check_tempo_maps` was first written with three shared bindings — + +```rust +let anchor = ViolationKind::Invariant(GraphInvariant::CrossCuttingRefsResolve); +let shape = ViolationKind::Requirement("req:time:tempo-segment-shape"); +let order = ViolationKind::Requirement("req:time:tempo-segment-order"); +``` + +— passed to the `flag` closure at all six emission sites. **§3's M1 requires +"seven separate mutations, one per requirement condition", and §3's column +header requires each mutation be *applicable*.** Under shared bindings it is +not: re-tagging `shape` moves C4 **and** C5 together, and `order` moves C6 and +C7 together. The first two runs made that concrete — a single edit to `shape` +failed four tests, the union of C4's and C5's radii. + +**The six kinds are now written inline at their emission sites and the three +bindings are gone.** Behaviour is identical — `cargo test --workspace` returned +the same `44 suites / 1604 passed / 0 failed / 0 ignored` before and after — and +each condition is now independently re-taggable, which is what M1 asks for. + +*This is an execution fault of the same family as §3.1–§3.4: code written from +what reads well rather than from what the contract has to be able to do to it. +It is the only one of the five that no compiler, panic or assertion would ever +have caught — the mutation simply would have measured something coarser than the +cell it was compared against, and matched a union that looked like a radius.* + +### 3.6 Restoration and baseline + +After both faults were repaired and pin 11's migration completed: + +``` +suites=43 passed=1586 failed=0 ignored=0 +``` + +The rung's structural baseline, unchanged from the ratified input, because +nothing in pins 1–11 adds or removes a test. The new tests of pins 1b and 10 +move it; that movement is recorded in §4 when they land. + +--- + +## §4. Structural baseline after the new tests + +``` +suites=44 passed=1604 failed=0 ignored=0 +cargo +1.95.0 clippy --workspace --all-targets -- -D warnings: clean +cargo +1.95.0 fmt -p epiphany-core -p epiphany-testkit --check: clean +core_spec.pdf rebuilt, 0 undefined references +``` + +**1586 → 1604, and 43 → 44 suites.** Eighteen net-new tests: pin 10's sixteen, +pin 1b's derives guard, and pin 1b's integration test — the last being the new +suite, since `tests/public_surface.rs` is a new integration target. + +**Every mutation radius below is measured against this surface**, not against +the ratified input's. + +### 4.1 Pin 1b's guard found a real defect on its first run + +`violation_types_declare_their_pinned_derives` failed immediately: + +``` +assertion `left == right` failed: ViolationKind's rustdoc is pinned + left: "A violation of a graph invariant: which invariant, and a short witness naming + the smallest offending objects (Chapter 5; QUICKSTART: …). What a + [`WellFormednessViolation`] failed. `Invariant` names a numbered …" + right: "What a [`WellFormednessViolation`] failed. `Invariant` names a numbered …" +``` + +**The old `InvariantViolation` rustdoc had survived**, stranded above +`ViolationKind` when the enum was inserted before the struct. Nothing else in the +suite could see it: it is prose, and every other assertion is behavioural. It was +removed. + +*This is the case pin 1b was written for — round 15 called the derives and +rustdocs "prose that no test or gate reads", and the first thing the new guard +read was a stale one.* + +--- + +## §5. Expected-versus-observed matrix + +**The phase is halted at M1.** Five of the seven M1 conditions matched their §3 +cells exactly; **M1·C6 and M1·C7 did not**, and the difference is a defect in +§3, not in the tree. §7 states the finding; the remaining mutations (M2 onward) +are **not run** and this section stays open until the amendment lands. + +Every row below was run as `cargo test --workspace --no-fail-fast` against the +§4 surface (`44 / 1604 / 0 / 0`), with a `cargo build --tests --workspace` +compile check first — **a mutation that does not compile observed nothing** — +and restored by hand write-back. + +| M | §3 cell | Observed | | +|---|---|---|---| +| M1·C4 | 2 | 2 | ✅ | +| M1·C5 | 3 | 3 | ✅ | +| M1·C6 | 1 | **2** | ❌ | +| M1·C7 | 1 | **2** | ❌ | +| M1·C8 | 4 | 4 | ✅ | +| M1·C9 | 2 | 2 | ✅ | +| M1·C10 | 3 | 3 | ✅ | + +### 5.1 M1·C4 — `tempo_constant_mismatch_reports_shape` + +Cell: that test **plus** `f4_tempo_segment_structural_defects_fire`. Observed +`1602 passed / 2 failed`, exactly those two. + +### 5.2 M1·C5 — `tempo_nonconstant_missing_end_reports_shape` + +Cell: that test, `f4_tempo_segment_structural_defects_fire`, and +`requirement_selector_discriminates_its_payload` — pin 10 builds the requirement +discriminator from C5 and C8. Observed `1601 passed / 3 failed`, exactly those +three. + +### 5.3 M1·C6 — MISMATCH + +**Cell: `tempo_out_of_order_reports_order` alone. Observed two.** + +``` +passed=1602 failed=2 + invariants::s29_violation_kind_tests::tempo_out_of_order_reports_order + invariants::s29_violation_kind_tests::tempo_overlap_reports_order + +---- invariants::s29_violation_kind_tests::tempo_out_of_order_reports_order stdout ---- +thread '...tempo_out_of_order_reports_order' panicked at +crates/epiphany-core/src/invariants.rs:6677:9: +aggregate must carry (Requirement("req:time:tempo-segment-order"), "tempo segments are +out of start order"); got [(Invariant(CrossCuttingRefsResolve), "tempo segments are out +of start order"), (Requirement("req:time:tempo-segment-order"), "tempo segments overlap +in musical time")] + +---- invariants::s29_violation_kind_tests::tempo_overlap_reports_order stdout ---- +thread '...tempo_overlap_reports_order' panicked at +crates/epiphany-core/src/invariants.rs:6681:9: +the rider must not answer to invariant 10; got [WellFormednessViolation { kind: +Invariant(CrossCuttingRefsResolve), witness: "tempo segments are out of start order" }] +``` + +**The second failure is pin 10's own fourth assertion, on the sibling test.** + +### 5.4 M1·C7 — MISMATCH, symmetrically + +**Cell: `tempo_overlap_reports_order` alone. Observed the same two, with the +roles exchanged.** + +``` +passed=1602 failed=2 + invariants::s29_violation_kind_tests::tempo_out_of_order_reports_order + invariants::s29_violation_kind_tests::tempo_overlap_reports_order + +---- invariants::s29_violation_kind_tests::tempo_out_of_order_reports_order stdout ---- +thread '...tempo_out_of_order_reports_order' panicked at +crates/epiphany-core/src/invariants.rs:6681:9: +the rider must not answer to invariant 10; got [WellFormednessViolation { kind: +Invariant(CrossCuttingRefsResolve), witness: "tempo segments overlap in musical time" }] + +---- invariants::s29_violation_kind_tests::tempo_overlap_reports_order stdout ---- +thread '...tempo_overlap_reports_order' panicked at +crates/epiphany-core/src/invariants.rs:6677:9: +aggregate must carry (Requirement("req:time:tempo-segment-order"), "tempo segments +overlap in musical time"); got [(Requirement("req:time:tempo-segment-order"), "tempo +segments are out of start order"), (Invariant(CrossCuttingRefsResolve), "tempo segments +overlap in musical time")] +``` + +### 5.5 M1·C8 — `aleatoric_ordering_outside_region_reports_locality` + +Cell: that test, `f3_aleatoric_dag_referencing_absent_event_fires`, +`mixed_fixture_splits_by_arm` (C8 is in the pinned mixed fixture), and +`requirement_selector_discriminates_its_payload`. Observed `1600 / 4`, exactly +those four. + +``` +thread '...f3_aleatoric_dag_referencing_absent_event_fires' panicked at invariants.rs:4325:9: +assertion failed: fires_req(&s, "req:time:aleatoric-reference-locality") + +thread '...mixed_fixture_splits_by_arm' panicked at invariants.rs:7040:9: +aggregate must carry the rider as its requirement; got [ ... kind: Invariant( +CrossCuttingRefsResolve), witness: "tempo segment start anchor target ... dangling" }, +... kind: Invariant(CrossCuttingRefsResolve), witness: "aleatoric region ... ordering +references event ..., absent from the region" }] +``` + +### 5.6 M1·C9 — `aleatoric_bounds_outside_region_reports_locality` + +Cell: that test plus `f3_aleatoric_bounds_key_absent_and_reversed_window_fire`. +Observed `1602 / 2`, exactly those two. + +### 5.7 M1·C10 — `accidental_incompatible_reports_tuning_requirement` + +Cell: that test, the migrated `cmn_chromatic_accidental_in_edo_31_fires`, and +`display_renders_each_arm_exactly`, whose requirement side uses a real +accidental violation. Observed `1601 / 3`, exactly those three. + +### 5.8 What the five matching rows establish about the two that did not + +**The sibling-fixture hazard is specific to C6/C7 and measurably absent +elsewhere**, which is why the correction must not be generalized into a blanket +rule about shared labels: + +- **C4/C5 share the label `req:time:tempo-segment-shape`** and did **not** + cross-talk: C4's fixture is `Constant` with a mismatched `end_tempo`, C5's is + non-constant with none, and neither shape can emit the other's condition. +- **C8/C9 share `req:time:aleatoric-reference-locality`** and did **not** + cross-talk: each aggregate in the transcripts above carries exactly one + violation, so the fixtures are genuinely disjoint. +- **C6/C7 share `req:time:tempo-segment-order` and cannot be made disjoint** — + pin 10 says so and rules out the fixture that would separate them. + +**Restoration after every row**, verified by full run: + +``` +suites=44 passed=1604 failed=0 ignored=0 +``` + +--- + +## §6. Gate 6 — pin 9's boundary check, verbatim + +*(pending)* + +--- + +## §7. Finding against §3: M1·C6 and M1·C7's radii + +**Reported, not patched.** The pins are frozen; this needs an amendment with its +own review round, and the mutation phase stays halted until one lands. + +### 7.1 What §3 says + +> **C6 and C7 fail their pin-10 test alone**: the legacy `f4` assertion is one +> fixture tripping *both*, so re-tagging one leaves the other still reporting the +> same label and the legacy assertion still passes + +### 7.2 Why it is wrong + +**The quoted sentence is true about `f4`, and `f4` is indeed not in either +radius** — measurement confirms it. The error is that the derivation *stopped at +the legacy observer*. It never asked the same question of pin 10's own C6 and C7 +tests, which share the fixture **shape**. + +Pin 10 pins **four** assertions per C4–C10 row. The fourth is: + +> the aggregate's **invariant arm is empty** + +and pin 10 states the fixture relationship outright: + +> C6's natural fixture — `seg(2,3)` then `seg(1,2)` — is *also* overlapping, so +> it emits C6 **and** C7 under the same label. + +Both tests are built by `two_segments(seed, (2, 3), (1, 2))`, differing only in +the seed. So re-tagging **either** condition puts an `Invariant` violation into +**both** fixtures, and the sibling's fourth assertion fails. The radius is two, +not one, in both directions. + +### 7.3 The tree is correct; the cell is not + +**No implementation change can reconcile them, and none should be attempted.** +The only fixture that isolates C6 needs `seg1.end < seg1.start` — an +end-before-start segment — and pin 10 **explicitly rejects it**: + +> *The alternative to pairs — an isolated C6 fixture — would need an +> end-before-start segment, which is unnatural and tests a shape the checker +> should never see.* + +Pin 10 chose shared fixtures deliberately and §3 then costed them as though it +had not. **Changing the fixtures to fit §3 would violate pin 10**; changing the +fourth assertion would discard the property §3's own M2a derivation leans on. + +### 7.4 The defect class + +**The one-hop correction** — the ledger's recurring shape, and named as such in +this rung's own review history. A fact is established in one place (pin 10: this +fixture emits both conditions) and not carried into the place that depends on it +(§3: what fails when one of them moves). §3 even *cites* the shared-fixture +property, in the same cell, about a different observer. + +It is also the fifth instance of the pattern §3's preamble already documents: + +> Every one of the four differed from what static reading predicted + +Four cells were measured because they reached tests the contract did not write. +**C6 and C7 reach tests the contract *did* write — which is exactly why they +were derived instead of measured, and exactly why the derivation was trusted.** +Authorship of a test is not knowledge of its fixture's reach. + +### 7.5 The measured replacement + +| M | Radius | +|---|---| +| M1·C6 | `tempo_out_of_order_reports_order` **and** `tempo_overlap_reports_order` | +| M1·C7 | the same two | + +Measured, not derived; transcripts in §5.3 and §5.4. + +**This strengthens M1 rather than weakening it.** Under the pinned cell a +re-tagging that broke only the sibling would have read as a radius mismatch; +under the corrected cell each of C6 and C7 is observed by two independent +assertions — its own pair assertion and the sibling's invariant-arm assertion.