P13-S16 EXECUTED: StaffGroup.members becomes a maintained projection

Disposition A replaces genesis tranche G3a's disposition B. Staff.group was
already the sole authority, but members was stored exactly as carried and
neither maintained nor trusted, so both disagreeing states were permitted
outcomes. Neither is authorable any more.

  - CreateStaffGroup refuses a non-empty carried members (ContainerNotEmpty).
    This is an empty-container precondition on the carried value, NOT a
    referential one, so unlike the sibling mints it is not graph-gated and
    holds base-free too. t7's assertion inverts for exactly that reason.
  - CreateStaff carrying group: Some(g) appends the staff to g's members in
    the graph, idempotently; undo of a staff strips it back out.
  - Graph invariant 21, StaffGroupMembershipAgreement, flags disagreement in
    either direction between live objects via two independently removable
    checks. It abstains on dangling membership -- an undeclared member is
    invariant 10's concern, not a disagreement.
  - staff_group_values keeps the carried value, and seed_from_graph reseeds it
    with members emptied, closing the reload hazard that only appears after a
    snapshot round trip.
  - CURRENT_REDUCTION_ALGORITHM_VERSION 0 -> 1 with its Bumps entry, naming
    both causes separately: CreateStaffGroup changes a reduction verdict,
    CreateStaff changes canonical reduced state. Either alone requires it.
    Bases materialized before this rung must be rebuilt, not reused.

Specification: operation_catalog.tex 0.15.0 and core_spec.tex's Revision
History; nine disposition-B prose sites rewritten, invariant 21 appended to the
Chapter 5 enumeration (count 20 -> 21), both PDFs rebuilt. No payload bytes
move, no schema or epoch moves, no vector artifact changes.

Evidence: 20 pins, 14 gates, 11 mutation executions. Baseline 1577 -> 1583
(six net-new tests). Both S27 tripwires fired on the bump and were updated to
independent literals, never to the constant.

Six findings reported against the contract rather than patched into it:
invariant 21's abstention vs the undo-hole attribution in 0.6/pin 5a/pin 6b;
M6a's failure set is seven, not six; t8d under M2 is falsified as a survivor;
pin 10 cites four of nine prose sites; cargo test --workspace truncates the
failure set without --no-fail-fast; pin 8's line numbers had drifted.

CLAUDE.md and spec/HANDOFF_2026-08-07.md are deliberately NOT in this commit
(contract 4a) and still describe the pre-bump state; their reconciliation is
post-acceptance work.

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

crates/epiphany-core/src/generators.rs

@@ -500,6 +500,27 @@ pub fn violating_score(inv: GraphInvariant, seed: u64) -> Score {
     let mut s = valid_score(seed);
     let replica = s.identity.replica_id;
     match inv {
+        StaffGroupMembershipAgreement => {
+            // P13-S16 touch row 8. Direction is PINNED to S->G: mint a group with
+            // an EMPTY `members` and point staff 0 at it. The staff names the
+            // group and the group omits the staff — the exact shape a pin-2
+            // maintenance gap produces, and the smallest corruption of
+            // `valid_score` (one field set, one empty group added).
+            //
+            // This must NOT violate G->S: `members` is empty, so that direction
+            // has nothing to disagree about. Both directions are the same
+            // `GraphInvariant`, so no `all()`-driven test can tell them apart —
+            // `invariant_21_negative_generator_breaks_staff_to_group_only` is the
+            // only guard on the direction, and it checks the shrunk fixture too.
+            let group_id = crate::ids::StaffGroupId::new(replica, 21_000);
+            s.staff_groups.push(crate::graph::StaffGroup {
+                id: group_id,
+                name: None,
+                kind: crate::graph::StaffGroupKind::Bracket,
+                members: Vec::new(),
+            });
+            s.staves[0].group = Some(group_id);
+        }
         EventVoiceBacklink => {
             // Arena event whose voice no longer lists it: drop it from the list.
             let (e0, _) = first_two_event_ids(&s);
@@ -999,6 +1020,114 @@ mod tests {
         }
     }
 
+    /// **P13-S16 touch row 8.** `violating_score`'s invariant-21 arm breaks the
+    /// **S→G** direction ONLY — in the raw fixture **and after shrinking**.
+    ///
+    /// Invariant 21's two directions carry the same `GraphInvariant`, so every
+    /// `all()`-driven test in this module is satisfied by either one and **none
+    /// can observe which**. This is the only guard on the generator's direction,
+    /// and `m41b` is the only permanent guard on the other direction being
+    /// dispatched at all.
+    ///
+    /// **The shrunk leg is not redundant.** `shrink` rebuilds the witness, and
+    /// nothing in its contract preserves *which way* the pair disagrees: a shrink
+    /// that cleared the staff's `group` while leaving it listed in `members`
+    /// would flip the direction, still violate invariant 21, and satisfy
+    /// `every_invariant_shrinks_to_a_small_witness` and `shrink_is_idempotent`
+    /// alike.
+    ///
+    /// **Mutation (M6a):** delete the `check_staff_names_absent_group` call from
+    /// `check_invariants`; both legs report nothing and the cardinality
+    /// assertions print `0` against `1`. Under **M6b** — deleting the G→S arm —
+    /// this test must **pass**, and that asymmetry is the direction claim.
+    #[test]
+    fn invariant_21_negative_generator_breaks_staff_to_group_only() {
+        let inv = GraphInvariant::StaffGroupMembershipAgreement;
+
+        // The two legs are built and checked SEQUENTIALLY, and the raw leg is
+        // fully validated before `shrink` is ever called.
+        //
+        // Building both in one array would evaluate `shrink` first — Rust
+        // constructs every element before the loop body runs — and `shrink`
+        // opens with `assert!(!check_invariant(score, inv).is_empty())`. Under
+        // M6a that check returns empty, so shrink PANICS on its own entry
+        // assertion before the raw leg's cardinality assertion executes, and M6a
+        // would report "shrink starting point must violate the target invariant"
+        // instead of the pinned `0` against `1`. **A panic upstream of the
+        // pinned assertion destroys the evidence the mutation owes.**
+        let raw = violating_score(inv, 0x2121_2121);
+        assert_breaks_staff_to_group_only("raw", &raw, inv);
+
+        let shrunk = shrink(&raw, inv);
+        assert_breaks_staff_to_group_only("shrunk", &shrunk, inv);
+    }
+
+    /// Pin 6a's three properties for one leg of
+    /// `invariant_21_negative_generator_breaks_staff_to_group_only`: exact
+    /// cardinality, the S→G witness naming both ids, and the G→S direction
+    /// holding — each asserted rather than implied.
+    fn assert_breaks_staff_to_group_only(leg: &str, s: &Score, inv: GraphInvariant) {
+        // Bound before any assertion, and read from the score so both legs
+        // survive shrinking rather than hardcoding the generator's counter. The
+        // ids are formatted here so this helper needs no extra id imports; the
+        // named group's `members` is carried as a value because the G->S claim
+        // must be checked against the FIXTURE, not against the checker's output.
+        let named = s.staves.iter().find_map(|staff| {
+            staff.group.map(|group| {
+                let members = s
+                    .staff_groups
+                    .iter()
+                    .find(|candidate| candidate.id == group)
+                    .map(|candidate| candidate.members.clone());
+                (format!("{:?}", staff.id), format!("{group:?}"), members)
+            })
+        });
+        let violations = check_invariants(s);
+
+        // First, because it is the assertion M6a trips.
+        assert_eq!(
+            violations.len(),
+            1,
+            "{leg}: expected exactly the invariant-21 S->G violation and nothing \
+             else, got {violations:?}"
+        );
+        assert_eq!(
+            violations[0].invariant, inv,
+            "{leg}: the single violation must be invariant 21, got {violations:?}"
+        );
+        assert!(
+            violations[0].witness.starts_with("S->G:"),
+            "{leg}: the generator must break the S->G direction only — a flipped \
+             direction still violates invariant 21 and no other test would \
+             notice; got {violations:?}"
+        );
+        let (staff_id, group_id, group_members) = named.unwrap_or_else(|| {
+            panic!("{leg}: the fixture must have a staff naming a group; got {violations:?}")
+        });
+        assert!(
+            violations[0].witness.contains(&staff_id) && violations[0].witness.contains(&group_id),
+            "{leg}: the witness must name both {staff_id} and {group_id}, got \
+             {violations:?}"
+        );
+        // The opposite direction holds, asserted against the FIXTURE. Checking
+        // only that no `G->S:` witness was emitted would pass **vacuously under
+        // M6b**: with the G->S arm deleted no such witness can appear whatever the
+        // fixture holds, so a flipped or both-directions fixture would slip
+        // through the leg that is supposed to guarantee the direction. The empty
+        // `members` is the checker-independent fact, and `m41` asserts it the
+        // same way.
+        assert_eq!(
+            group_members.as_deref(),
+            Some(&[][..]),
+            "{leg}: fixture — group {group_id} must list nobody, so nothing can \
+             disagree G->S; got {group_members:?}"
+        );
+        assert!(
+            !violations.iter().any(|v| v.witness.starts_with("G->S:")),
+            "{leg}: the G->S direction must hold, got {violations:?}"
+        );
+    }
+
     #[test]
     fn every_invariant_shrinks_to_a_small_witness() {
         for inv in GraphInvariant::all() {

crates/epiphany-core/src/graph.rs

@@ -840,11 +840,20 @@ pub struct Staff {
     pub instrument: InstrumentId,
     pub default_staff_lines: StaffLineConfiguration,
     /// Which staff group (if any) this staff belongs to. **The sole authority
-    /// for group membership** (genesis tranche G3a,
+    /// for group membership** (`spec/CONTRACT_P13S16_PROJECTION.md`, §1.1
-    /// `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, filed as
+    /// disposition A): writing this field is the only way membership changes.
-    /// P13-S16): every consumer MUST read membership from this field, not
+    ///
-    /// from [`StaffGroup::members`], which is a non-authoritative denormalized
+    /// [`StaffGroup::members`] is a projection **maintained from** this field
-    /// projection that may disagree with this field in either direction.
+    /// under reduction, never an independent input. The two **must agree** in
+    /// both directions, and graph invariant 21
+    /// (`StaffGroupMembershipAgreement`) flags any disagreement between live
+    /// objects.
+    ///
+    /// **P13-S16 replaced genesis tranche G3a's disposition B**
+    /// (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1), under which `members`
+    /// was stored exactly as carried and permitted to disagree with this field
+    /// in either direction. `CreateStaffGroup` now refuses a non-empty carried
+    /// `members` outright, so neither disagreeing state is authorable.
     pub group: Option<StaffGroupId>,
     /// Default clef for new instances of this staff (schema major 2,
     /// appended last per the wire rule; migration default treble).
@@ -1640,13 +1649,23 @@ pub struct StaffGroup {
     pub id: StaffGroupId,
     pub name: Option<String>,
     pub kind: StaffGroupKind,
-    /// A **non-authoritative denormalized projection** of group membership
+    /// A denormalized projection of group membership, **maintained from**
-    /// (genesis tranche G3a, `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1,
+    /// [`Staff::group`] under reduction (`spec/CONTRACT_P13S16_PROJECTION.md`,
-    /// disposition B, filed as P13-S16). [`Staff::group`] is the sole
+    /// §1.1 disposition A). [`Staff::group`] is the **sole authority**; this
-    /// authority: this field MUST NOT be read to decide whether a staff is in
+    /// field is derived from it, and the two **must agree** in both directions.
-    /// a group, and MAY be stale in **both** directions — a member missing
+    ///
-    /// here while `Staff.group` names this group, or a staff listed here
+    /// `CreateStaffGroup` **refuses** a non-empty carried `members`
-    /// while its own `Staff.group` is `None` or names a different group.
+    /// (`ContainerNotEmpty`): the operation authors the group, not its
+    /// membership. Membership changes only by writing [`Staff::group`], which
+    /// reduction mirrors here. Graph invariant 21
+    /// (`StaffGroupMembershipAgreement`) flags a disagreement in either
+    /// direction between live objects.
+    ///
+    /// **P13-S16 replaced genesis tranche G3a's disposition B**
+    /// (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1), under which this field
+    /// was authored directly, was not to be trusted, and could disagree with
+    /// [`Staff::group`] either way. Both of those states are now unreachable
+    /// through the ordinary API.
     pub members: Vec<StaffId>,
 }
 
@@ -2125,59 +2144,107 @@ mod g3a_tests {
             .expect("this file contains at least one #[cfg(test)] module")
     }
 
-    /// (t14) `Staff.group`'s doc comment states it is authoritative for
+    /// The doc block directly above `field_decl`, located **from the
-    /// group membership. Grep-assert, **sliced to that field's doc block
+    /// declaration** and extended backwards over the contiguous `///` lines.
-    /// only** — `graph.rs` mentions `group` throughout, so a file-wide
-    /// search cannot fail.
     ///
-    /// **Mutation:** delete the doc comment (revert to no doc comment on
+    /// **Neither end of this slice depends on the doc text** (P13-S16 pin 10,
-    /// this field, its pre-G3a state); must fail.
+    /// ratification round 9). Both `t14` guards previously anchored the *start*
+    /// on a phrase from the comment, and for `StaffGroup.members` that phrase was
+    /// the disposition-B claim pin 10 rewrites. Once rewritten, `.find()`
+    /// returned `None` and the `.expect` panicked on absent text — **naming no
+    /// needle and dumping no block**, so the mutation's required observation
+    /// became an anchor failure instead of a needle miss.
+    ///
+    /// A guard whose *locator* depends on the text it inspects fails before it
+    /// can report, and **failing early looks like failing correctly.** Anchored
+    /// on the declaration, the block exists under either disposition and the only
+    /// way to fail is the needle assertion, with its message and block intact.
+    fn doc_block_above<'a>(source: &'a str, field_decl: &str) -> &'a str {
+        let decl = source
+            .find(field_decl)
+            .unwrap_or_else(|| panic!("the field declaration `{field_decl}` is present"));
+        // Start of the declaration's own line, then walk back over `///` lines.
+        let mut start = source[..decl].rfind('\n').map_or(0, |i| i + 1);
+        while let Some(prev_end) = start.checked_sub(1) {
+            let prev_start = source[..prev_end].rfind('\n').map_or(0, |i| i + 1);
+            if source[prev_start..prev_end].trim_start().starts_with("///") {
+                start = prev_start;
+            } else {
+                break;
+            }
+        }
+        &source[start..decl]
+    }
+
+    /// (t14) `Staff.group`'s doc comment states it is the sole authority and that
+    /// the projection is **maintained from** it and **must agree**. Grep-assert,
+    /// **sliced to that field's doc block only** — `graph.rs` mentions `group`
+    /// throughout, so a file-wide search cannot fail.
+    ///
+    /// **The needles must be wording disposition B cannot satisfy.** "sole
+    /// authority" alone is insufficient: it was true under B as well, so a guard
+    /// built from it passes against the very text it is meant to have replaced.
+    /// "maintained from" and "must agree" are false under B, which is what makes
+    /// this guard able to fail.
+    ///
+    /// **Mutation (M7a):** revert this doc block to its disposition-B wording;
+    /// must fail here while the `StaffGroup.members` guard below still passes.
     #[test]
     fn t14_staff_group_field_doc_comment_states_sole_authority() {
-        let source = production_source();
+        let doc_block = doc_block_above(production_source(), "pub group: Option<StaffGroupId>,");
-        let start = source
-            .find("    /// Which staff group (if any) this staff belongs to.")
-            .expect("Staff.group's doc comment is present");
-        let end = source[start..]
-            .find("pub group: Option<StaffGroupId>,")
-            .map(|offset| start + offset)
-            .expect("the `group` field declaration follows its doc comment");
-        let doc_block = &source[start..end];
         assert!(
             doc_block.contains("sole authority"),
             "Staff.group's doc comment must state it is the sole authority; block was:\n{doc_block}"
         );
+        assert!(
+            doc_block.contains("maintained from"),
+            "Staff.group's doc comment must state the projection is maintained from it \
+             (P13-S16 disposition A); block was:\n{doc_block}"
+        );
+        assert!(
+            doc_block.contains("must agree"),
+            "Staff.group's doc comment must state the two must agree — a needle \
+             disposition B cannot satisfy; block was:\n{doc_block}"
+        );
     }
 
-    /// (t14) `StaffGroup.members`'s doc comment states it is a
+    /// (t14) `StaffGroup.members`'s doc comment states it is **maintained from**
-    /// non-authoritative projection that may be stale in **both**
+    /// [`Staff::group`], that the two **must agree**, and that a non-empty
-    /// directions. Grep-assert, **sliced to that field's doc block only** —
+    /// carried value is refused. Sliced to that field's doc block only — same
-    /// same discipline as the `Staff.group` guard above.
+    /// discipline as the `Staff.group` guard above.
     ///
-    /// **Mutation:** delete the doc comment (revert to no doc comment on
+    /// **The name is retained deliberately.** P13-S16's §3 and §6 name this test
-    /// this field, its pre-G3a state); must fail.
+    /// exactly for M7a/M7b evidence, so renaming it would break the contract's
+    /// own citations. It also stays accurate: under disposition A `members` is a
+    /// **non-authoritative projection** — `Staff.group` is still the sole
+    /// authority — and what changed is that the projection is now *maintained*
+    /// rather than merely stored. The assertions below test maintenance; the name
+    /// records what the field is.
+    ///
+    /// **Mutation (M7b):** revert this doc block to its disposition-B wording;
+    /// must fail here while the `Staff.group` guard above still passes.
     #[test]
     fn t14_staff_group_members_field_doc_comment_states_non_authoritative_projection() {
-        let source = production_source();
+        let doc_block = doc_block_above(production_source(), "pub members: Vec<StaffId>,");
-        let start = source
-            .find("    /// A **non-authoritative denormalized projection** of group")
-            .expect("StaffGroup.members's doc comment is present");
-        let end = source[start..]
-            .find("pub members: Vec<StaffId>,")
-            .map(|offset| start + offset)
-            .expect("the `members` field declaration follows its doc comment");
-        let doc_block = &source[start..end];
         assert!(
-            doc_block.contains("non-authoritative"),
+            doc_block.contains("maintained from"),
-            "StaffGroup.members's doc comment must state it is non-authoritative; block was:\n{doc_block}"
+            "StaffGroup.members's doc comment must state it is maintained from \
+             Staff.group; block was:\n{doc_block}"
         );
         assert!(
-            doc_block.contains("MUST NOT be read"),
+            doc_block.contains("must agree"),
-            "StaffGroup.members's doc comment must forbid reading it to decide membership; block was:\n{doc_block}"
+            "StaffGroup.members's doc comment must state the two must agree; block \
+             was:\n{doc_block}"
         );
         assert!(
-            doc_block.contains("both** directions"),
+            doc_block.contains("sole authority"),
-            "StaffGroup.members's doc comment must permit staleness in both directions; block was:\n{doc_block}"
+            "StaffGroup.members's doc comment must name Staff.group as the sole \
+             authority; block was:\n{doc_block}"
+        );
+        assert!(
+            doc_block.contains("refuses"),
+            "StaffGroup.members's doc comment must record that a non-empty carried \
+             members is refused; block was:\n{doc_block}"
         );
     }
 }

crates/epiphany-core/src/invariants.rs

@@ -7,14 +7,18 @@
 //! enumerated invariant has exactly one check returning a typed
 //! [`InvariantViolation`] witness identifying the smallest offending objects.
 //!
-//! **Count.** The QUICKSTART says "the 18 graph invariants enumerated in
+//! **Count.** [`GraphInvariant::all`] is the single origin: its length *is* the
-//! Chapter 5"; the spec body (pre-G3b) enumerates **19** items (1–19 in
+//! count, and no prose here restates it — a restated count goes stale silently
-//! §"Graph Invariants"). We implement all 19 of those and record the
+//! the next time the enumeration grows, which it has twice.
-//! discrepancy as a Pass 11 candidate in `DECISIONS.md` (the spec is the
+//!
-//! contract). Genesis tranche G3b
+//! The QUICKSTART's summary count disagrees with `core_spec.tex`'s own Chapter 5
-//! (`spec/CONTRACT_GENESIS_G3B_MEASURE.md`) adds a 20th, measure-meter
+//! enumeration; that discrepancy is recorded as a Pass 11 candidate in
-//! consistency, ahead of `core_spec.tex`'s own update (a later packet in the
+//! `DECISIONS.md` (the spec is the contract) and is not reconciled here. Beyond
-//! same tranche) — see [`GraphInvariant::MeasureMeterConsistency`].
+//! the spec body's original set, two rungs have appended: Genesis tranche G3b
+//! (`spec/CONTRACT_GENESIS_G3B_MEASURE.md`) added measure-meter consistency
+//! (see [`GraphInvariant::MeasureMeterConsistency`]), and P13-S16
+//! (`spec/CONTRACT_P13S16_PROJECTION.md`) added staff-group membership
+//! agreement (see [`GraphInvariant::StaffGroupMembershipAgreement`]).
 //!
 //! **Scope of structural decidability.** A few invariants depend on resolving
 //! [`crate::TimeAnchor`]s to absolute time (region time-overlap, anchor-offset
@@ -32,8 +36,8 @@ use crate::graph::{
     TieClass, TimeSignature, VoiceOrigin,
 };
 use crate::ids::{
-    EventId, MeasureId, PitchId, RegionId, ReplicaId, StaffId, StaffInstanceId, TimeSignatureId,
+    EventId, MeasureId, PitchId, RegionId, ReplicaId, StaffGroupId, StaffId, StaffInstanceId,
-    VoiceId,
+    TimeSignatureId, VoiceId,
 };
 use crate::pitch::{PitchSpaceId, SpellingDirective, SpellingScope};
 use crate::time::{
@@ -115,10 +119,24 @@ pub enum GraphInvariant {
     ///     `measure_duration()` and can be refused and flagged (P13-S19,
     ///     deferred).
     MeasureMeterConsistency,
+    /// 21. `Staff.group` and `StaffGroup.members` **agree in both directions**:
+    ///     every live staff naming a group appears in that group's `members`,
+    ///     and every staff a group lists names that group in its own `group`
+    ///     field. `Staff.group` is the sole authority; `members` is the
+    ///     projection maintained from it under reduction (P13-S16 pins 1, 2, 5).
+    ///
+    ///     Witnesses name **both ids and the direction**, because the two
+    ///     directions fail for different reasons and are checked by two
+    ///     separately dispatched methods (P13-S16 pin 6b) — a maintenance gap
+    ///     leaves a staff absent from `members`, while a stale projection lists
+    ///     a staff that no longer names the group.
+    StaffGroupMembershipAgreement,
 }
 
 impl GraphInvariant {
-    /// The spec enumeration number (1–19).
+    /// This invariant's position in `core_spec.tex` §"Graph Invariants",
+    /// numbered from 1. Deliberately count-free: the highest number is whatever
+    /// the last arm below returns, not a figure restated in prose.
     pub fn number(self) -> u8 {
         use GraphInvariant::*;
         match self {
@@ -142,11 +160,13 @@ impl GraphInvariant {
             VoiceOriginConsistent => 18,
             BarlineGroupSameRegion => 19,
             MeasureMeterConsistency => 20,
+            StaffGroupMembershipAgreement => 21,
         }
     }
 
-    /// All 20 invariants in enumeration order.
+    /// Every invariant, in enumeration order. The array's own length is the
-    pub fn all() -> [GraphInvariant; 20] {
+    /// authoritative count — see the module header's **Count** note.
+    pub fn all() -> [GraphInvariant; 21] {
         use GraphInvariant::*;
         [
             EventVoiceBacklink,
@@ -169,6 +189,7 @@ impl GraphInvariant {
             VoiceOriginConsistent,
             BarlineGroupSameRegion,
             MeasureMeterConsistency,
+            StaffGroupMembershipAgreement,
         ]
     }
 }
@@ -280,6 +301,12 @@ pub fn check_invariants(score: &Score) -> Vec<InvariantViolation> {
     idx.check_voice_origin_consistent(&mut v);
     idx.check_barline_group_same_region(&mut v);
     idx.check_measure_meter_consistency(&mut v);
+    // Invariant 21's two directions, dispatched separately (P13-S16 pin 6b).
+    // Each call site is independently deletable, which is what M6a and M6b
+    // delete; a single call handling both would leave the mutation with no way
+    // to fail one direction while the other still reports.
+    idx.check_staff_names_absent_group(&mut v);
+    idx.check_group_lists_unowned_staff(&mut v);
     v
 }
 
@@ -1481,11 +1508,11 @@ impl<'a> GraphIndex<'a> {
     // --- Accidental modification / pitch-space compatibility (Chapter 4
     // §"Accidental Registries", `req:tuning:accidental-modification-compatibility`,
     // `core_spec.tex:3120`; Push 4b tranche 3a,
-    // `spec/CONTRACT_PUSH4B_ACCIDENTALS.md`). Not one of the 19
+    // `spec/CONTRACT_PUSH4B_ACCIDENTALS.md`). Not one of the spec-enumerated
-    // spec-enumerated Chapter 5 graph invariants (this is a Chapter 4
+    // Chapter 5 graph invariants (this is a Chapter 4
     // requirement), so — like the tempo-map and aleatoric-model checks above
     // — it is surfaced under an existing `GraphInvariant` tag rather than
-    // inventing a 20th. `CrossCuttingRefsResolve` is the closest fit: like
+    // minting a new one. `CrossCuttingRefsResolve` is the closest fit: like
     // those checks, this is "does this cross-cutting structure's content
     // hold against the rest of the score", not a per-event/per-voice
     // structural rule.
@@ -2755,6 +2782,78 @@ impl<'a> GraphIndex<'a> {
             }
         }
     }
+
+    // --- Invariant 21, `StaffGroupMembershipAgreement` (P13-S16 pins 6, 6b).
+    // TWO separately dispatched methods, one per direction. The split is
+    // required, not stylistic: each direction must have an independently
+    // deletable call site so that deleting one leaves the other reporting
+    // (M6a/M6b). A single shared comparison would satisfy every behavioural
+    // assertion while making that observation impossible. Both emit the same
+    // `GraphInvariant`, so both directions collapse to one variant in any
+    // `kinds`-style set — which is why direction is asserted by name, never by
+    // counting. -----------------------------------------------------------
+    /// Direction **S→G**: every live staff naming a group appears in that
+    /// group's `members`. A maintenance gap — pin 2 failing to append — shows up
+    /// here.
+    ///
+    /// A staff naming a group that does not exist is **not** flagged here:
+    /// dangling reference resolution belongs to the referential invariants, and
+    /// abstaining keeps this invariant's witnesses about *agreement* only.
+    fn check_staff_names_absent_group(&self, out: &mut Vec<InvariantViolation>) {
+        let members: HashMap<StaffGroupId, BTreeSet<StaffId>> = self
+            .score
+            .staff_groups
+            .iter()
+            .map(|group| (group.id, group.members.iter().copied().collect()))
+            .collect();
+        for staff in &self.score.staves {
+            let Some(group_id) = staff.group else {
+                continue;
+            };
+            if let Some(ids) = members.get(&group_id) {
+                if !ids.contains(&staff.id) {
+                    out.push(InvariantViolation::new(
+                        GraphInvariant::StaffGroupMembershipAgreement,
+                        format!(
+                            "S->G: staff {:?} names group {:?}, but that group's members omit it",
+                            staff.id, group_id
+                        ),
+                    ));
+                }
+            }
+        }
+    }
+
+    /// Direction **G→S**: every staff a group lists names that group in its own
+    /// `group` field. A stale projection — a member left behind, or one pointing
+    /// at a different group — shows up here.
+    ///
+    /// A member id with no live staff is **not** flagged here, for the same
+    /// reason as the S→G direction.
+    fn check_group_lists_unowned_staff(&self, out: &mut Vec<InvariantViolation>) {
+        let owner: HashMap<StaffId, Option<StaffGroupId>> = self
+            .score
+            .staves
+            .iter()
+            .map(|staff| (staff.id, staff.group))
+            .collect();
+        for group in &self.score.staff_groups {
+            for member in &group.members {
+                let Some(named) = owner.get(member) else {
+                    continue;
+                };
+                if *named != Some(group.id) {
+                    out.push(InvariantViolation::new(
+                        GraphInvariant::StaffGroupMembershipAgreement,
+                        format!(
+                            "G->S: group {:?} lists staff {:?}, but that staff names {:?}",
+                            group.id, member, named
+                        ),
+                    ));
+                }
+            }
+        }
+    }
 }
 
 /// Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 6c): the
@@ -6044,7 +6143,7 @@ mod g3b_measure20_tests {
 
 /// Genesis tranche G3b packet 2: M40, asserted BEHAVIOURALLY against
 /// `check_invariants`' dispatch (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin
-/// 11) -- `all().len() == 20` passes even with the dispatch arm deleted, so
+/// 11) -- an `all().len()` count passes even with the dispatch arm deleted, so
 /// this row must instead show a score violating ONLY invariant 20 is
 /// actually flagged by the top-level `check_invariants` entry point.
 #[cfg(test)]
@@ -6058,10 +6157,10 @@ mod g3b_dispatch_tests {
     use crate::time::{AnchorOffset, MusicalDuration, RationalTime, RegionEdge};
 
     /// M40: deleting invariant 20's arm from `check_invariants`' dispatch
-    /// must be observed here -- `all().len() == 20` alone would not notice.
+    /// must be observed here -- an `all().len()` count alone would not notice.
     #[test]
     fn m40_check_invariants_dispatches_invariant_20() {
-        assert_eq!(GraphInvariant::all().len(), 20);
+        assert_eq!(GraphInvariant::all().len(), 21);
         let mut s = crate::generators::valid_score(4242);
         let replica = s.identity.replica_id;
         // Corrupt ONLY invariant 20: two measures, both `None` (so
@@ -6130,7 +6229,170 @@ mod g3b_dispatch_tests {
                 .any(|v| v.invariant == GraphInvariant::MeasureMeterConsistency),
             "check_invariants (the top-level dispatch) must surface the invariant-20 \
              violation -- this is the behavioural assertion M40 needs, since \
-             all().len() == 20 alone passes even with the dispatch arm deleted"
+             an all().len() count alone passes even with the dispatch arm deleted"
+        );
+    }
+}
+
+/// P13-S16 pins 6/6a/6b: invariant 21's **two directions**, each surfaced
+/// through `check_invariants`' dispatch and each isolated to its own direction.
+///
+/// Both directions carry the same `GraphInvariant`, so **no `all()`-driven test
+/// can tell them apart** — every such test is satisfied by either one. These two
+/// are the only permanent guarantee that both are dispatched, which is what pin
+/// 6b's two independently removable methods exist for.
+///
+/// **Each fixture violates its own direction ONLY**, asserted as an exact set.
+/// A fixture disagreeing both ways would be reported after either arm was
+/// deleted, so it would sign neither.
+#[cfg(test)]
+mod s16_agreement_dispatch_tests {
+    use super::*;
+    use crate::graph::{StaffGroup, StaffGroupKind};
+    use crate::ids::StaffGroupId;
+
+    /// (m41) **Breaks S→G**: a staff whose `group` names a group whose `members`
+    /// omit it — the shape a pin-2 maintenance gap produces.
+    ///
+    /// **Holds G→S**: `members` is empty, so that direction has nothing to
+    /// disagree about. **Holds every other invariant**, which is what the exact
+    /// cardinality assertion proves and what `any()` could never touch.
+    ///
+    /// **Mutation (M6a):** delete the `check_staff_names_absent_group` call from
+    /// `check_invariants`. This fixture then goes **unreported** — the assertion
+    /// prints `0` against `1` with an empty vector, which is the observation M6a
+    /// owes, quoted rather than inferred. `m41b` must still pass.
+    #[test]
+    fn m41_check_invariants_dispatches_invariant_21_staff_names_absent_group() {
+        let mut s = crate::generators::valid_score(4243);
+        let replica = s.identity.replica_id;
+        let group_id = StaffGroupId::new(replica, 21_001);
+        s.staff_groups.push(StaffGroup {
+            id: group_id,
+            name: None,
+            kind: StaffGroupKind::Bracket,
+            members: Vec::new(),
+        });
+        let staff_id = s.staves[0].id;
+        s.staves[0].group = Some(group_id);
+
+        // Bound before ANY assertion: the opposite-direction fact this fixture
+        // depends on, then the violations. Nothing is asserted until the
+        // cardinality check, which is the one M6a trips.
+        let group_members: Option<Vec<StaffId>> = s
+            .staff_groups
+            .iter()
+            .find(|group| group.id == group_id)
+            .map(|group| group.members.clone());
+        let violations = check_invariants(&s);
+
+        assert_eq!(
+            violations.len(),
+            1,
+            "expected exactly the invariant-21 S->G violation and nothing else, \
+             got {violations:?}"
+        );
+        assert_eq!(
+            violations[0].invariant,
+            GraphInvariant::StaffGroupMembershipAgreement,
+            "the single violation must be invariant 21, got {violations:?}"
+        );
+        assert!(
+            violations[0].witness.starts_with("S->G:"),
+            "the witness must name the S->G direction so this test cannot pass \
+             on m41b's fixture, got {violations:?}"
+        );
+        assert!(
+            violations[0].witness.contains(&format!("{staff_id:?}"))
+                && violations[0].witness.contains(&format!("{group_id:?}")),
+            "the witness must name both the staff and the group id, got \
+             {violations:?}"
+        );
+        // The G->S direction holds, asserted directly rather than left to follow
+        // from the cardinality above: the group must genuinely list nobody, and
+        // no G->S witness may be present.
+        assert_eq!(
+            group_members.as_deref(),
+            Some(&[][..]),
+            "fixture: the group must list nobody, so only S->G disagrees"
+        );
+        assert!(
+            !violations.iter().any(|v| v.witness.starts_with("G->S:")),
+            "the G->S direction must hold on this fixture, got {violations:?}"
+        );
+    }
+
+    /// (m41b) **Breaks G→S**: a group listing a staff whose own `group` is not
+    /// that group — the shape a stale projection produces.
+    ///
+    /// **Holds S→G**: the listed staff's `group` is `None`, so it names no group
+    /// and that direction abstains. **Holds every other invariant** — note the
+    /// listed staff is genuinely declared, so this is a *disagreement*, not a
+    /// dangling reference (invariant 21 abstains on those; invariant 10 owns
+    /// them).
+    ///
+    /// **Mutation (M6b):** delete the `check_group_lists_unowned_staff` call from
+    /// `check_invariants`. This fixture then goes unreported, printing `0`
+    /// against `1`. **`m41b` is the ONLY test M6b breaks** — `m41`, the generator
+    /// direction test and all four `all()` consumers use S→G fixtures, so
+    /// without this test the G→S arm could be deleted and the suite would stay
+    /// green.
+    #[test]
+    fn m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff() {
+        let mut s = crate::generators::valid_score(4244);
+        let replica = s.identity.replica_id;
+        let group_id = StaffGroupId::new(replica, 21_002);
+        let staff_id = s.staves[0].id;
+        s.staff_groups.push(StaffGroup {
+            id: group_id,
+            name: None,
+            kind: StaffGroupKind::Bracket,
+            members: vec![staff_id],
+        });
+
+        // Bound before ANY assertion: the opposite-direction fact (`valid_score`
+        // leaves every staff's `group` as `None`, which is what keeps S->G
+        // abstaining), then the violations. This was asserted *before* the
+        // binding in the first draft, which put a check ahead of the cardinality
+        // assertion M6b trips — if the precondition ever broke, M6b's evidence
+        // would be replaced by a fixture complaint.
+        let listed_staff_group = s.staves[0].group;
+        let violations = check_invariants(&s);
+
+        assert_eq!(
+            violations.len(),
+            1,
+            "expected exactly the invariant-21 G->S violation and nothing else, \
+             got {violations:?}"
+        );
+        assert_eq!(
+            violations[0].invariant,
+            GraphInvariant::StaffGroupMembershipAgreement,
+            "the single violation must be invariant 21, got {violations:?}"
+        );
+        assert!(
+            violations[0].witness.starts_with("G->S:"),
+            "the witness must name the G->S direction so this test cannot pass \
+             on m41's fixture, got {violations:?}"
+        );
+        assert!(
+            violations[0].witness.contains(&format!("{staff_id:?}"))
+                && violations[0].witness.contains(&format!("{group_id:?}")),
+            "the witness must name both the staff and the group id, got \
+             {violations:?}"
+        );
+        // The S->G direction holds, asserted directly: the listed staff must name
+        // no group at all, and no S->G witness may be present. Without the first
+        // of these the fixture could silently become a both-directions one, which
+        // would be reported after EITHER arm was deleted and so would sign
+        // neither.
+        assert_eq!(
+            listed_staff_group, None,
+            "fixture: the listed staff must name no group, so only G->S disagrees"
+        );
+        assert!(
+            !violations.iter().any(|v| v.witness.starts_with("S->G:")),
+            "the S->G direction must hold on this fixture, got {violations:?}"
         );
     }
 }

crates/epiphany-ops/src/lib.rs

@@ -126,22 +126,51 @@ pub mod vectors;
 /// regression look identical from outside. **The discipline is the guarantee;
 /// there is no backstop.**
 ///
-/// # Why `0`, and why that is a decision
+/// # Why the series *started* at `0`, and why that was a decision
 ///
-/// Bundles written to date carry `0` when they have no canonical base, and
+/// Bundles written before the authority check carry `0` when they have no
-/// bases self-report whatever they were stamped with. Starting anywhere but `0`
+/// canonical base, and bases self-report whatever they were stamped with.
-/// would make every existing base-bearing document fail to open **without any
+/// Starting the series anywhere but `0` would have made every existing
-/// semantics having changed** — the check would manufacture the breakage it
+/// base-bearing document fail to open **without any semantics having changed** —
-/// exists to detect. `0` is therefore a decision, **not "unset"**.
+/// the check would have manufactured the breakage it exists to detect. `0` was
+/// therefore a decision, **not "unset"**.
+///
+/// This is a fact about the *baseline*, not about the current value: read the
+/// declaration below for that, and the `Bumps` list for how the series got
+/// there.
 ///
 /// # Bumps
 ///
 /// * `0` — the baseline. The semantics `canonical_reduction_order` and
 ///   `reduce_onto` implement as of P13-S27 (2026-08-08). No earlier version
 ///   exists; nothing predates this constant.
+/// * `1` — **P13-S16** (2026-08-09, `spec/CONTRACT_P13S16_PROJECTION.md`), the
+///   first real bump. It carries **one change of each kind**, and the two are
+///   not interchangeable:
+///   - a **reduction verdict** change — `CreateStaffGroup` carrying a non-empty
+///     `members` now reduces to a `ContainerNotEmpty` no-op where version `0`
+///     applied it. The effect recorded for that operation differs.
+///   - a **canonical reduced state** change — `CreateStaff` carrying
+///     `group: Some(g)` now appends the staff to `g`'s `members`. Its verdict is
+///     unchanged (it still applies); the graph the reduction produces is what
+///     differs.
 ///
-/// The first real bump belongs to **P13-S16**, which changes
+///   Either alone would require this bump. A base materialized under `0` holds
-/// `CreateStaffGroup`'s reduction verdict and must move this to `1`.
+///   state this version would not have computed, so it must be rebuilt rather
+///   than reused.
+///
+/// A bump without its entry above leaves a number nobody can account for: this
+/// list is the only record of *why* each version exists.
+///
+/// **No mechanism detects a missed bump.** The authority check compares
+/// *declared* versions, so it catches a base stamped with a version other than
+/// this one — it cannot notice that the semantics changed while the constant
+/// stood still. Every future change to a canonical reduction verdict **or to
+/// canonical reduced state** must move this constant and add its entry here.
+/// Both classes are named because a change that leaves every verdict intact
+/// while altering the reduced graph is the easier one to overlook, and it
+/// invalidates a base just as completely. That discipline is the whole
+/// guarantee.
 ///
 /// # Layering
 ///
@@ -149,7 +178,7 @@ pub mod vectors;
 /// `epiphany-bundle` in order to use that crate's `ReductionAlgorithmVersion`
 /// wrapper. The wrapper is constructed at the composition boundary by whoever
 /// depends on both (P13-S27 pin 1, §0.3).
-pub const CURRENT_REDUCTION_ALGORITHM_VERSION: u32 = 0;
+pub const CURRENT_REDUCTION_ALGORITHM_VERSION: u32 = 1;
 
 pub use anomaly::{
     AnomalousReplicaSegment, IntegrityAnomaly, IntegrityAnomalyKind, ReplicaAnomalyReason,

crates/epiphany-ops/src/payload.rs

@@ -278,10 +278,13 @@ pub enum OperationKind {
     // --- Genesis tranche G3a (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md`): the
     // four remaining root-level `Score` entity mints. Discriminant extends
     // additively past 34. ---
-    /// Mint a staff group on the score root (set-union creation). Graph-aware
+    /// Mint a staff group on the score root (set-union creation). Reduction
-    /// reduction preconditions every carried member resolves to a live
+    /// **refuses a non-empty carried `members`** (`ContainerNotEmpty`): the
-    /// `Staff`; the mint stores `members` as given and neither maintains nor
+    /// operation authors the group, not its membership, which is maintained
-    /// trusts it thereafter (contract §1.1, disposition B).
+    /// from `Staff.group` (P13-S16 §1.1, disposition A). The refusal is an
+    /// empty-container precondition on the carried value, so it is **not**
+    /// graph-gated and holds base-free — unlike the sibling mints' liveness
+    /// checks below.
     CreateStaffGroup(CreateStaffGroupOp),
     /// Mint a part-extraction view definition on the score root (set-union
     /// creation). Graph-aware reduction preconditions every carried staff
@@ -1788,11 +1791,19 @@ impl CanonicalEncode for SetTuningContextOp {
 
 /// Mint a global [`StaffGroup`] on the score root (operation_catalog
 /// §CreateStaffGroup). Carries the full staff-group value: identity, optional
-/// name, kind, and the carried `members` list. Graph-aware reduction
+/// name, kind, and a `members` list that **must be empty**.
-/// preconditions every carried member resolves to a live `Staff`; per §1.1
+///
-/// (disposition B), the mint stores `members` exactly as given and neither
+/// Reduction refuses a non-empty carried `members` with `ContainerNotEmpty`
-/// maintains nor trusts it thereafter — `Staff.group` is the sole authority
+/// (P13-S16 §1.1, disposition A): this operation authors the group, not its
-/// for membership.
+/// membership. `Staff.group` is the sole authority for membership and
+/// `StaffGroup.members` is the projection maintained from it, so the only way
+/// to put a staff in a group is to write `Staff.group`.
+///
+/// The refusal is an **empty-container** precondition on the carried value, not
+/// a referential one, so it is not graph-gated and holds base-free too.
+/// **The payload bytes are unchanged** — `members` is still encoded, and a blob
+/// authored under disposition B still decodes; only what reduction will accept
+/// has narrowed.
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct CreateStaffGroupOp {
     pub group: StaffGroup,

crates/epiphany-ops/src/reduce.rs

@@ -1616,7 +1616,29 @@ impl<'a> Reducer<'a> {
             // retained value and misclassifies (the G1 `instrument_values`
             // hazard, `reduce.rs:13264`–`:13268`, copied here for all four
             // families).
-            self.staff_group_values.insert(group.id, group.clone());
+            //
+            // P13-S16 pin 4: seed the **carried** value, so `members` is
+            // emptied here rather than cloned from the graph. This map answers
+            // "what was authored?", and pin 1 refuses any non-empty carried
+            // `members` — so empty is the *only* authorable value and emptying
+            // is an exact reconstruction, not a lossy approximation. The
+            // graph's `members` is derived, maintained from `Staff.group` by
+            // pin 2, and must never reach `create_staff_group`'s re-carry
+            // comparator.
+            //
+            // DO NOT "fix" this back to `group.clone()`. That is the base-ingest
+            // half of §0.4's re-carry hazard, and it is invisible to any test
+            // that does not reload: within one session nothing has been
+            // maintained into the carried slot, so a re-carry of
+            // `CreateStaffGroup(g, [])` still compares `[]` against `[]` and
+            // correctly yields `AlreadyApplied`. A snapshot round trip then
+            // launders the *derived* value into the carried slot, and the same
+            // re-carry compares `[]` against `[s]` and misverdicts
+            // `RecreateContentMismatch`. `t8d` is the only test that crosses
+            // that boundary; pin 4 is unguarded without it.
+            let mut carried = group.clone();
+            carried.members.clear();
+            self.staff_group_values.insert(group.id, carried);
         }
         for part in &score.parts {
             self.objects
@@ -2966,6 +2988,37 @@ impl<'a> Reducer<'a> {
                 // graph (the undo path preconditions no live reference remains).
                 TypedObjectId::Staff(id) => {
                     score.staves.retain(|value| value.id != *id);
+                    // P13-S16 pin 5: `StaffGroup.members` is a projection of
+                    // `Staff.group`, so a staff leaving the graph must also
+                    // leave every group that lists it — otherwise the undo
+                    // strands a group naming a staff that no longer exists.
+                    //
+                    // **That residue is NOT invariant 21, checked rather than
+                    // assumed.** A stranded id has no staff left to disagree
+                    // with, and invariant 21 abstains on dangling members —
+                    // agreement is a claim about *live* pairs. Run M5 and
+                    // invariant 21 reports nothing, while invariant 10
+                    // `CrossCuttingRefsResolve` reports "staff group ... member
+                    // staff ... is not declared". What pin 5 closes is the
+                    // unguarded **projection-maintenance** direction; the
+                    // detector for the dangling reference it would otherwise
+                    // leave is invariant 10.
+                    //
+                    // The maintenance pair is guarded asymmetrically, which is
+                    // why the repair belongs here: `undo_strand_block`'s
+                    // `TypedObjectId::StaffGroup` arm already refuses to undo a
+                    // group a live staff still names, but nothing blocks undoing
+                    // the staff itself. This walk's own `StaffGroup` arm needs no
+                    // change.
+                    //
+                    // Only the graph needs stripping. The one other place a
+                    // `StaffGroup` value is held, `staff_group_values`, carries
+                    // the authored value whose `members` pin 1 keeps empty and
+                    // pin 4 re-empties in `seed_from_graph` — so there is no
+                    // derived copy anywhere else for this id to survive in.
+                    for group in &mut score.staff_groups {
+                        group.members.retain(|member| member != id);
+                    }
                 }
                 TypedObjectId::TimeSignature(id) => {
                     score.time_signatures.retain(|value| value.id != *id);
@@ -4327,6 +4380,13 @@ impl<'a> Reducer<'a> {
     /// precondition no-op. Graph-aware reduction additionally preconditions
     /// that the referenced instrument is live and, when `group` is present,
     /// that the staff group resolves.
+    ///
+    /// **P13-S16 pin 2:** when `group` is present this also **maintains that
+    /// group's `members`** in the graph, appending this staff's id. `Staff.group`
+    /// is the sole authority; `StaffGroup.members` is the projection maintained
+    /// from it, and the two must agree in both directions (graph invariant 21).
+    /// The maintained value is written **only** to `self.graph` — never to
+    /// `staff_group_values`, which holds the group as authored (pin 3).
     fn create_staff(&mut self, env: &OperationEnvelope, op: &CreateStaffOp) -> OperationEffect {
         let sobj = TypedObjectId::Staff(op.staff_id());
         match self.objects.get(&sobj) {
@@ -4384,6 +4444,27 @@ impl<'a> Reducer<'a> {
         }
         if let Some(score) = self.graph.as_mut() {
             score.staves.push(op.staff.clone());
+            // P13-S16 pin 2: maintain `StaffGroup.members` from `Staff.group`,
+            // which is the sole authority. Only in the graph — `staff_group_values`
+            // keeps the value as authored (pin 3), so the re-carry comparator at
+            // `create_staff_group` still compares carried against carried.
+            // Base-free reduction has no graph to maintain, which the enclosing
+            // `if let` already guards.
+            //
+            // Set-union and order-independent per staff id, and idempotent:
+            // convergence replays operations, so an id already present is never
+            // appended twice.
+            if let Some(group_id) = op.staff.group {
+                if let Some(group) = score
+                    .staff_groups
+                    .iter_mut()
+                    .find(|group| group.id == group_id)
+                {
+                    if !group.members.contains(&op.staff_id()) {
+                        group.members.push(op.staff_id());
+                    }
+                }
+            }
         }
         self.mint_container(env, sobj);
         self.staff_values.insert(op.staff_id(), op.staff.clone());
@@ -4450,11 +4531,23 @@ impl<'a> Reducer<'a> {
     // has no universe to check against. -------------------------------------
 
     /// Set-union creation of a global `StaffGroup` on the score root
-    /// (operation_catalog §CreateStaffGroup). Graph-aware reduction
+    /// (operation_catalog §CreateStaffGroup). A carried non-empty `members` is
-    /// preconditions every carried member resolves to a live `Staff`. Per
+    /// **refused**: this operation authors the group, not its membership, which
-    /// §1.1 (disposition B), `members` is stored exactly as carried and
+    /// is **maintained from `Staff.group`** under reduction (`create_staff`,
-    /// neither maintained nor trusted thereafter — `Staff.group` is the sole
+    /// P13-S16 pin 2). `Staff.group` remains the sole authority and
-    /// authority for membership.
+    /// `StaffGroup.members` its maintained projection; the two **must agree**
+    /// in both directions (graph invariant 21).
+    ///
+    /// **P13-S16 inverted the previous rule, and the inversion is deliberate.**
+    /// Before this rung, per §1.1 disposition B, `members` was stored exactly as
+    /// carried and neither maintained nor trusted — a non-empty carried value
+    /// was accepted and left permanently stale. It is now unauthorable.
+    ///
+    /// The refusal is an **empty-container precondition on the carried value**,
+    /// not a referential one, so unlike the sibling mints' member-liveness
+    /// checks it is **not graph-gated**: it holds base-free too. Conflating the
+    /// two classes is how a later reader would wrongly restore a graph gate here
+    /// (see `t7`'s inversion).
     fn create_staff_group(
         &mut self,
         env: &OperationEnvelope,
@@ -4486,19 +4579,13 @@ impl<'a> Reducer<'a> {
             }
             None => {}
         }
-        if self.graph.is_some() {
+        // Reject a carried non-empty `members`: the mint authors the group, and
-            for member in &op.group.members {
+        // membership is maintained from `Staff.group` (P13-S16 pin 2). Unlike the
-                if !matches!(
+        // sibling mints' referential preconditions this is NOT graph-gated — an
-                    self.objects.get(&TypedObjectId::Staff(*member)),
+        // empty-container precondition asks only about the carried value, so it
-                    Some(ObjectState::Live)
+        // holds base-free as well (pin 1; `t7` asserts the inversion).
-                ) {
+        if !op.group.members.is_empty() {
-                    return OperationEffect::NoOp {
+            return container_not_empty();
-                        reason: NoOpReason::PreconditionFailedUnderReduction {
-                            reason: PreconditionFailureReason::TargetMissing,
-                        },
-                    };
-                }
-            }
         }
         if let Some(score) = self.graph.as_mut() {
             score.staff_groups.push(op.group.clone());
@@ -16145,15 +16232,27 @@ mod tests {
         assert_eq!(out.score.views.len(), 1, "no duplicate view minted");
     }
 
-    /// (t6) Genesis tranche G3a: all three referential loops refuse under a
+    /// (t6) Genesis tranche G3a: the referential loops refuse under a graph —
-    /// graph, each asserted separately: `CreateStaffGroup.members`,
+    /// `CreatePartDefinition.staves` and `CreateView.active_layers` naming a
-    /// `CreatePartDefinition.staves`, and `CreateView.active_layers` naming a
+    /// non-live target are each `TargetMissing` — while `CreateStaffGroup`
-    /// non-live target are each `TargetMissing`.
+    /// refuses any non-empty carried `members` outright.
     ///
-    /// **Mutation (three separate sub-mutations, each run alone):** drop the
+    /// **P13-S16 pin 1a inverted the first arm.** Before this rung all three
-    /// members loop from `create_staff_group`; drop the staves loop from
+    /// arms asserted `TargetMissing`, and the first was a genuine *referential*
-    /// `create_part_definition`; drop the active-layers loop from
+    /// precondition: a liveness loop checking `members` against the graph. Pin 1
-    /// `create_view`. Each must fail on its own row.
+    /// replaced that loop with an **empty-container** precondition — the mint
+    /// authors the group and membership is maintained from `Staff.group`, so a
+    /// carried `members` is refused `ContainerNotEmpty` whether or not its ids
+    /// are live. The arm below keeps its non-live id **only to show liveness has
+    /// stopped mattering**: the identical refusal fires for a live one. It no
+    /// longer tests a referential loop at all. The other two arms are untouched
+    /// and must stay — they are the reason this test still has a referential
+    /// claim to make.
+    ///
+    /// **Mutation:** the `CreateStaffGroup` arm is signed by **M1** (remove pin
+    /// 1's refusal). The other two keep their own sub-mutations, each run alone:
+    /// drop the staves loop from `create_part_definition`; drop the
+    /// active-layers loop from `create_view`. Each must fail on its own row.
     #[test]
     fn t6_g3a_referential_loops_refuse_a_dangling_target_under_a_graph() {
         let target_missing = Some(OperationEffect::NoOp {
@@ -16162,7 +16261,9 @@ mod tests {
             },
         });
 
-        // CreateStaffGroup.members naming a non-live staff.
+        // CreateStaffGroup carrying a non-empty `members` — refused as an
+        // empty-container precondition (pin 1), so the id's non-liveness is
+        // incidental rather than the reason.
         let dangling_staff = StaffId::new(ReplicaId(1), 99);
         let group =
             crate::valuegen::staff_group(StaffGroupId::new(ReplicaId(1), 1), vec![dangling_staff]);
@@ -16177,8 +16278,9 @@ mod tests {
                 .iter()
                 .find(|(e, _)| *e == group_env.id)
                 .map(|(_, eff)| eff.clone()),
-            target_missing,
+            Some(container_not_empty()),
-            "CreateStaffGroup.members naming a non-live staff must refuse TargetMissing"
+            "CreateStaffGroup carrying a non-empty members must refuse \
+             ContainerNotEmpty (P13-S16 pin 1), not TargetMissing"
         );
 
         // CreatePartDefinition.staves naming a non-live staff.
@@ -16220,13 +16322,32 @@ mod tests {
         );
     }
 
-    /// (t7) Genesis tranche G3a: those same referential preconditions are
+    /// (t7) Genesis tranche G3a, **inverted by P13-S16 pin 1a**:
-    /// **not** enforced base-free — base-free reduction has no universe to
+    /// `CreateStaffGroup`'s non-empty-`members` refusal **is** enforced
-    /// check against.
-    ///
-    /// **Mutation:** remove the `if self.graph.is_some()` guard from
-    /// `create_staff_group`; must fail — the dangling member now refuses even
     /// base-free.
+    ///
+    /// **Before this rung this arm asserted `Applied`**, on the sound reasoning
+    /// that base-free reduction has no staff universe to check a member's
+    /// liveness against. Pin 1 changed the *class* of the precondition, and that
+    /// is the whole reason the assertion inverts:
+    ///
+    /// - A **graph-aware** precondition asks about the *universe* — "is this id
+    ///   live?" — and genuinely cannot run base-free. There is nothing to ask.
+    /// - An **empty-container** precondition asks only about the *carried value*
+    ///   — "is `members` empty?" — which is answerable with no graph at all, so
+    ///   it holds everywhere.
+    ///
+    /// **These are different classes, and conflating them is how a later reader
+    /// would wrongly "restore" the graph gate** — reinstating an
+    /// `if self.graph.is_some()` around a check that never needed one. M9 is
+    /// exactly that mutation, and this arm is its only signature.
+    ///
+    /// The sibling referential preconditions (`CreatePartDefinition.staves`,
+    /// `CreateView.active_layers`) are unchanged and still are not enforced
+    /// base-free; see `t6`.
+    ///
+    /// **Mutation (M9):** graph-gate pin 1's refusal in `create_staff_group`;
+    /// must fail — the carried `members` would then be accepted base-free.
     #[test]
     fn t7_g3a_referential_preconditions_are_not_enforced_base_free() {
         let dangling_staff = StaffId::new(ReplicaId(1), 99);
@@ -16242,8 +16363,10 @@ mod tests {
                 .iter()
                 .find(|(e, _)| *e == group_env.id)
                 .map(|(_, eff)| eff.clone()),
-            Some(OperationEffect::Applied),
+            Some(container_not_empty()),
-            "base-free reduction has no staff universe to check the dangling member against"
+            "an empty-container precondition asks only about the carried value, \
+             so it refuses base-free too (P13-S16 pin 1a); a graph gate here \
+             would wrongly accept"
         );
     }
 
@@ -16314,29 +16437,47 @@ mod tests {
         );
     }
 
-    /// (t8b) Both permitted stale forms (§1.1, disposition B) are pinned:
+    /// (t8b) **P13-S16 pin 7 inverted this test.** The projection is
-    /// the **missing** form (`CreateStaffGroup(g, [])` ->
+    /// **maintained** in the missing order, and the spurious form is
-    /// `CreateStaff(s, Some(g))` ⟹ `s.group == Some(g)`, `g.members == []`)
+    /// **refused** — the same two authoring orders as before (§0.5), with the
-    /// and the **spurious** form (`CreateStaff(s, None)` ->
+    /// verdicts the ratified disposition A requires.
-    /// `CreateStaffGroup(g, [s])` ⟹ `g.members == [s]`, `s.group == None`).
-    /// Both asserted to **hold**, as states the ruling permits.
     ///
-    /// **Mutation 1 (missing form; mutate `create_staff`, which runs SECOND
+    /// **It previously pinned the exact opposite**, as
-    /// in this order):** when `group` is `Some(g)`, append the newly minted
+    /// `t8b_both_permitted_stale_forms_hold`: under disposition B both stale
-    /// staff to `g.members` (disposition A's maintenance rule); the
+    /// forms were *permitted states*, so the missing form left `g.members == []`
-    /// missing-form assertion must fail.
+    /// and the spurious form let `g.members == [s]` reach the graph alongside
+    /// `s.group == None`. **That is not a regression being fixed here** — it was
+    /// the correct assertion under the ruling in force at the time. P13-S16
+    /// ratified disposition A, under which `Staff.group` is the sole authority
+    /// and `StaffGroup.members` is maintained from it (pins 1 and 2), so neither
+    /// disagreeing state is reachable any more and the assertions invert with the
+    /// ruling.
     ///
-    /// **Mutation 2 (spurious form; mutate `create_staff_group`, which runs
+    /// **Deleting this test is forbidden** — the *pairing* of the two orders is
-    /// SECOND in this order):** reject or normalize away a non-empty carried
+    /// the coverage, because each order signs a different production change.
-    /// `members`; the spurious-form assertion must fail.
     ///
-    /// An earlier draft assigned these the other way round, which is
+    /// **Mutation 1 (M1; spurious order, where `create_staff_group` runs
-    /// impossible in both directions: `create_staff_group` runs first in the
+    /// SECOND):** remove pin 1's refusal; the group mints carrying `[s]` while
-    /// missing order and cannot append a staff that does not exist yet, and
+    /// `s.group` is `None`.
-    /// `create_staff` runs first in the spurious order and has no later group
+    ///
-    /// to repair.
+    /// **Mutation 2 (M2; missing order, where `create_staff` runs SECOND):**
+    /// remove pin 2's append; `g.members` stays empty and invariant 21 fires.
+    ///
+    /// An earlier draft assigned these the other way round, which is impossible
+    /// in both directions: `create_staff_group` runs first in the missing order
+    /// and cannot append a staff that does not exist yet, and `create_staff`
+    /// runs first in the spurious order and has no later group to repair.
+    ///
+    /// **Observation harness (pin 7a).** The two orders are two reductions over
+    /// two *different* groups, so there are **four** observations, not three —
+    /// and a `#[test]` emits nothing but its assertion diagnostics, so state not
+    /// in those diagnostics is unobtainable. All four are bound **before any
+    /// assertion** and formatted into **every** assertion's message: a failing
+    /// test stops at its *first* failed assertion, and M1 and M2 trip
+    /// *different* assertions, so each one must carry the whole set. Splitting
+    /// the set per order would reintroduce the same gap one level down.
     #[test]
-    fn t8b_both_permitted_stale_forms_hold() {
+    fn t8b_the_projection_is_maintained_and_the_spurious_form_is_refused() {
         let instrument_id = InstrumentId::new(ReplicaId(1), 1);
 
         // Missing form: CreateStaffGroup(g, []) -> CreateStaff(s, Some(g)).
@@ -16371,28 +16512,6 @@ mod tests {
         set.accept_all(vec![create_instrument, create_group, create_staff]);
         let out =
             reduce_operation_set_onto(&set, &Score::empty(IdentityContext::new(ReplicaId(1))));
-        let staff = out
-            .score
-            .staves
-            .iter()
-            .find(|s| s.id == staff_id)
-            .expect("staff minted");
-        assert_eq!(
-            staff.group,
-            Some(group_id),
-            "missing form: s.group == Some(g)"
-        );
-        let group = out
-            .score
-            .staff_groups
-            .iter()
-            .find(|g| g.id == group_id)
-            .expect("group minted");
-        assert_eq!(
-            group.members,
-            Vec::<StaffId>::new(),
-            "missing form: g.members stays empty (stored, not maintained)"
-        );
 
         // Spurious form: CreateStaff(s, None) -> CreateStaffGroup(g, [s]).
         let group_id2 = StaffGroupId::new(ReplicaId(2), 3);
@@ -16421,45 +16540,335 @@ mod tests {
             CausalContext::new(),
             crate::valuegen::staff_group(group_id2, vec![staff_id2]),
         );
+        let spurious_group_env_id = create_group2.id;
         let mut set2 = OperationSet::new();
         set2.accept_all(vec![create_instrument2, create_staff2, create_group2]);
         let out2 =
             reduce_operation_set_onto(&set2, &Score::empty(IdentityContext::new(ReplicaId(2))));
-        let group2 = out2
+
+        // ---------------------------------------------------------------------
+        // Pin 7a's four bindings. ALL taken BEFORE ANY assertion, and read
+        // through `find`/`map` rather than `expect` — an `expect` panic here
+        // would preempt the harness and emit nothing.
+        // ---------------------------------------------------------------------
+
+        // [1] Spurious-order effect for the `CreateStaffGroup` op. M1 turns this
+        //     into an applied effect.
+        let spurious_effect = out2
+            .state
+            .effects
+            .iter()
+            .find(|(e, _)| *e == spurious_group_env_id)
+            .map(|(_, eff)| eff.clone());
+        // [2] Spurious-order `StaffGroup.members` — `None` while pin 1 refuses
+        //     the mint outright. M1 makes it `Some([s])`: the spurious
+        //     membership that reached the graph.
+        let spurious_members: Option<Vec<StaffId>> = out2
             .score
             .staff_groups
             .iter()
             .find(|g| g.id == group_id2)
-            .expect("group minted");
+            .map(|g| g.members.clone());
-        assert_eq!(
+        // [3] Missing-order `StaffGroup.members` — `[s]` while pin 2 maintains
-            group2.members,
+        //     it. M2 leaves it empty. A DIFFERENT group in a DIFFERENT
-            vec![staff_id2],
+        //     reduction from [2]; one shared `members` local would satisfy this
-            "spurious form: g.members == [s]"
+        //     harness while leaving one mutation's observation absent.
+        let missing_members: Option<Vec<StaffId>> = out
+            .score
+            .staff_groups
+            .iter()
+            .find(|g| g.id == group_id)
+            .map(|g| g.members.clone());
+        // [4] Missing-order invariant-21 verdict — the disagreement an
+        //     unmaintained projection leaves. Filtered from the missing-order
+        //     score; from the other reduction it would be the wrong verdict
+        //     rather than a missing one.
+        let missing_agreement = epiphany_core::check_invariant(
+            &out.score,
+            epiphany_core::GraphInvariant::StaffGroupMembershipAgreement,
         );
-        let staff2 = out2
+
+        let harness = format!(
+            "\n  [1] spurious-order CreateStaffGroup effect: {spurious_effect:?}\
+             \n  [2] spurious-order g.members:               {spurious_members:?}\
+             \n  [3] missing-order  g.members:               {missing_members:?}\
+             \n  [4] missing-order  invariant-21 violations: {missing_agreement:?}"
+        );
+
+        // ---- Missing order: the projection is maintained. --------------------
+        let missing_staff_group = out
+            .score
+            .staves
+            .iter()
+            .find(|s| s.id == staff_id)
+            .map(|s| s.group);
+        assert_eq!(
+            missing_staff_group,
+            Some(Some(group_id)),
+            "missing order: s.group == Some(g) — the staff carries the sole \
+             authority{harness}"
+        );
+        assert_eq!(
+            missing_members.as_deref(),
+            Some(&[staff_id][..]),
+            "missing order: g.members is MAINTAINED to [s] (P13-S16 pin 2), not \
+             left empty as disposition B permitted{harness}"
+        );
+        assert!(
+            missing_agreement.is_empty(),
+            "missing order: a maintained projection must leave invariant 21 \
+             clean{harness}"
+        );
+
+        // ---- Spurious order: the mint is refused. ---------------------------
+        assert_eq!(
+            spurious_effect,
+            Some(container_not_empty()),
+            "spurious order: CreateStaffGroup carrying [s] must refuse \
+             ContainerNotEmpty (P13-S16 pin 1){harness}"
+        );
+        assert_eq!(
+            spurious_members, None,
+            "spurious order: the refused mint must leave no group in the \
+             graph{harness}"
+        );
+        let spurious_staff_group = out2
             .score
             .staves
             .iter()
             .find(|s| s.id == staff_id2)
-            .expect("staff minted");
+            .map(|s| s.group);
-        assert_eq!(staff2.group, None, "spurious form: s.group == None");
+        assert_eq!(
+            spurious_staff_group,
+            Some(None),
+            "spurious order: s.group stays None — CreateStaffGroup never writes \
+             Staff.group{harness}"
+        );
+    }
+
+    /// (t8c) **P13-S16 pin 3a.** The re-carry comparator reads the **carried**
+    /// `members`, never the derived one: after maintenance has put `[s]` into the
+    /// graph, a byte-identical re-carry of `CreateStaffGroup(g, [])` is still
+    /// `AlreadyApplied`.
+    ///
+    /// This is the hazard of §0.4. `create_staff_group`'s idempotence check
+    /// compares `op.group` against `self.staff_group_values` as a **whole
+    /// value**, `members` included. If pin 2's maintenance wrote the
+    /// appended members into that map, the re-carry would compare `[]` against
+    /// `[s]` and return `RecreateContentMismatch` — a spurious conflict on an
+    /// operation that genuinely is a duplicate. Pin 2 therefore writes the
+    /// maintained members **only** into `self.graph`, and pin 3 leaves the
+    /// comparator untouched.
+    ///
+    /// The second assertion is what makes the first one mean something: without
+    /// it, `AlreadyApplied` would also pass on a build where maintenance never
+    /// ran at all, and the test would be pinning the absence of a feature rather
+    /// than the separation of two values.
+    ///
+    /// **Mutation (M3):** make pin 3 write the derived members into
+    /// `staff_group_values`; the re-carry becomes `RecreateContentMismatch`.
+    ///
+    /// A mutation demonstrates the hazard once; only a test keeps it
+    /// demonstrated.
+    #[test]
+    fn t8c_recarry_compares_against_the_carried_members_not_the_derived() {
+        let instrument_id = InstrumentId::new(ReplicaId(1), 1);
+        let group_id = StaffGroupId::new(ReplicaId(1), 3);
+        let staff_id = StaffId::new(ReplicaId(1), 5);
+
+        let create_instrument = prim_env(
+            1,
+            0,
+            10,
+            CausalContext::new(),
+            OperationKind::CreateInstrument(CreateInstrumentOp {
+                instrument: crate::valuegen::instrument(instrument_id),
+            }),
+        );
+        let create_group = staff_group_env(
+            1,
+            2,
+            20,
+            CausalContext::new(),
+            crate::valuegen::staff_group(group_id, vec![]),
+        );
+        let mut staff = crate::valuegen::staff(staff_id, instrument_id);
+        staff.group = Some(group_id);
+        let create_staff = prim_env(
+            1,
+            4,
+            30,
+            CausalContext::new(),
+            OperationKind::CreateStaff(CreateStaffOp { staff }),
+        );
+        // The re-carry: byte-identical to `create_group`, authored after
+        // maintenance has run.
+        let recarry = staff_group_env(
+            1,
+            6,
+            40,
+            CausalContext::new(),
+            crate::valuegen::staff_group(group_id, vec![]),
+        );
+        let recarry_env_id = recarry.id;
+
+        let mut set = OperationSet::new();
+        set.accept_all(vec![create_instrument, create_group, create_staff, recarry]);
+        let out =
+            reduce_operation_set_onto(&set, &Score::empty(IdentityContext::new(ReplicaId(1))));
+
+        let recarry_effect = out
+            .state
+            .effects
+            .iter()
+            .find(|(e, _)| *e == recarry_env_id)
+            .map(|(_, eff)| eff.clone());
+        let members: Option<Vec<StaffId>> = out
+            .score
+            .staff_groups
+            .iter()
+            .find(|g| g.id == group_id)
+            .map(|g| g.members.clone());
+
+        assert_eq!(
+            recarry_effect,
+            Some(OperationEffect::NoOp {
+                reason: NoOpReason::AlreadyApplied,
+            }),
+            "a byte-identical re-carry must compare against the CARRIED members \
+             and read AlreadyApplied; graph members at this moment: {members:?}"
+        );
+        assert_eq!(
+            members.as_deref(),
+            Some(&[staff_id][..]),
+            "and the graph's derived members must genuinely hold [s] at that \
+             moment — otherwise AlreadyApplied proves nothing about separation"
+        );
+    }
+
+    /// (t8d) **P13-S16 pin 4a.** The same idempotence holds **across a reload**:
+    /// reduce, materialize the score, re-reduce onto it as a *base*, and a
+    /// re-carry of `CreateStaffGroup(g, [])` is still `AlreadyApplied`.
+    ///
+    /// **This is the only test that crosses the snapshot boundary, and pin 4 is
+    /// unguarded without it.** `t8c` cannot see the defect pin 4 fixes: within
+    /// one session nothing has been maintained into `staff_group_values`, so the
+    /// comparison is `[]` against `[]` whichever way base ingest is written. Base
+    /// ingest (`seed_from_graph`) reseeds that map from `score.staff_groups` — the
+    /// **maintained** value — so a `group.clone()` there launders the derived
+    /// members into the carried slot, and the misverdict appears only *after* a
+    /// reload. Pin 4 empties `members` on the seed, which is exact rather than
+    /// lossy because pin 1 makes empty the only authorable carried value.
+    ///
+    /// **Mutation (M4):** restore `group.clone()` at the base-ingest seed; this
+    /// test fails with `RecreateContentMismatch` while `t8c`, which never
+    /// reloads, still passes.
+    #[test]
+    fn t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent() {
+        let instrument_id = InstrumentId::new(ReplicaId(1), 1);
+        let group_id = StaffGroupId::new(ReplicaId(1), 3);
+        let staff_id = StaffId::new(ReplicaId(1), 5);
+
+        // Session 1: the pin-3a sequence, reduced from empty.
+        let create_instrument = prim_env(
+            1,
+            0,
+            10,
+            CausalContext::new(),
+            OperationKind::CreateInstrument(CreateInstrumentOp {
+                instrument: crate::valuegen::instrument(instrument_id),
+            }),
+        );
+        let create_group = staff_group_env(
+            1,
+            2,
+            20,
+            CausalContext::new(),
+            crate::valuegen::staff_group(group_id, vec![]),
+        );
+        let mut staff = crate::valuegen::staff(staff_id, instrument_id);
+        staff.group = Some(group_id);
+        let create_staff = prim_env(
+            1,
+            4,
+            30,
+            CausalContext::new(),
+            OperationKind::CreateStaff(CreateStaffOp { staff }),
+        );
+        let mut set = OperationSet::new();
+        set.accept_all(vec![create_instrument, create_group, create_staff]);
+        let first =
+            reduce_operation_set_onto(&set, &Score::empty(IdentityContext::new(ReplicaId(1))));
+
+        // The materialized score becomes the base — the reload boundary. It
+        // carries the MAINTAINED members, which is what makes the seed lossy if
+        // pin 4 is undone.
+        let base = first.score.clone();
+        let base_members: Option<Vec<StaffId>> = base
+            .staff_groups
+            .iter()
+            .find(|g| g.id == group_id)
+            .map(|g| g.members.clone());
+
+        // Session 2: re-carry against that base.
+        let recarry = staff_group_env(
+            1,
+            8,
+            50,
+            CausalContext::new(),
+            crate::valuegen::staff_group(group_id, vec![]),
+        );
+        let recarry_env_id = recarry.id;
+        let mut set2 = OperationSet::new();
+        set2.accept_all(vec![recarry]);
+        let out = reduce_operation_set_onto(&set2, &base);
+
+        let recarry_effect = out
+            .state
+            .effects
+            .iter()
+            .find(|(e, _)| *e == recarry_env_id)
+            .map(|(_, eff)| eff.clone());
+
+        assert_eq!(
+            base_members.as_deref(),
+            Some(&[staff_id][..]),
+            "precondition: the materialized base must carry the maintained \
+             members, or this test is not exercising the reload hazard at all"
+        );
+        assert_eq!(
+            recarry_effect,
+            Some(OperationEffect::NoOp {
+                reason: NoOpReason::AlreadyApplied,
+            }),
+            "across a reload the re-carry must still compare against the CARRIED \
+             members (P13-S16 pin 4); base members were {base_members:?}"
+        );
     }
 
     /// (t9) A score reduced from empty through all four G3a ops **passes
     /// `check_invariants`**, and each skipped reducer check **independently**
-    /// makes invariant 10 fire (pin 5). The fixture is constant across all
+    /// makes invariant 10 fire (pin 5). The fixture is constant across the
-    /// mutations: it already attempts a dangling reference in each of the
+    /// mutations that remain: it attempts a dangling reference in each of the
-    /// three referential loops, and passes only because the reducer refuses
+    /// **two** referential loops, and passes only because the reducer refuses
     /// them.
     ///
-    /// **Mutation (three separate sub-mutations, each run alone; mutate
+    /// **P13-S16 pin 1a changed the fixture and shrank the mutation set.**
-    /// production only):** drop the members loop from `create_staff_group` /
+    /// `CreateStaffGroup` previously carried a dangling member here, making a
-    /// the staves loop from `create_part_definition` / the active-layers loop
+    /// third referential row. Pin 1 refuses *any* non-empty carried `members`,
-    /// from `create_view`. Each must let its dangling reference through and
+    /// so that op can no longer smuggle a dangling reference into the graph at
-    /// make invariant 10 fire.
+    /// all — the refusal happens before liveness is ever consulted, and no
+    /// mutation of it can make invariant 10 fire from this op. The group
+    /// therefore carries `[]` and **applies**, which is also what keeps this
+    /// test a required survivor of **M1**: with nothing dangling attempted
+    /// through this op, removing pin 1's refusal changes nothing here.
+    ///
+    /// **Mutation (two separate sub-mutations, each run alone; mutate
+    /// production only):** drop the staves loop from `create_part_definition` /
+    /// the active-layers loop from `create_view`. Each must let its dangling
+    /// reference through and make invariant 10 fire.
     #[test]
     fn t9_from_empty_through_all_four_g3a_ops_passes_check_invariants() {
-        let dangling_staff_a = StaffId::new(ReplicaId(1), 90);
         let dangling_staff_b = StaffId::new(ReplicaId(1), 91);
         let dangling_layer = AnalysisLayerId::new(ReplicaId(1), 92);
 
@@ -16468,10 +16877,9 @@ mod tests {
             0,
             10,
             CausalContext::new(),
-            crate::valuegen::staff_group(
+            // Empty: pin 1 refuses any carried `members`, so this op cannot
-                StaffGroupId::new(ReplicaId(1), 1),
+            // contribute a dangling reference and applies instead.
-                vec![dangling_staff_a],
+            crate::valuegen::staff_group(StaffGroupId::new(ReplicaId(1), 1), vec![]),
-            ),
         );
         let create_part = part_definition_env(
             1,
@@ -16517,8 +16925,9 @@ mod tests {
         });
         assert_eq!(
             effect_at(&out.state, 0),
-            target_missing,
+            Some(&OperationEffect::Applied),
-            "CreateStaffGroup with a dangling member must refuse"
+            "CreateStaffGroup carrying an empty members has nothing to refuse \
+             and applies (P13-S16 pin 1a)"
         );
         assert_eq!(
             effect_at(&out.state, 2),
@@ -17745,6 +18154,143 @@ mod tests {
         );
     }
 
+    /// (u5) **P13-S16 pin 5a.** Undoing a `CreateStaff` strips the staff's id
+    /// from every live group's `members`.
+    ///
+    /// **This is the unguarded direction of projection maintenance** — *not* of
+    /// invariant 21; see assertion 4 for why the distinction is load-bearing. The
+    /// reverse direction is blocked: `undo_strand_block`'s
+    /// `TypedObjectId::StaffGroup` arm refuses to undo a group a live staff still
+    /// names (see `u2a`). Nothing blocks undoing the *staff*, so before pin 5 the
+    /// undo removed it from `Score.staves` and left its id sitting in
+    /// `g.members`: a group naming a staff that no longer exists.
+    ///
+    /// **Nothing permanent exercised this sequence before, checked rather than
+    /// assumed.** Pin 8's four are group-undo guards; `u2tomb_a` undoes a staff
+    /// but undoes the group along with it — it asserts *"the group leaves
+    /// `Score.staff_groups`"* — so no *live* group's `members` is ever inspected.
+    /// `m41`/`m41b` build materialized fixtures and never run the reducer's undo
+    /// path at all. A mutation demonstrates the hazard once; only a test keeps it
+    /// demonstrated.
+    ///
+    /// **Mutation (M5):** remove pin 5's strip from the `Staff` arm of
+    /// `materialize_graph_tombstones`; assertion 2 fails with `s` still in
+    /// `members`.
+    ///
+    /// **Observation harness (same rule as pin 7a).** Both the post-undo
+    /// `members` and the invariant-21 violations are bound **before assertion
+    /// 2**, and both appear in every assertion's message. Under M5 it is
+    /// assertion 2 that fires, so assertion 3 never executes — computing the
+    /// violations only where assertion 3 needs them would put M5's required
+    /// witness behind an assertion M5 guarantees is unreachable. **The state a
+    /// mutation owes must be bound before the assertion that mutation trips.**
+    #[test]
+    fn u5_undoing_a_staff_strips_it_from_the_live_groups_members() {
+        let identity = IdentityContext::new(ReplicaId(1));
+        let instrument_id = InstrumentId::new(ReplicaId(9), 1);
+        let mut base = Score::empty(identity);
+        base.instruments
+            .push(crate::valuegen::instrument(instrument_id));
+
+        let group_id = StaffGroupId::new(ReplicaId(1), 1);
+        let staff_id = StaffId::new(ReplicaId(1), 5);
+        let tx = TransactionId::new(ReplicaId(1), 900);
+
+        let mut staff_value = crate::valuegen::staff(staff_id, instrument_id);
+        staff_value.group = Some(group_id);
+
+        let mut set = OperationSet::new();
+        set.accept_all(vec![
+            // The group is authored OUTSIDE the transaction, so undoing the
+            // transaction takes the staff and leaves the group live — which is
+            // what gives assertion 1 something to hold.
+            staff_group_env(
+                1,
+                0,
+                10,
+                CausalContext::new(),
+                crate::valuegen::staff_group(group_id, vec![]),
+            ),
+            declare_transaction(1, 1, 20, seen_r1(0), tx),
+            tx_member(
+                1,
+                2,
+                21,
+                seen_r1(1),
+                tx,
+                OperationKind::CreateStaff(CreateStaffOp { staff: staff_value }),
+            ),
+            undo_env(1, 3, 30, seen_r1(2), tx, UndoPolicy::StrictInverse),
+        ]);
+        let out = reduce_operation_set_onto(&set, &base);
+
+        // Bound BEFORE assertion 2 — see the harness note above.
+        let members: Option<Vec<StaffId>> = out
+            .score
+            .staff_groups
+            .iter()
+            .find(|g| g.id == group_id)
+            .map(|g| g.members.clone());
+        let agreement = epiphany_core::check_invariant(
+            &out.score,
+            epiphany_core::GraphInvariant::StaffGroupMembershipAgreement,
+        );
+        let staff_present = out.score.staves.iter().any(|s| s.id == staff_id);
+        let all_violations = epiphany_core::check_invariants(&out.score);
+        let harness = format!(
+            "\n  post-undo g.members:            {members:?}\
+             \n  invariant-21 violations:        {agreement:?}\
+             \n  staff {staff_id:?} still in graph: {staff_present}\
+             \n  ALL violations:                 {all_violations:?}"
+        );
+
+        // 1. The group must still be live, or there is no projection left to be
+        //    wrong and this test asserts nothing.
+        assert!(
+            out.score.staff_groups.iter().any(|g| g.id == group_id),
+            "the group must survive the staff's undo for this test to mean \
+             anything{harness}"
+        );
+        // 1b. Not in pin 5a's list, added so a BLOCKED undo cannot be mistaken
+        //     for a failed strip: both leave `s` in `members`, and only this
+        //     tells them apart.
+        assert!(
+            !staff_present,
+            "precondition: the staff's undo must actually have removed it from \
+             the graph — if it was blocked instead, assertion 2 below would fail \
+             for an unrelated reason{harness}"
+        );
+        // 2. The strip itself.
+        assert!(
+            !members.as_deref().unwrap_or_default().contains(&staff_id),
+            "P13-S16 pin 5: undoing the staff must strip {staff_id:?} from the \
+             live group's members{harness}"
+        );
+        // 3. Pin 5a's third assertion: no invariant-21 residue in either
+        //    direction.
+        assert!(
+            agreement.is_empty(),
+            "the post-undo graph must leave invariant 21 clean in both \
+             directions{harness}"
+        );
+        // 4. Added during execution, because assertion 3 CANNOT see the residue
+        //    this test exists to catch — observed, not reasoned. Under M5 the
+        //    strip is gone and `members` keeps an id whose staff has left the
+        //    graph: that is a **dangling** reference, and invariant 21
+        //    deliberately abstains on those (agreement is a claim about live
+        //    pairs; dangling resolution belongs to the referential invariants).
+        //    M5 was run and invariant 21 reported `[]`, while invariant 10
+        //    `CrossCuttingRefsResolve` reported "staff group ... member staff
+        //    ... is not declared". Pin 5a expects assertion 3 to fail "on a
+        //    residue whichever direction it leaves"; on its own it does not, so
+        //    the whole set is asserted here.
+        assert!(
+            all_violations.is_empty(),
+            "the post-undo graph must be invariant-clean overall — a stripped \
+             member must not be left dangling either{harness}"
+        );
+    }
+
     // =========================================================================
     // Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md`): CreateMeasure,
     // the comparable relation (pin 6), the musical delta (pin 6b), and the

crates/epiphany-ops/src/valuegen.rs

@@ -369,10 +369,15 @@ pub fn instrument(id: epiphany_core::InstrumentId) -> epiphany_core::Instrument
     epiphany_core::Instrument::new(id, format!("instrument-{}", id.counter()))
 }
 
-/// A minimal [`StaffGroup`](epiphany_core::StaffGroup) (genesis tranche G3a) —
+/// A minimal [`StaffGroup`](epiphany_core::StaffGroup) (genesis tranche G3a):
-/// the value a `CreateStaffGroup` mints: named for its counter, a grand-staff
+/// named for its counter, a grand-staff kind, and the given `members` list
-/// kind, and the given `members` list carried exactly as given (contract
+/// carried exactly as given — **this helper never normalizes `members`**, which
-/// §1.1, disposition B — this helper never normalizes `members`).
+/// is what lets a test hand a non-empty list to a refusal path.
+///
+/// **A non-empty result is no longer something `CreateStaffGroup` can mint**
+/// (P13-S16 §1.1, disposition A): reduction refuses such a value with
+/// `ContainerNotEmpty`. The helper is unchanged and deliberately so — it builds
+/// values, including ones the reducer will reject.
 pub fn staff_group(id: StaffGroupId, members: Vec<StaffId>) -> epiphany_core::StaffGroup {
     epiphany_core::StaffGroup {
         id,

crates/epiphany-testkit/src/roundtrip.rs

@@ -869,12 +869,20 @@ mod tests {
     ///
     /// # Two provably independent operands
     ///
-    /// The fixture is built with `synthetic_for_fixture(0)` and commits a base
+    /// The fixture is built with `synthetic_for_fixture(1)` and commits a base
-    /// carrying the **literal** `ReductionAlgorithmVersion(0)`; the reopen then
+    /// carrying the **literal** `ReductionAlgorithmVersion(1)`; the reopen then
     /// supplies `production_caps()`, which wraps the real constant. One operand
     /// is a literal written into a fixture, the other is the authority read at
     /// the reopen — neither derived from the other.
     ///
+    /// **The literals track the constant's value by hand.** P13-S16 moved the
+    /// authority `0` → `1`, so every literal below moved with it — by editing,
+    /// never by referencing `CURRENT_REDUCTION_ALGORITHM_VERSION`. That this
+    /// test must be edited whenever the authority moves is the **point**, not
+    /// friction to be engineered away: it is the tripwire. A future rung that
+    /// bumps the constant will see this test fail, and updating these literals
+    /// is how it acknowledges the bump.
+    ///
     /// **Round 3 caught the alternative**: if both the supplied capability and
     /// the base version descended from `CURRENT_REDUCTION_ALGORITHM_VERSION`,
     /// both would move together under M5b's mutation and the comparison would
@@ -898,7 +906,7 @@ mod tests {
             MemStore::new(),
             FileUuid([0x5E; 16]),
             Manifest::empty(DocumentId([0x5E; 16])),
-            BundleCapabilities::synthetic_for_fixture(0),
+            BundleCapabilities::synthetic_for_fixture(1),
         )
         .expect("fixture bundle creates");
 
@@ -915,7 +923,7 @@ mod tests {
                     snapshot_id: SnapshotId([0x5E; 16]),
                     covers_causal_frontier: FrontierBytes::empty(),
                     // A deliberate LITERAL — not the constant. See above.
-                    reduction_algorithm_version: ReductionAlgorithmVersion(0),
+                    reduction_algorithm_version: ReductionAlgorithmVersion(1),
                     profile_id: ProfileId::Full,
                     hash: root.hash,
                     root,
@@ -938,13 +946,13 @@ mod tests {
                         .as_ref()
                         .unwrap()
                         .reduction_algorithm_version,
-                    ReductionAlgorithmVersion(0)
+                    ReductionAlgorithmVersion(1)
                 );
             }
             Err(BundleError::CanonicalBaseRequiresRebuild { base, current }) => {
                 // Reached only under M5b. Assert both fields, then fail loudly
                 // quoting them — that is the mutation's required observation.
-                assert_eq!(base, ReductionAlgorithmVersion(0));
+                assert_eq!(base, ReductionAlgorithmVersion(1));
                 panic!(
                     "M5b observation: base={} current={} — the authority is load-bearing here",
                     base.0, current.0

crates/epiphany-textproj/src/serialize.rs

@@ -643,7 +643,7 @@ mod tests {
     /// because `epiphany-bundle` must not depend on `epiphany-ops` (pin 1, §0.3)
     /// and so no test there can reach the real authority.
     ///
-    /// # The `0` is a deliberate LITERAL, and that is load-bearing
+    /// # The `1` is a deliberate LITERAL, and that is load-bearing
     ///
     /// Comparing against `CURRENT_REDUCTION_ALGORITHM_VERSION` would compare the
     /// constant with itself laundered through one function call: mutate the
@@ -652,9 +652,11 @@ mod tests {
     /// constant** — doing so makes M5a vacuous while leaving every test green,
     /// a failure invisible to the suite (contract §7 item 4b exists to catch it).
     ///
-    /// **This test is expected to fail when P13-S16 bumps the authority**, and
+    /// **This test failed when P13-S16 bumped the authority `0` → `1`, exactly as
-    /// that is correct: the literal is a tripwire on the production wiring, and
+    /// S27 predicted it would**, and the literal below was updated by hand. That
-    /// S16 updating it is S16 stating that the authority moved.
+    /// is the tripwire working, not friction: editing this literal is how a rung
+    /// *states* that the authority moved. A future bump must break this test
+    /// again.
     #[test]
     fn serialize_document_supplies_the_real_reduction_authority() {
         let document = minimal_document(42);
@@ -662,7 +664,7 @@ mod tests {
             .expect("a base-free document serializes");
         assert_eq!(
             bundle.capabilities().current_reduction_version,
-            ReductionAlgorithmVersion(0),
+            ReductionAlgorithmVersion(1),
             "the production writer must supply the real authority, not a literal of its own"
         );
     }

spec/core_spec.tex

@@ -4232,13 +4232,16 @@ pub struct StaffGroup {
     pub id: StaffGroupId,
     pub name: Option<String>,
     pub kind: StaffGroupKind,
-    /// A non-authoritative denormalized projection of group membership
+    /// A denormalized projection of group membership, maintained from
-    /// (genesis tranche G3a, ratified disposition B, filed as P13-S16).
+    /// \texttt{Staff.group} by reduction (P13-S16, ratified disposition A;
-    /// \texttt{Staff.group} below is the sole authority: this field
+    /// supersedes genesis tranche G3a's disposition B).
-    /// \MUSTNOT{} be read to decide whether a staff is in a group, and MAY
+    /// \texttt{Staff.group} below is the sole authority; this field is
-    /// be stale in both directions --- a member missing here while
+    /// derived from it and the two \MUST{} agree in both directions, which
-    /// \texttt{Staff.group} names this group, or a staff listed here while
+    /// graph invariant~21 enforces. \texttt{CreateStaffGroup} refuses a
-    /// its own \texttt{Staff.group} is absent or names a different group.
+    /// non-empty carried \texttt{members}: membership changes only by
+    /// writing \texttt{Staff.group}. Under disposition B this field was
+    /// authored directly and MAY have been stale in both directions;
+    /// neither state is reachable now.
     pub members: Vec<StaffId>,
 }
 
@@ -5584,11 +5587,14 @@ pub struct Staff {
 
     /// Visual grouping: which staff group (if any) this staff
     /// belongs to (e.g., piano grand staff, choral group). The sole
-    /// authority for group membership (genesis tranche G3a, ratified
+    /// authority for group membership (P13-S16, ratified disposition A;
-    /// disposition B, filed as P13-S16): every consumer \MUST{} read
+    /// supersedes genesis tranche G3a's disposition B): every consumer
-    /// membership from this field, not from \texttt{StaffGroup.members}
+    /// \MUST{} read membership from this field, and writing it is the only
-    /// above, which is a non-authoritative denormalized projection that MAY
+    /// way membership changes. \texttt{StaffGroup.members} above is a
-    /// disagree with this field in either direction.
+    /// projection maintained from this field by reduction; the two \MUST{}
+    /// agree in both directions, which graph invariant~21 enforces. Under
+    /// disposition B that projection was authored directly and MAY have
+    /// disagreed with this field in either direction.
     pub group: Option<StaffGroupId>,
 }
 
@@ -6639,6 +6645,23 @@ The score graph maintains a set of structural invariants. Implementations
       \texttt{measure\_duration()}, and IS flagged when that
       distance is the pickup's own shorter length rather than a
       full bar.
+    \item (P13-S16.) \texttt{Staff.group} and
+      \texttt{StaffGroup.members} AGREE in both directions:
+      whenever a \texttt{Staff} names a \texttt{StaffGroup}, that
+      group's \texttt{members} contains the staff; and whenever a
+      group's \texttt{members} lists a staff, that staff's own
+      \texttt{group} names that group. \texttt{Staff.group} is the
+      sole authority and \texttt{members} is the projection
+      maintained from it, so a violation means the projection has
+      drifted --- a maintenance gap leaving a staff absent from
+      \texttt{members}, or a stale entry listing a staff that no
+      longer names the group. The two directions fail for different
+      reasons and are checked independently. This invariant
+      ABSTAINS on \emph{dangling} membership: a \texttt{members}
+      entry naming a staff that is not declared at all is
+      invariant~10's reference-resolution concern, not a
+      disagreement, since an absent staff has no \texttt{group} to
+      compare against.
   \end{enumerate}
 
   Implementations \MUST{} reject graph configurations that violate any
@@ -6647,14 +6670,16 @@ The score graph maintains a set of structural invariants. Implementations
   changes that restore them within the same operation.
 \end{requirement}
 
-This enumeration contains exactly \textbf{20} invariants. (Earlier
+This enumeration contains exactly \textbf{21} invariants. (Earlier
 summary material, including the QUICKSTART, referred to ``18 graph
 invariants''; a subsequent revision of this document corrected that
 to 19; genesis tranche G3b
 (\texttt{spec/CONTRACT\_GENESIS\_G3B\_MEASURE.md}) then appended a
-20th, measure-meter consistency, above --- the authoritative count is
+20th, measure-meter consistency, and P13-S16
-20, matching this enumeration and the reference implementation.)
+(\texttt{spec/CONTRACT\_P13S16\_PROJECTION.md}) a 21st, staff-group
-These 20 are
+membership agreement --- the authoritative count is 21, matching this
+enumeration and the reference implementation.)
+These 21 are
 \emph{runtime} invariants: they hold over every well-formed graph and
 are restored by compensating changes when an edit would break them.
 
@@ -7012,8 +7037,9 @@ pub enum OperationKind {
     // Genesis tranche G3a: the four remaining root-level Score entity
     // mints, on the InsertStaff set-union mint pattern. Staff.group is the
     // sole authority for group membership (see the Staff/StaffGroup
-    // declarations below); CreateStaffGroup stores members as carried and
+    // declarations below); CreateStaffGroup refuses a non-empty carried
-    // neither maintains nor trusts it.
+    // members, and the projection is maintained from Staff.group by
+    // reduction (P13-S16, disposition A).
     CreateStaffGroup(CreateStaffGroupOp),
     CreatePartDefinition(CreatePartDefinitionOp),
     CreateAnalysisLayer(CreateAnalysisLayerOp),
@@ -16897,6 +16923,27 @@ layouts they own versus inherit:
   during open is prohibited outright, because the envelopes a rebuild would
   need may have been pruned.
   \\
+  \today & \sectionsc{Top-Level Score Structure},
+  \sectionsc{Graph Invariants} & \textbf{P13-S16: \texttt{StaffGroup.members}
+  becomes a maintained projection (disposition A), superseding genesis tranche
+  G3a's disposition B, and graph invariant~21 is appended.}
+  \texttt{Staff.group} was already the sole authority for group membership, but
+  \texttt{members} was stored exactly as carried and neither maintained nor
+  trusted, so \emph{both} disagreeing states were permitted outcomes rather
+  than defects --- a sound ruling while the tranche minted only, since no
+  authoring order could repair a disagreement once made. This revision makes
+  \texttt{members} derived: \texttt{CreateStaffGroup} refuses a non-empty
+  carried \texttt{members} (\texttt{ContainerNotEmpty}, an
+  \emph{empty-container} precondition on the carried value and therefore
+  enforced base-free, unlike the sibling mints' graph-aware liveness checks),
+  \texttt{CreateStaff} carrying a group appends the staff to that group's
+  \texttt{members}, and undo of a staff strips it back out. The two \MUST{}
+  now agree in both directions, which new graph invariant~21
+  (\texttt{StaffGroupMembershipAgreement}) enforces between live objects while
+  abstaining on dangling membership --- an undeclared member is
+  invariant~10's reference-resolution concern, not a disagreement. The
+  enumeration count moves from 20 to 21 accordingly.
+  \\
   \bottomrule
 \end{longtable}
 

spec/operation_catalog.tex

@@ -442,27 +442,38 @@ staff group authorable: with mints only, and no modify or delete operation
 for either side, no authoring order can bring \texttt{Staff.group} and
 \texttt{StaffGroup.members} into agreement once they disagree.
 
-\textbf{Ruled (disposition B, filed as P13-S16): \texttt{Staff.group} is the
+\textbf{Ruled (disposition A, P13-S16; supersedes disposition B):
-sole authority for group membership; \texttt{StaffGroup.members} is a
+\texttt{Staff.group} is the sole authority for group membership, and
-non-authoritative denormalized projection.} \texttt{CreateStaffGroup} stores
+\texttt{StaffGroup.members} is a projection maintained from it by reduction.}
-\texttt{members} exactly as carried and neither maintains nor trusts it
+\texttt{CreateStaffGroup} \textbf{refuses} a non-empty carried \texttt{members}
-thereafter. Both stale forms are permitted outcomes, not defects: a
+(\texttt{ContainerNotEmpty}) --- the operation authors the group, not its
-\textbf{missing} member (\texttt{Staff.group} names a group whose
+membership --- and \texttt{CreateStaff} carrying \texttt{group: Some(g)}
-\texttt{members} omits that staff) and a \textbf{spurious} member
+appends the new staff to \texttt{g}'s \texttt{members} in the graph. The two
-(\texttt{StaffGroup.members} names a staff whose own \texttt{Staff.group} is
+\MUST{} agree in both directions, and graph invariant~21 (core specification
-absent or names a different group). Every consumer \MUST{} read group
+\sectionsc{Graph Invariants}) flags any disagreement between live objects.
-membership from \texttt{Staff.group} only; core specification Chapter~5's
+Every consumer \MUST{} read group membership from \texttt{Staff.group}; core
-\texttt{Staff}/\texttt{StaffGroup} declarations (\sectionsc{Top-Level Score
+specification Chapter~5's \texttt{Staff}/\texttt{StaffGroup} declarations
-Structure}) now state this normatively, and Section~\ref{sec:k0:create-staff}
+(\sectionsc{Top-Level Score Structure}) state this normatively, and
-above states the corresponding authoring-order consequence for
+Section~\ref{sec:k0:create-staff} above states the corresponding
-\texttt{CreateStaff}. Disposition A (maintaining \texttt{members} by
+authoring-order consequence for \texttt{CreateStaff}.
-reduction, making it a derived field) remains the later
+
-maintenance/enforcement fix, sequenced after G3b.
+\textbf{What disposition B ruled, and why it no longer holds.} Genesis tranche
+G3a ratified disposition B: \texttt{members} was stored exactly as carried and
+\textbf{neither maintained nor trusted}, and \textbf{both} stale forms were
+permitted outcomes rather than defects --- a \textbf{missing} member
+(\texttt{Staff.group} naming a group whose \texttt{members} omits that staff)
+and a \textbf{spurious} member (\texttt{StaffGroup.members} naming a staff
+whose own \texttt{Staff.group} is absent or names a different group). That
+ruling was sound while the tranche minted only: with no modify or delete
+operation for either side, no authoring order could bring the two into
+agreement once they disagreed. Disposition A was recorded there as the later
+maintenance/enforcement fix, sequenced after G3b; \textbf{P13-S16 is that
+fix}, and neither stale form is authorable any more.
 
 \textbf{Referential preconditions, graph-aware only, mirroring
-\texttt{CreateStaff} exactly.} \texttt{CreateStaffGroup.members} and
+\texttt{CreateStaff} exactly.} \texttt{CreatePartDefinition.staves}
-\texttt{CreatePartDefinition.staves} each precondition every named id
+preconditions every named id resolves to a live \texttt{Staff};
-resolves to a live \texttt{Staff}; \texttt{CreateView.active\_layers}
+\texttt{CreateView.active\_layers}
 preconditions every named id resolves to a live analysis layer;
 \texttt{CreateAnalysisLayer} carries no outbound reference and needs no
 referential precondition at all, the \texttt{CreateInstrument} shape rather
@@ -471,6 +482,16 @@ these, exactly as for \texttt{CreateStaff}: there is no universe to check
 against. No new \texttt{PreconditionFailureReason} --- every referential
 refusal reuses \texttt{TargetMissing} (discriminant 0).
 
+\textbf{\texttt{CreateStaffGroup} is deliberately not in that list (P13-S16).}
+Its \texttt{members} check is an \textbf{empty-container} precondition on the
+carried value, not a referential one, and the distinction is normative: a
+graph-aware precondition asks about the \emph{universe} (``is this id live?'')
+and therefore cannot run base-free, whereas an empty-container precondition asks
+only about the \emph{carried value} (``is \texttt{members} empty?'') and
+therefore \MUST{} be enforced everywhere, base-free included. It refuses with
+\texttt{ContainerNotEmpty}, and the sentence above about base-free reduction
+enforcing none of these does \textbf{not} extend to it.
+
 No accept-set change: all four carried types have exactly one wire layout
 (core specification's \sectionsc{Binary Format Companion} confirms no
 versioned walk exists for any of the four), so none gains a
@@ -542,6 +563,63 @@ successor is refused the identical way. Closing this needs a per-measure
 duration concept this rung does not introduce
 (\texttt{spec/PASS13\_CANDIDATES.md}, P13-S19, still open).
 
+\medskip
+
+\noindent\textbf{Version 0.15.0 (P13-S16, the maintained projection,
+\texttt{spec/CONTRACT\_P13S16\_PROJECTION.md}).} No payload byte changes ---
+\texttt{CreateStaffGroupOp} and \texttt{CreateStaffOp} encode exactly as in
+0.12.0 --- but a \textbf{behaviour change on two operations}, replacing genesis
+tranche G3a's ratified \textbf{disposition~B} with \textbf{disposition~A}.
+\texttt{StaffGroup.members} stops being a non-authoritative field stored as
+carried and becomes a projection \emph{maintained} from \texttt{Staff.group}:
+
+\begin{itemize}[leftmargin=1.2em]
+  \item \texttt{CreateStaffGroup} (Section~\ref{sec:k0:create-staff-group})
+    now \textbf{refuses} a non-empty carried \texttt{members} with
+    \texttt{ContainerNotEmpty} (discriminant~10, no new
+    \texttt{PreconditionFailureReason}). This \textbf{replaces} the
+    graph-aware precondition that every id in \texttt{members} resolve to a
+    live \texttt{Staff} (\texttt{TargetMissing}). The new check is an
+    \emph{empty-container} precondition on the carried value, so unlike the
+    check it replaces it is \textbf{not graph-gated and is enforced base-free}
+    --- the one place where the sibling mints' ``referential preconditions are
+    graph-aware only'' rule does not extend.
+  \item \texttt{CreateStaff} (Section~\ref{sec:k0:create-staff}) carrying
+    \texttt{group: Some(g)} now appends the minted staff to \texttt{g}'s
+    \texttt{members} in the graph, idempotently per staff id. Undo of a staff
+    strips the id back out.
+\end{itemize}
+
+\noindent Both formerly \textbf{permitted} stale forms --- the missing member
+and the spurious member --- are therefore \textbf{unauthorable}, and the core
+specification gains graph invariant~21
+(\texttt{StaffGroupMembershipAgreement}) requiring the two to agree in both
+directions between live objects, abstaining on dangling membership because an
+undeclared member is invariant~10's concern.
+
+\textbf{This breaks documents authored under 0.12.0--0.14.0 only in what they
+may newly assert}, not in what they may read: an existing blob carrying a
+disagreeing pair still decodes, and no stored bytes are reinterpreted.
+
+\textbf{A canonical base materialized before this rung \MUST{} be rebuilt rather
+than reused}, and the two operations oblige that for \emph{different} reasons,
+either of which alone would suffice:
+
+\begin{itemize}[leftmargin=1.2em]
+  \item \texttt{CreateStaffGroup} changes its \textbf{reduction verdict} --- a
+    non-empty carried \texttt{members} now reduces to a no-op where it
+    previously applied, so the recorded effect differs.
+  \item \texttt{CreateStaff} changes \textbf{canonical reduced state} --- its
+    verdict is unchanged (it still applies), but the graph the reduction
+    produces now carries the maintained \texttt{members}.
+\end{itemize}
+
+\noindent Accordingly
+\texttt{epiphany\_ops::CURRENT\_REDUCTION\_ALGORITHM\_VERSION} moves
+\texttt{0}~$\rightarrow$~\texttt{1}, and P13-S27's authority check refuses a
+base declaring the older version. Core specification \sectionsc{Canonical
+Document Identity} requires the bump for either class of change.
+
 % ===========================================================================
 \chapter{The Catalog Framework}
 \label{ch:framework}
@@ -1262,20 +1340,29 @@ With staves mintable, \texttt{CreateStaffInstance}
 instance's referenced \texttt{Staff} is live (previously the reference was
 satisfiable only from the seeded base, so the check was vacuous).
 
-\textbf{Stale-form semantics (genesis tranche G3a, disposition B, filed as
+\textbf{Membership maintenance (P13-S16, disposition A; supersedes genesis
-P13-S16).} \texttt{Staff.group} is the \textbf{sole authority} for group
+tranche G3a's disposition B).} \texttt{Staff.group} is the \textbf{sole
-membership; \texttt{StaffGroup.members}
+authority} for group membership, and \texttt{StaffGroup.members}
-(Section~\ref{sec:k0:create-staff-group}) is a non-authoritative denormalized
+(Section~\ref{sec:k0:create-staff-group}) is a projection \textbf{maintained
-projection no consumer may read to decide membership. \texttt{CreateStaff}
+from it} under graph-aware reduction. \texttt{CreateStaff} carrying
-is the operation that authors the \textbf{missing-member} stale form: a
+\texttt{group: Some(g)} therefore appends the newly minted staff to \texttt{g}'s
+\texttt{members} in the graph. The append is set-union and idempotent per staff
+id --- convergence replays operations, so appending an id already present
+\MUSTNOT{} duplicate it --- and base-free reduction has no graph to maintain and
+writes nothing. The two \MUST{} agree in both directions, and graph
+invariant~21 (core specification \sectionsc{Graph Invariants}) flags any
+disagreement between live objects.
+
+\textbf{What this replaced.} Under disposition B, \texttt{CreateStaff} authored
+a \textbf{permitted} \textbf{missing-member} stale form: a
 \texttt{CreateStaffGroup(g, members: [])} followed by a
-\texttt{CreateStaff(s, group: Some(g))} leaves \texttt{s.group == Some(g)}
+\texttt{CreateStaff(s, group: Some(g))} left \texttt{s.group == Some(g)} while
-while \texttt{g.members} omits \texttt{s} --- a \textbf{permitted} outcome,
+\texttt{g.members} omitted \texttt{s}, because that tranche minted only and no
-not a defect, since G3a mints only and no operation maintains
+operation maintained the projection. \textbf{That outcome is no longer
-\texttt{StaffGroup.members} by reduction. The mirror-image \textbf{spurious}
+reachable}: the identical sequence now yields agreement. The mirror-image
-form (a staff named in \texttt{members} whose own \texttt{group} is absent or
+\textbf{spurious} form is likewise unauthorable --- \texttt{CreateStaffGroup}
-different) is authored by \texttt{CreateStaffGroup} instead; see
+refuses a non-empty carried \texttt{members} outright; see
-Section~\ref{sec:k0:create-staff-group}'s own stale-form paragraph.
+Section~\ref{sec:k0:create-staff-group}.
 
 \textbf{Conflict cases.} None at reduction time (set-union; the differing-value
 re-create is a precondition gate, not a conflict).
@@ -1283,6 +1370,14 @@ re-create is a precondition gate, not a conflict).
 \textbf{Undo semantics.} Undo of a create tombstones the minted staff
 (Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if a live staff
 instance references it (tombstoning it would strand the instance).
+\textbf{Undo also strips the removed staff's id from every live group's
+\texttt{members} (P13-S16)}: the projection is maintained from
+\texttt{Staff.group}, so a staff leaving the graph \MUST{} leave the projection
+with it. Without that strip the undo would leave a group naming a staff that no
+longer exists. Note this is the \emph{unguarded} direction of the pair --- undo
+of a \texttt{CreateStaffGroup} is refused while a live staff still names the
+group (Section~\ref{sec:k0:create-staff-group}), but nothing refuses undoing the
+staff itself.
 
 \textbf{Re-anchoring.} Not applicable (a staff mint references no tombstonable
 anchor; there is no \texttt{DeleteStaff} in this catalogue revision --- an
@@ -1519,23 +1614,43 @@ carrying a byte-identical value reduces idempotently
 (\texttt{NoOpReason::AlreadyApplied}); a create whose id is already live with
 a differing value is a precondition no-op with \texttt{RecreateContentMismatch};
 a create naming a tombstoned id is a precondition no-op with
-\texttt{TargetTombstoned}. Graph-aware reduction additionally preconditions
+\texttt{TargetTombstoned}.
-that every id in \texttt{members} resolves to a live \texttt{Staff} ---
-reusing \texttt{TargetMissing} (discriminant 0), no new
-\texttt{PreconditionFailureReason} --- and is skipped entirely base-free,
-which has no staff universe to check against.
 
-\textbf{Stale-form semantics (disposition B, filed as P13-S16).}
+\textbf{A non-empty carried \texttt{members} is refused (P13-S16).} This
-\texttt{Staff.group} (Section~\ref{sec:k0:create-staff}) is the \textbf{sole
+operation authors the group, not its membership, so reduction preconditions that
-authority} for group membership; \texttt{members} here is a
+the carried \texttt{members} is \textbf{empty}, refusing with
-\textbf{non-authoritative denormalized projection}, stored exactly as carried
+\texttt{ContainerNotEmpty} (discriminant 10) --- no new
-and \textbf{neither maintained nor trusted} by any subsequent reduction. This
+\texttt{PreconditionFailureReason}. \textbf{This precondition is not
-operation authors the \textbf{spurious-member} stale form: a
+graph-gated}: it asks only about the carried value, so unlike the sibling mints'
+member-liveness checks it holds \textbf{base-free as well}. Membership is
+maintained from \texttt{Staff.group} instead
+(Section~\ref{sec:k0:create-staff}).
+
+\textbf{This replaced a graph-aware liveness precondition.} Under disposition B
+this operation accepted a carried \texttt{members} and graph-aware reduction
+additionally preconditioned that every id in it resolved to a live
+\texttt{Staff}, reusing \texttt{TargetMissing} (discriminant 0) and skipped
+entirely base-free. Both halves are gone: liveness is never consulted, because
+the container must be empty before the question could arise.
+
+\textbf{Membership maintenance (P13-S16, disposition A; supersedes disposition
+B).} \texttt{Staff.group} (Section~\ref{sec:k0:create-staff}) is the
+\textbf{sole authority} for group membership, and \texttt{members} here is a
+projection \textbf{maintained from it} by reduction. The two \MUST{} agree in
+both directions; graph invariant~21 (core specification \sectionsc{Graph
+Invariants}) flags any disagreement between live objects, and no consumer may
+read \texttt{members} to decide membership in preference to
+\texttt{Staff.group}.
+
+\textbf{What this replaced.} Under disposition B, \texttt{members} was stored
+exactly as carried and \textbf{neither maintained nor trusted}, and this
+operation authored a \textbf{permitted spurious-member} stale form: a
 \texttt{CreateStaff(s, group: None)} followed by
-\texttt{CreateStaffGroup(g, members: [s])} leaves \texttt{g.members == [s]}
+\texttt{CreateStaffGroup(g, members: [s])} left \texttt{g.members == [s]} while
-while \texttt{s.group} stays \texttt{None} (or names a different group) ---
+\texttt{s.group} stayed \texttt{None} (or named a different group).
-a \textbf{permitted} outcome, not a defect. No consumer may read
+\textbf{That sequence now refuses} the second operation with
-\texttt{members} to decide whether a staff belongs to a group.
+\texttt{ContainerNotEmpty}, minting no group at all, so the form is
+unauthorable rather than merely discouraged.
 
 \textbf{Conflict cases.} None at reduction time (set-union; the differing-value
 re-create is a precondition gate, not a conflict).