P13-S26 amendment 3 EXECUTED: test 3 selects the normative clause

Test 3 asserted phrase presence over the whole requirement block, so a referent
could leave the sentence carrying the normative force and survive in the closing
recap. Execution measured that escape and the annex recorded it; this commit
closes it by strengthening the guard rather than softening pin 4a's claim.

Test 3 now selects the normative clause -- the sentence carrying the sole
\MUST{} -- and runs all four assertions on that slice alone. Both halves of the
start rule are load-bearing and the helper's doc comment says why: last ". "
before the occurrence, falling back to just after the label only when there is
none. An unconditional fallback would return one slice spanning label to recap,
containing every needle; a period-only rule would swallow the label, which is
not a sentence.

Six mutations, six matching radii, test 3 alone in every case. Each attacks a
different layer: M22-M24 vary what the selected clause contains, M25 varies
which sentence is selected, M26 varies the fallback boundary -- starting after
the label versus widening before it -- and M27 varies whether selection is
unambiguous and therefore permitted at all. M27 is the one that reaches the
exactly-one assertion, because an assertion guarding the precondition of
selection cannot be exercised by any mutation that presupposes selection
succeeded.

Rows 4, 6, 7 and 8 only. core_spec.tex is not touched: the requirement's text
was always correct and only the guard was weak. The rung's original 38/38
matrix is preserved unchanged and amendment 3's evidence is appended beside it,
not merged into it.

One prose defect in ratified section 8.4 remains OPEN and is deliberately not
repaired here: that entry says M27 varies which clause is chosen, which M25 does
and M27 does not, since a correct implementation rejects M27 before selecting
any clause. Section 8.6 is unaffected and states something true. The annex
carries the corrected characterization and records the correction as open;
frozen text stays frozen regardless of severity, so the repair belongs to its
own amendment, which is not part of this commit.

Baseline unchanged at 43 suites, 1586 passing: amendment 3 alters an existing
test's scope and adds none.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x

crates/epiphany-testkit/tests/invariant_ten_surface.rs

@@ -382,12 +382,49 @@ fn implementation_doc_names_exactly_the_derived_surface() {
     assert_eq!(actual, expected);
 }
 
+/// Select the requirement's **normative clause** -- the sentence carrying its
+/// sole `\MUST{}` -- from a normalised requirement block.
+///
+/// Both halves of the start rule are load-bearing (P13-S26 amendment 3, 8.3).
+/// The last-period rule is what makes the clause follow `\MUST{}` when the
+/// normative force moves to a later sentence; without it, a slice anchored
+/// unconditionally after the label would span label to recap and contain every
+/// needle. The fallback is needed because the normative sentence is *first* in
+/// this requirement, so no preceding ". " exists and a block-start default
+/// would swallow the label, which is not a sentence.
+fn normative_clause<'a>(block: &'a str, label: &str) -> &'a str {
+    let occurrences = block.matches("\\MUST{}").count();
+    assert_eq!(
+        occurrences, 1,
+        "the requirement must carry exactly one \\MUST{{}}; found {occurrences}. \
+         More than one leaves the normative clause ambiguous, and an \
+         implementation that silently took the first would scope every other \
+         assertion to whichever sentence happened to come first.\nBlock was:\n{block}"
+    );
+    let p = block.find("\\MUST{}").expect("checked above");
+
+    let start = match block[..p].rfind(". ") {
+        Some(period) => period + ". ".len(),
+        None => {
+            let at = block.find(label).expect("the block declares its label");
+            at + label.len()
+        }
+    };
+    let end = match block[p..].find(". ") {
+        Some(period) => p + period + 1,
+        None => block.len(),
+    };
+    block[start..end].trim()
+}
+
 #[test]
 fn aleatoric_reference_locality_states_both_referents_and_locality() {
-    // Phrase presence, not exact comparison -- weaker than the two tests above,
+    // Phrase presence, not exact comparison -- weaker than tests 1 and 2, and
-    // and stated as such rather than presented as equivalent coverage. What it
+    // stated as such. What it buys, since P13-S26 amendment 3: the phrases must
-    // buys: neither referent, nor the locality claim, nor the requirement's
+    // appear in the NORMATIVE CLAUSE, not merely somewhere in the block.
-    // normative force can silently leave.
+    // Execution measured the escape that motivated this: a referent deleted
+    // from the clause but left standing in the closing recap passed the
+    // block-scoped form.
     let spec = normalise(&read("spec/core_spec.tex"));
     let label = r"\label{req:time:aleatoric-reference-locality}";
     let at = spec
@@ -402,11 +439,15 @@ fn aleatoric_reference_locality_states_both_referents_and_locality() {
         .expect("that requirement block is closed");
     let block = &spec[start..end];
 
+    let clause = normative_clause(block, label);
+
     for needle in ["ordering", "bounds", "same region", "\\MUST{}"] {
         assert!(
-            block.contains(needle),
+            clause.contains(needle),
-            "req:time:aleatoric-reference-locality must state {needle:?}; \
+            "req:time:aleatoric-reference-locality's normative clause must state \
-             block was:\n{block}"
+             {needle:?}; the clause is the sentence carrying \\MUST{{}}, and a \
+             phrase surviving elsewhere in the block does not count.\n\
+             Clause was:\n{clause}"
         );
     }
 }

spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md

@@ -2089,10 +2089,15 @@ pin 3 with amendment 1's shape unchanged.
 
 ## §8. AMENDMENT 3 — TEST 3'S CLAUSE SCOPE, POST-EXECUTION
 
-STATUS: RATIFIED; DISPATCHED to clause-scope test 3.
+STATUS: LANDED by this commit.
 
-**Ratified 2026-08-11 on the authority of the repository owner**, review round 4
+> **DATED HISTORICAL RECORD — amendment 3 is ratified and executed. Its
-returning zero findings. The rung landed at `eddf6e9`; **this amendment does not
+> revision records, its finding statement and §8.6's disposition are an
+> account of what was found and decided on 2026-08-11. None of it states
+> current state.**
+
+**Ratified 2026-08-11 at `7c8a30d` on the authority of the repository owner**,
+review round 4 returning zero findings. The rung landed at `eddf6e9`; **this amendment does not
 reopen it.** The amended surface is executed, not edited; a further defect is its
 own amendment with its own review round.
 

spec/EVIDENCE_P13S26_EXECUTION.md

@@ -1110,3 +1110,217 @@ cargo +1.95.0 fmt -p epiphany-core -p epiphany-testkit --check: clean
 Exactly the structural baseline of §1. Every restoration was a hand write-back
 of captured bytes; `git checkout`, `git restore` and `git stash` were never used
 against the working tree.
+
+
+---
+
+# Amendment 3 evidence — test 3's clause scope
+
+**Appended, not merged.** Everything above is the historical record of the
+rung's own execution and is unchanged, including its 38/38 matrix. This section
+records amendment 3 (`7c8a30d`), whose execution touches touch rows 4, 6, 7 and
+8 only. `spec/core_spec.tex` is not modified: the requirement's text was always
+correct, and only the guard was weak.
+
+## A3.§1 What changed
+
+Test 3 previously asserted phrase presence over the **whole requirement block**.
+It now selects the **normative clause** — the sentence carrying the sole
+`\MUST{}` — and runs all four assertions on that slice alone.
+
+The selector, per amendment 3 §8.3: assert exactly one `\MUST{}` in the
+normalised block; start the clause after the **last `". "` at or before** that
+occurrence, falling back to just after the `\label{…}` **only when there is
+none**; end after the first `". "` at or after it.
+
+## A3.§2 Expected-versus-observed
+
+| M | # | Expected | Observed | Verdict |
+|---|---|---|---|---|
+| M22 | 1 | `aleatoric_reference_locality_states_both_referents_and_locality` | same | **MATCH** |
+| M23 | 1 | `aleatoric_reference_locality_states_both_referents_and_locality` | same | **MATCH** |
+| M24 | 1 | `aleatoric_reference_locality_states_both_referents_and_locality` | same | **MATCH** |
+| M25 | 1 | `aleatoric_reference_locality_states_both_referents_and_locality` | same | **MATCH** |
+| M26 | 1 | `aleatoric_reference_locality_states_both_referents_and_locality` | same | **MATCH** |
+| M27 | 1 | `aleatoric_reference_locality_states_both_referents_and_locality` | same | **MATCH** |
+
+**Six mutations, six matches**, each with test 3 as its sole radius. No listed
+test passed unexpectedly; no unlisted test failed.
+
+**Each signs a different step, which is the point of there being six.** M22 and
+M23 sign the referents' clause scope; M24 the locality phrase; M25 the
+last-period rule — it moves `\MUST{}` into a later sentence, and an
+implementation anchoring unconditionally after the label would return one slice
+from label to recap containing every needle, and pass; M26 the fallback anchor,
+via a period-free decoy that a correct fallback excludes and a block-start
+fallback includes; M27 the exactly-one assertion.
+
+**Each attacks a different layer, and this is the taxonomy the annex uses:**
+
+| Mutation | What it varies |
+|---|---|
+| M22, M23, M24 | what the selected clause **contains** |
+| M25 | **which sentence** is selected |
+| M26 | the **fallback boundary** — starting after the label versus widening before it |
+| M27 | whether selection is **unambiguous, and therefore permitted at all** |
+
+**One sentence in ratified §8 is inconsistent with that, and this annex does not
+repeat it.** §8.4's M27 entry closes by saying M27 *"varies which clause is
+chosen"*. It does not: **M25** varies which clause is chosen, and a correct
+implementation rejects M27 **before selecting any clause**, on the exactly-one
+assertion. *(§8.6 is unaffected — it says only that M27 was the step no mutation
+had reached, which is true.)*
+
+The sentence is frozen in a ratified section, so it is **corrected through the
+amendment lifecycle, not silently rewritten**. That correction is **open** as of
+this commit and is not part of it.
+
+## A3.§3 Mutation transcripts
+
+### M22
+
+*Mutation.* `ordering` leaves the normative clause, survives in the recap
+
+*Complete `--no-fail-fast` failure set* (full workspace, 1585 passed / 1 failed):
+
+```
+  aleatoric_reference_locality_states_both_referents_and_locality
+```
+
+*Failing assertion, verbatim:*
+
+```
+---- aleatoric_reference_locality_states_both_referents_and_locality stdout ----
+
+thread 'aleatoric_reference_locality_states_both_referents_and_locality' (2099485) panicked at crates/epiphany-testkit/tests/invariant_ten_surface.rs:445:9:
+req:time:aleatoric-reference-locality's normative clause must state "ordering"; the clause is the sentence carrying \MUST{}, and a phrase surviving elsewhere in the block does not count.
+Clause was:
+Every event used as a key in an aleatoric region's \texttt{bounds} map \MUST{} be an event of that same region.
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+```
+### M23
+
+*Mutation.* `bounds` leaves the clause, survives in the recap
+
+*Complete `--no-fail-fast` failure set* (full workspace, 1585 passed / 1 failed):
+
+```
+  aleatoric_reference_locality_states_both_referents_and_locality
+```
+
+*Failing assertion, verbatim:*
+
+```
+---- aleatoric_reference_locality_states_both_referents_and_locality stdout ----
+
+thread 'aleatoric_reference_locality_states_both_referents_and_locality' (2101173) panicked at crates/epiphany-testkit/tests/invariant_ten_surface.rs:445:9:
+req:time:aleatoric-reference-locality's normative clause must state "bounds"; the clause is the sentence carrying \MUST{}, and a phrase surviving elsewhere in the block does not count.
+Clause was:
+Every event referenced by an aleatoric region's \texttt{ordering} DAG \MUST{} be an event of that same region.
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+```
+### M24
+
+*Mutation.* the locality phrase leaves the clause, appears in the recap
+
+*Complete `--no-fail-fast` failure set* (full workspace, 1585 passed / 1 failed):
+
+```
+  aleatoric_reference_locality_states_both_referents_and_locality
+```
+
+*Failing assertion, verbatim:*
+
+```
+---- aleatoric_reference_locality_states_both_referents_and_locality stdout ----
+
+thread 'aleatoric_reference_locality_states_both_referents_and_locality' (2102882) panicked at crates/epiphany-testkit/tests/invariant_ten_surface.rs:445:9:
+req:time:aleatoric-reference-locality's normative clause must state "same region"; the clause is the sentence carrying \MUST{}, and a phrase surviving elsewhere in the block does not count.
+Clause was:
+Every event referenced by an aleatoric region's \texttt{ordering} DAG, and every event used as a key in its \texttt{bounds} map, \MUST{} be an event of that region.
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+```
+### M25
+
+*Mutation.* `\MUST{}` moves to the recap, taking the clause with it
+
+*Complete `--no-fail-fast` failure set* (full workspace, 1585 passed / 1 failed):
+
+```
+  aleatoric_reference_locality_states_both_referents_and_locality
+```
+
+*Failing assertion, verbatim:*
+
+```
+---- aleatoric_reference_locality_states_both_referents_and_locality stdout ----
+
+thread 'aleatoric_reference_locality_states_both_referents_and_locality' (2104554) panicked at crates/epiphany-testkit/tests/invariant_ten_surface.rs:445:9:
+req:time:aleatoric-reference-locality's normative clause must state "same region"; the clause is the sentence carrying \MUST{}, and a phrase surviving elsewhere in the block does not count.
+Clause was:
+Neither the ordering DAG nor the bounds map \MUST{} reach outside the region whose time model declares them.
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+```
+### M26
+
+*Mutation.* M22's replacement **plus** a period-free `ordering` decoy before the label
+
+*Complete `--no-fail-fast` failure set* (full workspace, 1585 passed / 1 failed):
+
+```
+  aleatoric_reference_locality_states_both_referents_and_locality
+```
+
+*Failing assertion, verbatim:*
+
+```
+---- aleatoric_reference_locality_states_both_referents_and_locality stdout ----
+
+thread 'aleatoric_reference_locality_states_both_referents_and_locality' (2106230) panicked at crates/epiphany-testkit/tests/invariant_ten_surface.rs:445:9:
+req:time:aleatoric-reference-locality's normative clause must state "ordering"; the clause is the sentence carrying \MUST{}, and a phrase surviving elsewhere in the block does not count.
+Clause was:
+Every event used as a key in an aleatoric region's \texttt{bounds} map \MUST{} be an event of that same region.
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+```
+### M27
+
+*Mutation.* the normative sentence unchanged; the recap gains a **second** `\MUST{}`
+
+*Complete `--no-fail-fast` failure set* (full workspace, 1585 passed / 1 failed):
+
+```
+  aleatoric_reference_locality_states_both_referents_and_locality
+```
+
+*Failing assertion, verbatim:*
+
+```
+---- aleatoric_reference_locality_states_both_referents_and_locality stdout ----
+
+thread 'aleatoric_reference_locality_states_both_referents_and_locality' (2107954) panicked at crates/epiphany-testkit/tests/invariant_ten_surface.rs:397:5:
+assertion `left == right` failed: the requirement must carry exactly one \MUST{}; found 2. More than one leaves the normative clause ambiguous, and an implementation that silently took the first would scope every other assertion to whichever sentence happened to come first.
+Block was:
+\begin{requirement} \label{req:time:aleatoric-reference-locality} Every event referenced by an aleatoric region's \texttt{ordering} DAG, and every event used as a key in its \texttt{bounds} map, \MUST{} be an event of that same region. Naming an event that does not exist is a dangling reference, governed by graph invariant~10; naming an event that exists in a \emph{different} region is a distinct defect, and this requirement is what forbids it. Neither the ordering DAG nor the bounds map \MUST{} reach outside the region whose time model declares them.
+  left: 2
+ right: 1
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+```
+
+## A3.§4 Restoration
+
+```
+suites=43 passed=1586 failed=0 ignored=0
+```
+
+Unchanged from the rung's own structural baseline: amendment 3 alters an
+existing test's scope and adds none. Every restoration was a hand write-back of
+captured bytes.
+
+## A3.§5 The finding this closes
+
+`eddf6e9` recorded, in §6(b) above, that pin 4a claimed test 3 buys that
+*"neither referent … can silently leave"*, and that measurement showed
+otherwise. **That finding is now closed by strengthening the guard rather than
+softening the claim** — pin 4a's sentence is true of the clause-scoped test.
+Pin 4a itself is frozen and unedited; amendment 3 is an additive override and
+governs from its ratification.