S16: ratification round 4 -- "the resulting value" is not a value when there are two reductions

Whole-artifact review of 3e0a4d3 returned one blocking finding in round 3's own
harness.

Pin 7a collapsed two fixtures into one binding. t8b runs TWO authoring orders
(§0.5) -- two reductions over two different groups -- but pin 7a bound "the
resulting StaffGroup.members" and one filtered invariant result. A single
members local satisfies the harness as written while leaving either mutation's
required observation absent, depending on which order it came from; and the
invariant result filtered from the wrong reduction is the wrong verdict, not a
missing one.

Pin 7a now binds four, before any assertion:

  1. spurious-order OperationEffect  (M1: becomes an applied effect)
  2. spurious-order members          (M1: the spurious membership in the graph)
  3. missing-order members           (M2: stays empty)
  4. missing-order invariant-21 violations (M2: the disagreement left behind)

Every assertion formats all four, so whichever assertion a mutation trips
carries both of that mutation's observations. Gate 14 must now establish WHICH
ORDER each binding came from rather than counting bindings. M1 and M2 name
their own order at every mention.

Round 3 fixed the channel and left the fixtures conflated. It correctly
established that a failing test has one output channel and that state must be
bound before the assertion a mutation trips, then described the state as though
t8b had one reduction. The ordering rule was right and the inventory was wrong,
which is why the harness looked complete: three plausible bindings, none wrong
on its face, and nothing in the pin revealing that two of them are per-order.

The generalisable form: a definite article asserts uniqueness exactly as
silently as a number asserts a total. "The resulting value" reads as precise
and hides the question of which one -- the singular-noun cousin of the count
defects this contract has been removing since revision A.

And gate 14 inherited gate 12's defect before gate 12's fix could reach it.
Gate 12 was rewritten in revision H because a four-line aggregate proved a
population and not a pairing; gate 14 was written in round 3 requiring "three
bindings" -- the same shape, one section over, three rounds later. Ratification
round 1 recorded a fix failing to reach a declared peer; this is a fix failing
to reach a gate written after it.

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

@@ -368,6 +368,31 @@ observation is a single value under `assert_eq!`, the default diagnostic carries
 `assert!(matches!(…))`, which prints nothing, and the report must say which form each
 uses. Where it is composite or behind an unreachable assertion, a harness is required.
 
+### RATIFICATION ROUND 4 — independent, whole-artifact, against `3e0a4d3`. One blocking finding.
+
+| # | Finding | Disposition |
+|---|---|---|
+| **1** | **Pin 7a collapsed two fixtures into one binding.** `t8b` runs **two authoring orders** (§0.5) — two reductions over two different groups — but pin 7a bound *"the resulting `StaffGroup.members`"* and one filtered invariant result. **A single `members` local satisfies the harness while leaving either mutation's observation absent**, depending on which order it was taken from; the invariant result filtered from the wrong reduction is the *wrong verdict*, not a missing one | Pin 7a now binds **four**: spurious-order effect, spurious-order members, missing-order members, missing-order invariant-21 violations — **every** assertion formatting all four. **Gate 14** must establish **which order each binding came from**, not count bindings. **M1 and M2 name their own order** at every mention |
+
+**Round 3 fixed the channel and left the fixtures conflated.** It correctly established
+that a failing test has one output channel and that state must be bound before the
+assertion a mutation trips — then described the state as though `t8b` had one reduction.
+**The ordering rule was right and the inventory was wrong**, which is why the harness
+looked complete: three plausible bindings, none of them wrong on its face, and no way to
+tell from the pin that two of them are per-order.
+
+**"The resulting value" is not a value when there are two reductions.** That is the
+generalisable form, and it is the singular-noun cousin of the count defects: *a
+definite article asserts uniqueness exactly as silently as a number asserts a total.*
+Both read as precise and both hide the question of which one.
+
+**And gate 14 inherited gate 12's defect before gate 12's fix could reach it.** Gate 12
+was rewritten in revision H because a four-line aggregate proved a population and not a
+pairing; gate 14 was written in round 3 requiring *"three bindings"* — **the same shape,
+one section over, three rounds later.** It now requires the mapping. *(A fix reaching a
+peer is what ratification round 1 recorded; this is a fix failing to reach a gate written
+after it.)*
+
 **The pattern across revisions A–J 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
@@ -945,21 +970,33 @@ emits nothing but its assertion diagnostics**, so unless the state is in those
 diagnostics it is unobtainable, and revision E already ruled out adding print
 instrumentation for a report.
 
-So `t8b` MUST:
+**`t8b` exercises TWO authoring orders (§0.5), which are two reductions over two
+different groups — so there are FOUR observations, not three. CORRECTED IN RATIFICATION
+ROUND 4.** Bind all four to locals **before any assertion**:
 
-1. **Bind all three observations to locals BEFORE the first assertion** — the
+| # | Binding | The mutation that needs it |
-   `OperationEffect` for the spurious-order `CreateStaffGroup`, the resulting
+|---|---|---|
-   `StaffGroup.members`, and `check_invariants` filtered to
+| 1 | **spurious-order `OperationEffect`** — `ContainerNotEmpty` when pin 1 holds | **M1**: becomes an applied effect |
-   `StaffGroupMembershipAgreement`;
+| 2 | **spurious-order `StaffGroup.members`** | **M1**: carries the spurious membership that reached the graph |
-2. **format all three into EVERY assertion's failure message**, not just the assertion
+| 3 | **missing-order `StaffGroup.members`** — `[s]` when pin 2 holds | **M2**: stays empty |
-   they most obviously belong to.
+| 4 | **missing-order `check_invariants`, filtered to `StaffGroupMembershipAgreement`** | **M2**: the disagreement the empty projection leaves |
 
-> **Requirement 2 is the load-bearing half, and ordering is why.** A failing test stops
+**Then format ALL FOUR into EVERY assertion's failure message.**
-> at its **first** failed assertion, so state carried only in a later assertion's message
+
-> is never printed. Under M1 the spurious-order assertion fires; under M2 the
+> **Bindings 2 and 3 are different groups in different reductions, and an earlier draft
-> missing-order one does — **different assertions, and each must carry the whole state**,
+> of this pin collapsed them into one "resulting `StaffGroup.members`".** A single
-> or the mutation that trips the other one observes nothing. **Putting each value in
+> `members` local satisfies the harness as written **while leaving either mutation's
-> "its own" assertion is exactly the arrangement that fails.**
+> required observation absent** — whichever order it was taken from. The invariant result
+> has the same problem: filtered from the wrong reduction it is the wrong verdict, not a
+> missing one. **A harness for two fixtures needs two sets of bindings; "the resulting
+> value" is not a value when there are two reductions.**
+>
+> **The ordering rule is unchanged and still load-bearing.** A failing test stops at its
+> **first** failed assertion, so state carried only in a later assertion's message is
+> never printed. **Under M1 the spurious-order assertion fires; under M2 the
+> missing-order one does** — different assertions, so each must carry the **whole** set.
+> **Putting each value in "its own" assertion is exactly the arrangement that fails**,
+> and splitting the set per order would reintroduce it one level down.
 
 **Pin 8 — the four G3a undo-repair tests are re-verified, not assumed. NAMED by draft
 amendment 1.** All four are in `crates/epiphany-ops/src/reduce.rs`:
@@ -1338,18 +1375,22 @@ Applied, **run**, output recorded verbatim, restored **by hand-editing back**.
 **M1 — the refusal fires. OBSERVATION TIGHTENED, draft amendment 1; CHANNEL PINNED IN
 RATIFICATION ROUND 3.** Remove pin 1's emptiness check. **Required observation:** a
 `CreateStaffGroup` carrying a **non-empty `members`** is now **applied instead of
-refused** — the resulting `OperationEffect` and the minted `StaffGroup.members`, showing
+refused** — the **spurious-order** `OperationEffect` and the **spurious-order**
-the spurious membership that reached the graph. **Obtain them by quoting `t8b`'s
+`StaffGroup.members`, showing the spurious membership that reached the graph. **Obtain
-spurious-order assertion failure verbatim**, which pin 7a's harness requires to carry
+them by quoting `t8b`'s spurious-order assertion failure verbatim**, which pin 7a's
-all three observations. The assertion failing is the *symptom*; the applied mint is the
+harness requires to carry **all four** of its bindings — so this mutation's two are
-observation.
+present whichever assertion fires. *(Read "all three observations" until round 4, when
+pin 7a's collapsed `members` binding was split per authoring order.)* The assertion
+failing is the *symptom*; the applied mint is the observation.
 
 **M2 — the maintenance fires. OBSERVATION TIGHTENED, draft amendment 1; CHANNEL PINNED
 IN RATIFICATION ROUND 3.** Remove pin 2's append. **Required observation:** after a
-`CreateStaff` naming a live group, `StaffGroup.members` is **still empty**, and invariant
+`CreateStaff` naming a live group, the **missing-order** `StaffGroup.members` is **still
-21's verdict on that state. **Obtain both by quoting `t8b`'s missing-order assertion
+empty**, and the **missing-order** invariant-21 verdict on that state. **Obtain both by
-failure verbatim** — the same harness, a different assertion, which is why pin 7a
+quoting `t8b`'s missing-order assertion failure verbatim** — the same harness, a
-requires every assertion to carry the whole state.
+different assertion and **a different reduction from M1's**, which is why pin 7a binds
+`members` and the invariant result **per authoring order** and requires every assertion
+to carry all four.
 
 **M3 — the re-carry stays idempotent.** Make pin 3 write maintained members into
 `staff_group_values`; a byte-identical re-carry must degrade from
@@ -1651,11 +1692,22 @@ weakening is invisible.
     formatted in. **M5 can only report what these messages print**, so a harness this
     gate does not check is a mutation that observes nothing.
 
-14. **Pin 7a's observation harness in `t8b` — ADDED IN RATIFICATION ROUND 3.** Quote from
+14. **Pin 7a's observation harness in `t8b` — ADDED IN RATIFICATION ROUND 3, CORRECTED IN
-    source: the three bindings above `t8b`'s first assertion, and **every** assertion's
+    ROUND 4.** Quote from source, above `t8b`'s first assertion, **all four** bindings —
-    failure message showing all three formatted in. **Both M1 and M2 draw their required
+    **spurious-order effect, spurious-order members, missing-order members, missing-order
-    observations from these messages, via different assertions** — so a message carrying
+    invariant-21 violations** — and **every** assertion's failure message showing **all
-    only "its own" value silently disarms whichever mutation trips the other one.
+    four** formatted in.
+
+    **Confirm bindings 2 and 3 come from the two different reductions**, not one value
+    reused: they are different groups, and a single `members` local satisfies a
+    four-line-shaped check while leaving one mutation's observation absent. **Name which
+    order each binding was taken from.**
+
+    > **Both M1 and M2 draw their observations from these messages, via different
+    > assertions** — so a message carrying only "its own" values silently disarms
+    > whichever mutation trips the other one. **This gate must establish a mapping from
+    > each binding to its order, not a count of bindings** — gate 12's lesson, one
+    > section over.
 
 ---