S16 draft amendment 1 rev D: a requirement no assertion can fail is not a requirement

Independent review of 25473a1 returned two blocking findings. A sweep
escalated one of them into a third. Both reported findings are the same
failure in different clothes: a requirement stated with nothing able to fail
it.

1. Pin 10a still deferred the label decision to execution -- twice reworded,
   never decided. The facts were readable in the .tex source the whole time:
   core_spec.tex:6529-:6648 is ONE requirement box carrying the single label
   req:graph:score-graph-invariants, with exactly 20 \items inside it.
   Invariant 21 is a 21st \item within that box, so pin 6 mints nothing. Pin
   10 rewrites prose plus a Revision History row and version bump, so it mints
   nothing either.

   DECIDED: neither document mints a label; touch row 11 is UNUSED and must
   not be staged; no counter moves. If execution finds otherwise that is a
   finding against this contract, not a keyboard decision. The counter table
   is retained for that case and for the next rung. Row 11 is kept rather than
   deleted because CLAUDE.md names the file as a recurring escapee -- a row
   reading "deliberately unused, and why" survives review; an absent row looks
   like an oversight.

   "Decide and report" reads like rigour and is its opposite: it makes the
   staged set and counter expectations depend on a choice made at the
   keyboard, so the touch table can be wrong in either direction and the
   report will agree with whatever happened.

2. Pin 6a required each fixture to violate its own direction only, and nothing
   could observe that. The prescribed model, m40, asserts only
   check_invariants(&s).iter().any(...) -- any() cannot see a second unrelated
   defect -- and gate 6 checked the target verdict and the opposite direction
   but never the absence of invariants 1-20. So a fixture carrying an
   unrelated second defect satisfied every stated gate and mutation outcome.

   Each m41/m41b must now assert the EXACT violation set: exactly one
   violation, StaffGroupMembershipAgreement, witness naming that direction's
   staff and group ids, opposite direction asserted satisfied. Gate 6 reports
   check_invariants' full return for both.

   Borrowing a test's shape imports its blind spots along with its virtue. m40
   was cited for its dispatch property, which is real and still applies;
   nothing about invariant 20 ever turned on exactness.

3. Sweep: the same blind spot covers touch row 8's generator, and worse.
   negative_generators_are_reasonably_targeted bounds kinds:
   BTreeSet<GraphInvariant> at <= 3, but both directions of invariant 21 are
   the SAME variant -- they collapse to one element, so no existing test can
   observe direction at all; the other three all() loops assert only
   !is_empty(). Row 8 now requires a dedicated permanent test that the
   generator violates S->G and not G->S.

Also fixed: revision D's block was first inserted inside revision C's,
orphaning C's closing paragraphs after it. Reordered, and the cross-revision
pattern paragraph moved to the end and extended.

That paragraph now carries rev D's converse: the fix-every-site rule asks who
READS a corrected rule; rev D asks what OBSERVES each requirement. Findings 2
and 3 were invisible to every sweep that looks for restated text, because
nothing was restated. A rule with no consumer goes stale; a rule with no
observer was never enforced at all.

Still DRAFT, still unratified. No implementation work has begun.

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

spec/CONTRACT_P13S16_PROJECTION.md

@@ -109,18 +109,47 @@ restated away from its origin. Removed, pin 8's table named instead.
 | **2** | **"One named direction" delegated a design decision to execution.** Either choice changes the generated witness and the shrink evidence, so reporting it afterward is not specifying it | **Pinned to S→G** in touch row 8, with the reason: smallest corruption of `valid_score`, matching every other arm's doctrine, **and the exact shape pin 2's append failing produces** — what M2 observes |
 | 3 | **§6's revision-B history said §4 has "twelve entries — 1–11 plus 4a"**, a false identity: `4a.` was a gate-numbered **scope note** with no command and no output, colliding with **§4a**, the landing-obligation section | The note is **demoted out of the gate numbering** into gate 4's body. §4 now has **eleven gates, 1–11**; `§4a` is unambiguous |
 
-**Finding 1 is the strongest evidence yet for a rule this contract already states and
+**Revision C's finding 1 is the strongest evidence for a rule this contract already
-did not apply to itself.** Pin 3a says *"a mutation demonstrates the hazard once; only a
+states and did not apply to itself.** Pin 3a says *"a mutation demonstrates the hazard
-test keeps it demonstrated."* M6 was carrying both directions on mutation alone, three
+once; only a test keeps it demonstrated."* M6 was carrying both directions on mutation
-sections below that sentence. **Every branch a contract mandates needs a permanent test,
+alone, three sections below that sentence. **Every branch a contract mandates needs a
-and a mutation is that test's signature — never its substitute.**
+permanent test, and a mutation is that test's signature — never its substitute.**
 
-**The pattern across revisions A, B and C is sharper than any individual finding: a
+### Draft amendment 1, revision D — independent review of `25473a1`
-correction propagates one hop and stops.** Rev A fixed pin 10a and left touch row 11; the
+
-sweep caught row 11 and the fix stopped before §6's consumer. Rev A removed item 1's
+**Two blocking findings, plus one the sweep escalated.** Both reported findings are the
-mutation tally and left item 2's gate tally on the next line. **The fix-every-site rule is
+same failure in different clothes: **a requirement stated with nothing able to fail it.**
-not satisfied by fixing the site *and* its obvious neighbour** — it requires asking who
+
-*reads* the corrected rule, and correcting them too.
+| # | Finding | Disposition |
+|---|---|---|
+| **1** | **Pin 10a still deferred the label decision to execution** — twice reworded, never decided. The facts were readable the whole time: `core_spec.tex:6529`–`:6648` is **one `requirement` box** carrying the single label `req:graph:score-graph-invariants`, with exactly **20 `\item`s**; invariant 21 is a 21st `\item` **inside** it. Pin 10 rewrites prose plus a Revision History row | **DECIDED: neither document mints a label. Row 11 is UNUSED and MUST NOT be staged. No counter moves.** If execution finds otherwise, that is a **finding against this contract**, not a decision to take at the keyboard. The counter table is retained for that case |
+| **2** | **Pin 6a required each fixture to violate its direction only, and nothing could observe it.** The prescribed shape, `m40`, asserts `check_invariants(&s).iter().any(...)` — **`any()` cannot see a second unrelated defect** — and gate 6 checked the target verdict and the opposite direction, but never the absence of invariants 1–20 | Each `m41`/`m41b` must assert the **EXACT violation set**: one violation, `StaffGroupMembershipAgreement`, witness naming the direction's staff and group ids, opposite direction asserted satisfied. **Gate 6 reports the full return of `check_invariants` for both** |
+| **3** | *(sweep)* **The same blind spot covers touch row 8's generator, and worse.** `negative_generators_are_reasonably_targeted` bounds `kinds: BTreeSet<GraphInvariant>` at `<= 3`, but **both directions of invariant 21 are the same variant** — they collapse to one element, so **no existing test can observe direction at all**; the other three `all()` loops assert only `!is_empty()` | Row 8 now requires a **dedicated permanent test** that the generator violates S→G and not G→S |
+
+**Finding 2 names the failure mode precisely: a requirement no assertion can fail is not
+a requirement.** Pin 6a demanded isolation and, in the same breath, pointed at a model
+test that cannot check isolation. **Borrowing a test's shape imports its blind spots
+along with its virtue** — `m40` was cited for its dispatch property, which is real and
+still applies, and nothing about invariant 20 ever turned on exactness.
+
+**Finding 1 closes the last conditional in the contract.** *"Decide and report"* reads
+like rigour and is its opposite: it makes the staged set and the counter expectations
+depend on a choice made at the keyboard, so **the touch table can be wrong in either
+direction and the report will agree with whatever happened.** Where the facts are
+readable — and these were, in the `.tex` source — the contract decides.
+
+**The pattern across revisions A–D is sharper than any individual finding: a correction
+propagates one hop and stops.** Rev A fixed pin 10a and left touch row 11; the sweep
+caught row 11 and stopped before §6's consumer; rev D found pin 10a's *decision* still
+deferred after two reworders. Rev A removed item 1's mutation tally and left item 2's
+gate tally on the next line. **The fix-every-site rule is not satisfied by fixing the
+site *and* its obvious neighbour** — it requires asking who *reads* the corrected rule,
+and correcting them too.
+
+**And rev D adds its converse:** ask what *observes* each requirement. Findings 2 and 3
+were both requirements with no assertion able to fail them — invisible to every sweep
+that looks for restated text, because nothing was restated. **A rule with no consumer
+goes stale; a rule with no observer was never enforced at all.**
 
 > **The original status, retained:** *DRAFT — BLOCKED on P13-S27. Not executable as
 > written. Pin 0 exposes that no authority defines the implementation's current
@@ -558,6 +587,31 @@ reported after either arm is deleted, so it signs neither — the same isolation
 requires, made permanent. **Each test must state in its doc which direction it holds
 and which it breaks**, so a later reader cannot "simplify" the two into one.
 
+**Each test MUST assert the EXACT violation set, not membership. ADDED IN REVISION D.**
+
+`m40_check_invariants_dispatches_invariant_20` — the shape this pin points at — asserts
+only that the target **appears**:
+`check_invariants(&s).iter().any(|v| v.invariant == …)`. **`any()` cannot detect a
+second, unrelated defect**, so a fixture carrying one satisfies m40's shape, satisfies
+gate 6, and satisfies M6's deletion outcome — while violating pin 6a's own
+"only its own direction" requirement, which nothing then observes. **A requirement no
+assertion can fail is not a requirement.**
+
+So each of `m41` / `m41b` MUST assert:
+
+1. **`check_invariants(&s)` returns EXACTLY one violation**, and its `invariant` is
+   `StaffGroupMembershipAgreement` — an exact-set assertion, not `any()`. This is what
+   proves invariants 1–20 are satisfied, which `any()` never touches.
+2. **The witness names the specific staff and group ids** for that direction, so the two
+   tests cannot pass on each other's fixture.
+3. **The opposite direction is satisfied** on the same score, asserted directly.
+
+> **Pin 6a required isolation and then prescribed a test shape that cannot check it.**
+> The model test was cited for its *dispatch* property — that `all().len()` alone passes
+> with the arm deleted — which is real and still applies. **Borrowing a test's shape
+> imports its blind spots along with its virtue**, and m40 never needed exactness because
+> nothing about invariant 20 turned on it.
+
 **Pin 6 is coupled to pin 5 and they split only together.** M5 signs the undo
 hole by requiring invariant 21 to *observe* the residue. If invariant 21 is
 deferred to a later rung, then either pin 5 and M5 defer with it, or M5 must be
@@ -639,27 +693,46 @@ This rung edits **`core_spec.tex`** (row 5, invariant 21's enumeration) and
 **`operation_catalog.tex`** (row 4), and `crates/epiphany-testkit/tests/requirement_labels.rs`
 counts requirements and labels in **both**. The two readings have different touch tables:
 
-**Which counters move depends on WHICH document mints the label — corrected on review.**
+### DECIDED IN REVISION D: NEITHER document mints a label. Row 11 is UNUSED. No counter moves.
-An earlier draft of this pin said *"all three counters move if either document mints a
+
-label"*, which is false: `CORE_REQUIREMENT_COUNT` is asserted **only against
+**This pin twice said "decide and report", which is not a decision.** It left the staged
-`core_spec.tex`** (`requirement_labels.rs:259`), while the two suite counters sum every
+set and the counter expectations conditional on a choice execution would make
-scanned document.
+arbitrarily — and a conditional touch row is a row that can be wrong in either
+direction. **The facts settle it, and they were readable while the pin was being
+written:**
+
+- **Pin 6 adds invariant 21 to an enumeration that already sits inside ONE requirement
+  box.** `core_spec.tex:6529` opens `\begin{requirement}`, `:6530` carries the single
+  label **`req:graph:score-graph-invariants`**, `:6533` opens the `enumerate`, and the
+  box closes at **`:6648`** — with exactly **20 `\item`s** inside. Item 21 is an `\item`
+  **within** that box. **It mints no requirement and no label.**
+- **Pin 10 rewrites existing prose** in `operation_catalog.tex` §CreateStaff and
+  §CreateStaffGroup, plus a Revision History row and a version bump. **No new
+  requirement box, no new label.**
+
+**Therefore:** `CORE_REQUIREMENT_COUNT`, `SUITE_REQUIREMENT_COUNT` and
+`SUITE_LABEL_COUNT` all stay **unchanged**; **touch row 11 is unused and MUST NOT be
+staged**; and the report states that it was unused for this reason rather than
+re-deriving the question.
+
+**If execution finds this wrong** — if either edit turns out to require a new
+`\begin{requirement}` — **that is a finding and a contract defect**, reported under §6
+item 5, not a decision to be made at the keyboard. The counters would then move per the
+table below, which is retained for that case and for the next rung.
 
 | Label minted in | `CORE_REQUIREMENT_COUNT` | `SUITE_REQUIREMENT_COUNT` | `SUITE_LABEL_COUNT` |
 |---|---|---|---|
-| `core_spec.tex` (pin 6) | **moves** | **moves** | **moves** |
+| `core_spec.tex` | **moves** | **moves** | **moves** |
-| `operation_catalog.tex` (pin 10) | **unchanged** | **moves** | **moves** |
+| `operation_catalog.tex` | **unchanged** | **moves** | **moves** |
-| both | **moves by 1** | moves by 2 | moves by 2 |
+| both | moves by 1 | moves by 2 | moves by 2 |
-| neither | — | — | — |
+| **neither — THIS RUNG** | **—** | **—** | **—** |
-
-- **If any label is minted**, touch row 11 is used and the report names **which document,
-  which counters, and their new values.**
-- **If none is**, row 11 is unused and **the report says so.**
 
 > **S27's lesson was "name all three, not one" — for a rung that touched only
 > `core_spec.tex`.** Carrying that conclusion across to a rung touching two documents
-> turned a correction into a different error. **A fix imported from another contract
+> turned a correction into a different error, and then into a deferred decision. **A fix
-> must be re-derived against this one's facts**, not pattern-matched.
+> imported from another contract must be re-derived against this one's facts** — and
+> where the facts are readable, re-derived *now*, not delegated to execution as a
+> "decide and report".
 
 > **`CLAUDE.md` names this file by name as a recurring escapee**, it escaped the
 > format-epoch rung's table, and S27 had to add it mid-execution. **A file that must
@@ -778,7 +851,7 @@ unblocked, dispatchable and resolved are three different states.
 | **8** | `crates/epiphany-core/src/generators.rs` | **ADDED by draft amendment 1 — the root cause below.** `violating_score` (`:498`) matches `GraphInvariant` **exhaustively**, so invariant 21 **does not compile** without a new arm. Four `all()`-driven tests (`:991`, `:1004`, `:1025`, `:1042`) then consume it, so the arm must be a **real generator**, not a stub |
 | **9** | `crates/epiphany-testkit/src/roundtrip.rs` | **ADDED by draft amendment 1.** S27 test 10b (`:894`) reopens a literal-`0` base under `production_caps()`; pin 12's bump makes that path return `Err` and hit an arm that **`panic!`s by design** |
 | **10** | `crates/epiphany-textproj/src/serialize.rs` | **ADDED by draft amendment 1.** S27 test 10a (`:659`) asserts the production writer supplies `ReductionAlgorithmVersion(0)`. Its own doc (`:655`) says it **is expected to fail when S16 bumps** and that updating it *is* S16 stating the authority moved |
-| **11** | `crates/epiphany-testkit/tests/requirement_labels.rs` | **ADDED by draft amendment 1 — CONDITIONAL**, exactly as S27's row 12. Only if pin 6 or pin 10 mints a `\label{req:...}`. **That decision MUST be made explicitly and stated in the report** — see pin 10a. **Which counters move depends on WHICH document mints it — pin 10a owns that table and this row deliberately does not restate it.** *(This row read "all three counters move" until revision A; pin 10a was corrected and this copy was left standing in the same edit — the fix-one-site defect, committed while fixing the other site.)* This file counts **both** `core_spec.tex` and `operation_catalog.tex`, and this rung touches both, which is exactly why "all three" is wrong here. If no label is minted, leave unmodified and say so |
+| **11** | `crates/epiphany-testkit/tests/requirement_labels.rs` | **UNUSED — DECIDED in revision D, no longer conditional.** Pin 10a establishes that **neither** pin 6 nor pin 10 mints a `\label{req:...}`: invariant 21 becomes an `\item` inside the existing `req:graph:score-graph-invariants` box (`core_spec.tex:6529`–`:6648`), and pin 10 rewrites prose. **No counter moves; this file MUST NOT be staged**, and the report says so citing pin 10a. **The row is retained rather than deleted** because `CLAUDE.md` names this file as a recurring escapee — a row reading *"deliberately unused, and why"* survives review, while an absent row looks like an oversight. *(Read as "CONDITIONAL — decide and report" until revision D, and as "all three counters move" until revision A.)* |
 
 Regenerate the two PDFs **only after** their sources reach final form.
 
@@ -807,6 +880,14 @@ mechanism can detect a semantics change. They must be **updated, not deleted or
   that violates the **S→G direction — a staff whose `group` names a group whose
   `members` omit it — and NOT the G→S direction**, and survives shrinking.
   **The direction is PINNED here, in revision C.**
+- **The direction needs its own permanent assertion — REVISION D.** **No existing
+  `all()`-driven test can observe it.** `negative_generators_are_reasonably_targeted`
+  (`:1037`) collects `kinds: BTreeSet<GraphInvariant>` and allows `kinds.len() <= 3`, but
+  **both directions of invariant 21 are the same `GraphInvariant` variant**, so they
+  collapse to one element and the bound is blind to the distinction; the other three
+  loops assert only `!is_empty()`. Add a dedicated test in `generators.rs`'s test module
+  asserting `violating_score(StaffGroupMembershipAgreement, seed)` violates **S→G and
+  not G→S**, with the witness ids quoted in the report.
 
   > **"Both directions" was wrong here and incompatible with M6 — corrected in revision
   > B.** `violating_score` returns **one** `Score` per variant, so it cannot carry two
@@ -992,6 +1073,11 @@ weakening is invisible.
    both verdicts reported, and each confirmed to satisfy the direction it does not
    break.** *(Revision C: this asked for one score, which left one branch with no durable
    coverage once M6 was reverted.)*
+   **Report the EXACT violation set each fixture produces — revision D.** Quote
+   `check_invariants`' full return for both, showing **one** violation each and its
+   witness ids. *(This gate asked for the target verdict and the opposite direction's
+   absence, but **not the absence of invariants 1–20**, so a fixture carrying an
+   unrelated second defect passed every stated check.)*
    `all().len() == 21` and the `core_spec.tex` enumeration ending at 21 are checked
    **in addition**, never instead.
 7. **Every test named in pin 8** runs, each verdict reported. *(Read "the four pin-8
@@ -1107,14 +1193,14 @@ its evidence at `invariants.rs:69`–`:71` must stay intact.
 2b. **Pin 12's bump and its `Bumps` entry**, with gate 10's two outputs; **and rows 9
    and 10's tripwire updates**, each quoted before and after, with gate 11's confirmation
    that neither was silenced. **ADDED BY DRAFT AMENDMENT 1.**
-2c. **Whether pin 6 or pin 10 minted a `\label{req:...}`**, and therefore whether touch
+2c. **Confirmation that neither pin 6 nor pin 10 minted a `\label{req:...}`** — as pin
-   row 11 was used. **If used: WHICH document minted it, and which counters moved with
+   10a decided in revision D — that **touch row 11 was not staged**, and that all three
-   their new values — per pin 10a's table, which this item does not restate.** If not,
+   counters are **unchanged**. **If either edit did mint one, that is a FINDING against
-   say so explicitly.
+   this contract** (§6 item 5), reported with pin 10a's table applied; it is not a
-   *(This item said "all three counters and their new values" — the rule pin 10a had
+   decision to be taken during execution.
-   just corrected, surviving in its own report consumer. **Third site of one false
+   *(This item read "decide and report" and, before that, "all three counters and their
-   claim**: pin 10a, touch row 11, and here. A correction reaches the statement, then
+   new values" — the rule pin 10a had just corrected, surviving in its own report
-   the table, then the thing that reads the table — and stops one short each time.)*
+   consumer. **Third site of one false claim**: the pin, touch row 11, and here.)*
 2d. **Invariant 21's negative fixture survives `shrink`** — quote the shrunk witness and
    confirm it still violates 21. **REWRITTEN on review:** this item asked whether
    `shrink` matches `GraphInvariant` exhaustively, which is a **static fact the draft