P13-S3: the engraved spelling set is a shared undo key, not the transpose's

My design note was half right, and the audit caught the other half. Keeping
engraved_spelling_chain physically separate from respell_chain was correct --
respell_chain is RespellPitch's LWW working state, read by its
concurrent-differing conflict detection, and folding transposes into it would
make a concurrent respell conflict with a transpose and move the canonical
bytes of every existing history. What that did NOT license was letting one
operation own the key.

RespellPitch mutates the same graph attachments and recorded nowhere on the
attachment chain, so a chain with a single writer was wrong both ways. Both
reproduced:

  respell -> [tx: transpose] -> StrictInverse undo
      Applied; pitch restored to C4; the UserChosen(C) attachment ERASED.
      The respell was an operation, not part of the base, so the transpose's
      chain had never seen it and its predecessor was absence.

  [tx: transpose] -> respell -> StrictInverse undo
      Applied; the newer UserChosen(D) authoring WIPED. The respell was
      invisible to the chain, so it never registered as a superseding writer,
      contradicting the catalog's rule that a later canonical writer supersedes
      a strict undo.

And BestEffort could restore the pre-transpose pitch while leaving a spelling
authored against the transposed one attached to it.

Fix: every writer of the attachments records on the attachment chain
(record_engraved_spellings), and a pitch's value and its engraved spelling set
undo as one unit -- if either half is superseded, neither is restored.
StrictInverse already refuses on any supersession, so the coupling only bites
for BestEffort. Two physical chains, two responsibilities: respell_chain owns
the ledger spelling and the LWW verdict, engraved_spelling_chain owns the graph
attachments.

Recording is gated on graph presence, so base-free reduction is byte-unchanged
and the seeded corpus's canonical-base digest does not move.

Four tests, two mutations verified: removing the respell's record fails all
three undo tests; removing the coupling fails the best-effort one with the
pitch back at C4 and its spelling still at C-sharp. The fourth test locks
convergence -- both permutations of a concurrent respell/transpose reduce to
identical canonical bytes.

Spec: new req:opcat:spelling-set-chain. Batch 3 of the Pass-13 ledger reopens
(P13-S1, S2 open; S3 resolved here).

Also: PitchSpelling::transposed's doc said B-sharp 3 becomes F-double-sharp 3.
The code, spec, and tests all correctly produce F-double-sharp 4 -- B to F
carries the octave. Doc only.

Gate: fmt clean, clippy 0, 30 targets / 998 passed / 0 failed, docs 0 under
-D warnings, conformance 8/8, zero golden churn, canonical-base digest unmoved.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

crates/epiphany-core/src/pitch.rs

@@ -770,7 +770,8 @@ impl PitchSpelling {
     /// [`Pitch::twelve_tet_semitone`].
     ///
     /// So B♯3 (sounding C4) transposed by a perfect fifth `(4, 7)` becomes
-    /// F×3 (sounding G4): the letter moved four diatonic steps, and the
+    /// F×4 (sounding G4): the letter moved four diatonic steps — B→F carries
+    /// the octave — and the
     /// double-sharp is what F needs to sound a G. The chromatic component never
     /// touches the spelling directly; it reaches it only through the pitch.
     ///

crates/epiphany-ops/DECISIONS.md

@@ -1393,3 +1393,46 @@ every existing history.
 - My own mutation harness restored the file between two tests, so the second
   ran unmutated and "passed". A mutation that no-ops looks exactly like a test
   that passes — the trap recorded after Push 4a, hit again in a new form.
+
+## P13-S3 — a shared undo key with one writer (2026-07-09)
+
+The `engraved_spelling_chain` added to make `TransposeInterval` undoable was
+written only by the transpose. But `RespellPitch` mutates the same graph
+attachments, and a chain with one writer is wrong in **both** directions:
+
+- **Prior respell erased.** `respell → [tx: transpose] → StrictInverse undo`
+  returned `Applied`, restored the pitch to C4, and removed *every* attachment.
+  The respell was an operation, not part of the base, so it existed only as a
+  chain write — and the transpose's chain had never seen it, so its predecessor
+  was absence.
+- **Later respell wiped.** `[tx: transpose] → respell → StrictInverse undo`
+  returned `Applied` and erased the newer authoring, because the respell was
+  invisible to the chain and so did not register as a superseding writer. The
+  catalog's general rule is that a later canonical writer supersedes a strict
+  undo.
+- **Best-effort split the unit.** With the spelling set superseded but the pitch
+  value not, `BestEffort` restored the pre-transpose pitch and left a spelling
+  authored against the transposed one attached to it.
+
+**Fix.** Both operations record on the shared key (`record_engraved_spellings`),
+and the pitch value and its spelling set undo as one unit: if either half is
+superseded, neither is restored. `StrictInverse` already refuses on any
+supersession, so the coupling only bites for `BestEffort`.
+
+**The physical separation stands, and my earlier note was only half right.** I
+kept `engraved_spelling_chain` distinct from `respell_chain` because the latter
+is `RespellPitch`'s LWW working state, read by its concurrent-differing conflict
+detection — folding transposes in would make a concurrent respell *conflict* with
+a transpose and would move the canonical bytes of every existing history. That
+reasoning holds. What it did **not** license was letting one operation own the
+key. Two physical chains, two responsibilities (`respell_chain`: the ledger
+spelling and the LWW verdict; `engraved_spelling_chain`: the graph attachments),
+but *every* writer of the attachments records on the attachment chain.
+
+Recording is gated on `self.graph.is_some()`, so base-free reduction is
+byte-unchanged and the seeded fuzz corpus's canonical-base digest does not move.
+
+Spec: `req:opcat:spelling-set-chain`. Mutation-verified: removing the respell's
+record fails all three new tests; removing the coupling fails the best-effort
+one with the pitch back at C4 and the spelling still at C-sharp. Also covered:
+both permutations of a concurrent respell/transpose reduce to identical bytes.

crates/epiphany-ops/src/reduce.rs

@@ -773,7 +773,7 @@ enum ValueRestoration {
     /// The engraved-layer explicit spelling attachments a `TransposeInterval`
     /// rewrote, restored as a set. `None` predecessor means the pitch carried
     /// none before, so they are removed.
-    TransposedSpellings {
+    EngravedSpellings {
         pitch: PitchId,
         predecessor: Option<Predecessor<Vec<SpellingAttachment>>>,
     },
@@ -874,18 +874,25 @@ struct Reducer<'a> {
     // what value-restoring undo walks. Advisory families (metadata, breaks,
     // staff layout) keep chains for undo but record no conflicts.
     respell_chain: BTreeMap<PitchId, WriteChain<PitchSpelling>>,
-    /// The engraved-layer, pitch-scoped, explicit spelling attachments a
-    /// `TransposeInterval` rewrites (`req:opcat:transpose-interval-spelling`):
-    /// the moved authored ones and the propagated one, as a single per-pitch
-    /// value so undo restores them together.
+    /// A pitch's engraved-layer, pitch-scoped, explicit spelling attachment
+    /// **set**, as one value. Written by *every* operation that changes it:
+    /// `RespellPitch` and `TransposeInterval` alike (P13-S3).
     ///
-    /// Deliberately NOT `respell_chain`. `RespellPitch` owns that chain, and
-    /// its last write is the LWW working state its concurrent-differing
-    /// conflict detection reads; folding transposes into it would make a
-    /// concurrent respell conflict with a transpose and would move the
-    /// canonical bytes of every existing history. A transpose that also moves a
-    /// `UserChosen` spelling is restored from here.
-    transposed_spelling_chain: BTreeMap<PitchId, WriteChain<Vec<SpellingAttachment>>>,
+    /// Both must record here or undo is wrong in both directions. If only the
+    /// transpose recorded, a prior respell would not be its chain-predecessor
+    /// and undoing the transpose would erase the respell; and a *later* respell
+    /// would be invisible, so a strict undo would report `Applied` and wipe it
+    /// instead of refusing as superseded.
+    ///
+    /// This is a *second* physical chain, not a replacement for `respell_chain`:
+    /// that one is `RespellPitch`'s LWW working state, read by its
+    /// concurrent-differing conflict detection, and folding transposes into it
+    /// would make a concurrent respell conflict with a transpose and move the
+    /// canonical bytes of every existing history. This chain owns the *graph
+    /// attachments*; `respell_chain` owns the *ledger spelling* and the LWW
+    /// verdict. Only ever written when a graph is present, so base-free
+    /// reduction is byte-unchanged.
+    engraved_spelling_chain: BTreeMap<PitchId, WriteChain<Vec<SpellingAttachment>>>,
     event_modify_chain: BTreeMap<EventId, WriteChain<Event>>,
     pitch_modify_chain: BTreeMap<PitchId, WriteChain<Pitch>>,
     cross_cutting_modify_chain: BTreeMap<TypedObjectId, WriteChain<CrossCuttingValue>>,
@@ -964,18 +971,25 @@ struct WorkingSnapshot {
     event_pitches: BTreeMap<EventId, Vec<PitchId>>,
     voice_occupancy: BTreeMap<VoiceId, Vec<(MusicalPosition, MusicalDuration, EventId)>>,
     respell_chain: BTreeMap<PitchId, WriteChain<PitchSpelling>>,
-    /// The engraved-layer, pitch-scoped, explicit spelling attachments a
-    /// `TransposeInterval` rewrites (`req:opcat:transpose-interval-spelling`):
-    /// the moved authored ones and the propagated one, as a single per-pitch
-    /// value so undo restores them together.
+    /// A pitch's engraved-layer, pitch-scoped, explicit spelling attachment
+    /// **set**, as one value. Written by *every* operation that changes it:
+    /// `RespellPitch` and `TransposeInterval` alike (P13-S3).
     ///
-    /// Deliberately NOT `respell_chain`. `RespellPitch` owns that chain, and
-    /// its last write is the LWW working state its concurrent-differing
-    /// conflict detection reads; folding transposes into it would make a
-    /// concurrent respell conflict with a transpose and would move the
-    /// canonical bytes of every existing history. A transpose that also moves a
-    /// `UserChosen` spelling is restored from here.
-    transposed_spelling_chain: BTreeMap<PitchId, WriteChain<Vec<SpellingAttachment>>>,
+    /// Both must record here or undo is wrong in both directions. If only the
+    /// transpose recorded, a prior respell would not be its chain-predecessor
+    /// and undoing the transpose would erase the respell; and a *later* respell
+    /// would be invisible, so a strict undo would report `Applied` and wipe it
+    /// instead of refusing as superseded.
+    ///
+    /// This is a *second* physical chain, not a replacement for `respell_chain`:
+    /// that one is `RespellPitch`'s LWW working state, read by its
+    /// concurrent-differing conflict detection, and folding transposes into it
+    /// would make a concurrent respell conflict with a transpose and move the
+    /// canonical bytes of every existing history. This chain owns the *graph
+    /// attachments*; `respell_chain` owns the *ledger spelling* and the LWW
+    /// verdict. Only ever written when a graph is present, so base-free
+    /// reduction is byte-unchanged.
+    engraved_spelling_chain: BTreeMap<PitchId, WriteChain<Vec<SpellingAttachment>>>,
     event_modify_chain: BTreeMap<EventId, WriteChain<Event>>,
     pitch_modify_chain: BTreeMap<PitchId, WriteChain<Pitch>>,
     cross_cutting_modify_chain: BTreeMap<TypedObjectId, WriteChain<CrossCuttingValue>>,
@@ -1254,7 +1268,7 @@ impl<'a> Reducer<'a> {
             event_pitches: BTreeMap::new(),
             voice_occupancy: BTreeMap::new(),
             respell_chain: BTreeMap::new(),
-            transposed_spelling_chain: BTreeMap::new(),
+            engraved_spelling_chain: BTreeMap::new(),
             event_modify_chain: BTreeMap::new(),
             pitch_modify_chain: BTreeMap::new(),
             cross_cutting_modify_chain: BTreeMap::new(),
@@ -1668,7 +1682,7 @@ impl<'a> Reducer<'a> {
             }
         }
         for (pitch, set) in by_pitch {
-            self.transposed_spelling_chain
+            self.engraved_spelling_chain
                 .entry(pitch)
                 .or_insert_with(WriteChain::new)
                 .seed(set);
@@ -3185,6 +3199,27 @@ impl<'a> Reducer<'a> {
             .or_insert_with(WriteChain::new)
             .record(env.id, env.transaction, op.spelling.clone());
         self.graph_respell_pitch(op.pitch, &op.spelling);
+        // A respell changes the graph attachment set, so it is a writer on
+        // `engraved_spelling_chain` too (P13-S3). Without this, a transpose
+        // undone after a respell would erase it, and a respell landing after a
+        // transposed transaction would be silently wiped by that undo instead
+        // of superseding it.
+        self.record_engraved_spellings(env, op.pitch);
+    }
+
+    /// Records `pitch`'s current graph attachment set as a write on
+    /// [`Self::engraved_spelling_chain`]. A no-op under base-free reduction,
+    /// which has no graph attachments to own — so base-free canonical bytes do
+    /// not move.
+    fn record_engraved_spellings(&mut self, env: &OperationEnvelope, pitch: PitchId) {
+        if self.graph.is_none() {
+            return;
+        }
+        let set = self.graph_spelling_set(pitch);
+        self.engraved_spelling_chain
+            .entry(pitch)
+            .or_insert_with(WriteChain::new)
+            .record(env.id, env.transaction, set);
     }
 
     fn graph_respell_pitch(&mut self, pitch: PitchId, spelling: &PitchSpelling) {
@@ -4894,6 +4929,14 @@ impl<'a> Reducer<'a> {
     ) -> (Vec<ValueRestoration>, Vec<OperationId>) {
         let mut restorations = Vec::new();
         let mut superseded: Vec<OperationId> = Vec::new();
+        // A `TransposeInterval` writes a pitch's value and its engraved spelling
+        // set as one act, so they undo as one unit (P13-S3). If either half was
+        // superseded, neither is restored: `BestEffort` must not put the pitch
+        // back while leaving a spelling written for the pitch it used to be.
+        // (`StrictInverse` refuses outright on any supersession, so this only
+        // bites for `BestEffort`.)
+        let mut superseded_pitches: std::collections::BTreeSet<PitchId> =
+            std::collections::BTreeSet::new();
         let slot_live = |obj: TypedObjectId| {
             matches!(self.objects.get(&obj), Some(ObjectState::Live)) && !targets.contains(&obj)
         };
@@ -4919,7 +4962,10 @@ impl<'a> Reducer<'a> {
             }
             match chain.undo_verdict(tx) {
                 ChainUndoVerdict::NotWritten => {}
-                ChainUndoVerdict::Superseded { by } => superseded.push(by),
+                ChainUndoVerdict::Superseded { by } => {
+                    superseded.push(by);
+                    superseded_pitches.insert(*pitch);
+                }
                 ChainUndoVerdict::Restore(predecessor) => {
                     restorations.push(ValueRestoration::Pitch {
                         pitch: *pitch,
@@ -4943,15 +4989,18 @@ impl<'a> Reducer<'a> {
                 }
             }
         }
-        for (pitch, chain) in &self.transposed_spelling_chain {
+        for (pitch, chain) in &self.engraved_spelling_chain {
             if !slot_live(TypedObjectId::Pitch(*pitch)) {
                 continue;
             }
             match chain.undo_verdict(tx) {
                 ChainUndoVerdict::NotWritten => {}
-                ChainUndoVerdict::Superseded { by } => superseded.push(by),
+                ChainUndoVerdict::Superseded { by } => {
+                    superseded.push(by);
+                    superseded_pitches.insert(*pitch);
+                }
                 ChainUndoVerdict::Restore(predecessor) => {
-                    restorations.push(ValueRestoration::TransposedSpellings {
+                    restorations.push(ValueRestoration::EngravedSpellings {
                         pitch: *pitch,
                         predecessor,
                     })
@@ -5090,6 +5139,20 @@ impl<'a> Reducer<'a> {
                 }
             }
         }
+        // Couple the two halves a transpose writes together. Dropping a `Pitch`
+        // restoration whose spelling set was superseded (and vice versa) is what
+        // makes them one undo unit. It cannot mis-fire on an unrelated operation:
+        // a chain reports `Superseded` only when the transaction actually wrote
+        // it, and `ModifyIdentifiedPitch` never writes the spelling set.
+        if !superseded_pitches.is_empty() {
+            restorations.retain(|r| match r {
+                ValueRestoration::Pitch { pitch, .. }
+                | ValueRestoration::EngravedSpellings { pitch, .. } => {
+                    !superseded_pitches.contains(pitch)
+                }
+                _ => true,
+            });
+        }
         superseded.sort();
         superseded.dedup();
         (restorations, superseded)
@@ -5148,12 +5211,12 @@ impl<'a> Reducer<'a> {
                         self.graph_remove_respell(pitch);
                     }
                 },
-                ValueRestoration::TransposedSpellings { pitch, predecessor } => {
+                ValueRestoration::EngravedSpellings { pitch, predecessor } => {
                     let set: Vec<SpellingAttachment> = match predecessor {
                         Some(Predecessor::Write(set)) | Some(Predecessor::Base(set)) => set,
                         None => Vec::new(),
                     };
-                    self.transposed_spelling_chain
+                    self.engraved_spelling_chain
                         .entry(pitch)
                         .or_insert_with(WriteChain::new)
                         .record(env.id, env.transaction, set.clone());
@@ -5798,11 +5861,7 @@ impl<'a> Reducer<'a> {
                 .entry(r.pitch)
                 .or_insert_with(WriteChain::new)
                 .record(env.id, env.transaction, r.value.clone());
-            let set = self.graph_spelling_set(r.pitch);
-            self.transposed_spelling_chain
-                .entry(r.pitch)
-                .or_insert_with(WriteChain::new)
-                .record(env.id, env.transaction, set);
+            self.record_engraved_spellings(env, r.pitch);
         }
         OperationEffect::Applied
     }
@@ -7137,7 +7196,7 @@ impl<'a> Reducer<'a> {
             event_pitches: self.event_pitches.clone(),
             voice_occupancy: self.voice_occupancy.clone(),
             respell_chain: self.respell_chain.clone(),
-            transposed_spelling_chain: self.transposed_spelling_chain.clone(),
+            engraved_spelling_chain: self.engraved_spelling_chain.clone(),
             event_modify_chain: self.event_modify_chain.clone(),
             pitch_modify_chain: self.pitch_modify_chain.clone(),
             cross_cutting_modify_chain: self.cross_cutting_modify_chain.clone(),
@@ -7173,7 +7232,7 @@ impl<'a> Reducer<'a> {
         self.event_pitches = s.event_pitches;
         self.voice_occupancy = s.voice_occupancy;
         self.respell_chain = s.respell_chain;
-        self.transposed_spelling_chain = s.transposed_spelling_chain;
+        self.engraved_spelling_chain = s.engraved_spelling_chain;
         self.event_modify_chain = s.event_modify_chain;
         self.pitch_modify_chain = s.pitch_modify_chain;
         self.cross_cutting_modify_chain = s.cross_cutting_modify_chain;
@@ -9662,6 +9721,222 @@ mod tests {
         );
     }
 
+    // --- P13-S3: RespellPitch and TransposeInterval share the engraved
+    // spelling set, so undo must see both. ---------------------------------
+
+    fn respell_env(
+        replica: u64,
+        counter: u64,
+        physical: i64,
+        ctx: CausalContext,
+        pitch: PitchId,
+        nominal: CmnNominal,
+    ) -> OperationEnvelope {
+        prim_env(
+            replica,
+            counter,
+            physical,
+            ctx,
+            OperationKind::RespellPitch(RespellPitchOp {
+                pitch,
+                spelling: PitchSpelling::cmn(nominal, 4),
+            }),
+        )
+    }
+
+    fn transpose_member(
+        replica: u64,
+        counter: u64,
+        physical: i64,
+        ctx: CausalContext,
+        tx: TransactionId,
+        pitch: PitchId,
+        iv: TranspositionInterval,
+    ) -> OperationEnvelope {
+        tx_member(
+            replica,
+            counter,
+            physical,
+            ctx,
+            tx,
+            OperationKind::TransposeInterval(TransposeIntervalOp {
+                targets: [pitch].into_iter().collect(),
+                interval: iv,
+            }),
+        )
+    }
+
+    /// `(source, nominal, accidental count)` of every engraved-layer explicit
+    /// attachment on `pitch`.
+    fn attachments_of(score: &Score, pitch: PitchId) -> Vec<(SpellingSource, CmnNominal, usize)> {
+        score
+            .spelling_attachments
+            .iter()
+            .filter(|a| a.layer.is_none())
+            .filter(|a| matches!(&a.scope, SpellingScope::Pitch(p) if *p == pitch))
+            .filter_map(|a| match (&a.directive, &a.source) {
+                (SpellingDirective::Explicit(sp), src) => match sp.nominal {
+                    epiphany_core::SpellingNominal::Cmn(n) => {
+                        Some((src.clone(), n, sp.accidentals.len()))
+                    }
+                    _ => None,
+                },
+                _ => None,
+            })
+            .collect()
+    }
+
+    fn undo_effect(state: &MaterializedState, id: OperationId) -> OperationEffect {
+        state
+            .effects
+            .iter()
+            .find(|(e, _)| *e == id)
+            .map(|(_, eff)| eff.clone())
+            .expect("effect recorded")
+    }
+
+    #[test]
+    fn undoing_a_transpose_restores_a_prior_respell() {
+        // P13-S3, direction one. The respell is an OPERATION, not part of the
+        // base, so it exists only as a write on the shared chain. Before the
+        // fix, the transpose's chain had no predecessor for it and the undo
+        // wiped every attachment on the pitch.
+        let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
+        let tx = TransactionId::new(ReplicaId(1), 900);
+        let undo = undo_env(1, 3, 13, seen_r1(2), tx, UndoPolicy::StrictInverse);
+        let undo_id = undo.id;
+
+        let mut set = OperationSet::new();
+        set.accept_all(vec![
+            respell_env(1, 0, 10, CausalContext::new(), pid, CmnNominal::C),
+            declare_transaction(1, 1, 11, seen_r1(0), tx),
+            transpose_member(1, 2, 12, seen_r1(1), tx, pid, interval(0, 1)),
+            undo,
+        ]);
+        let out = set.reduce_onto(&base);
+
+        assert_eq!(undo_effect(&out.state, undo_id), OperationEffect::Applied);
+        assert_eq!(cmn_of(&pitch_of(&out.score, pid)), (CmnNominal::C, 0, 4));
+        assert_eq!(
+            attachments_of(&out.score, pid),
+            vec![(SpellingSource::UserChosen, CmnNominal::C, 0)],
+            "the prior respell survives the undo, and the propagated one is gone"
+        );
+    }
+
+    #[test]
+    fn a_respell_after_a_transposed_transaction_supersedes_its_strict_undo() {
+        // P13-S3, direction two. The respell lands canonically AFTER the
+        // transaction, so it is a later writer on the pitch's spelling set:
+        // strict undo must refuse rather than erase it. Before the fix the
+        // respell was invisible to the transpose's chain, so the undo reported
+        // Applied and wiped the newer authoring.
+        let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
+        let tx = TransactionId::new(ReplicaId(1), 900);
+        let undo = undo_env(1, 3, 13, seen_r1(2), tx, UndoPolicy::StrictInverse);
+        let undo_id = undo.id;
+
+        let mut set = OperationSet::new();
+        set.accept_all(vec![
+            declare_transaction(1, 0, 10, CausalContext::new(), tx),
+            transpose_member(1, 1, 11, seen_r1(0), tx, pid, interval(0, 1)),
+            respell_env(1, 2, 12, seen_r1(1), pid, CmnNominal::D),
+            undo,
+        ]);
+        let out = set.reduce_onto(&base);
+
+        assert!(
+            matches!(
+                undo_effect(&out.state, undo_id),
+                OperationEffect::Conflicted { .. }
+            ),
+            "a later canonical writer supersedes a strict undo"
+        );
+        // Nothing was rolled back: the pitch stays transposed and the newer
+        // authored spelling stands.
+        assert_eq!(cmn_of(&pitch_of(&out.score, pid)), (CmnNominal::C, 1, 4));
+        let atts = attachments_of(&out.score, pid);
+        assert!(
+            atts.contains(&(SpellingSource::UserChosen, CmnNominal::D, 0)),
+            "the later respell was not erased: {atts:?}"
+        );
+    }
+
+    #[test]
+    fn best_effort_undo_will_not_restore_a_pitch_whose_spelling_was_superseded() {
+        // The pitch value and its engraved spelling set are one undo unit.
+        // Restoring the pitch alone would leave a spelling authored against the
+        // transposed pitch attached to the pitch it used to be.
+        let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
+        let tx = TransactionId::new(ReplicaId(1), 900);
+        let undo = undo_env(1, 3, 13, seen_r1(2), tx, UndoPolicy::BestEffort);
+        let undo_id = undo.id;
+
+        let mut set = OperationSet::new();
+        set.accept_all(vec![
+            declare_transaction(1, 0, 10, CausalContext::new(), tx),
+            transpose_member(1, 1, 11, seen_r1(0), tx, pid, interval(0, 1)),
+            respell_env(1, 2, 12, seen_r1(1), pid, CmnNominal::D),
+            undo,
+        ]);
+        let out = set.reduce_onto(&base);
+
+        assert_eq!(undo_effect(&out.state, undo_id), OperationEffect::Applied);
+        assert_eq!(
+            cmn_of(&pitch_of(&out.score, pid)),
+            (CmnNominal::C, 1, 4),
+            "best-effort skipped the pitch because its spelling set was superseded"
+        );
+        assert!(attachments_of(&out.score, pid).contains(&(
+            SpellingSource::UserChosen,
+            CmnNominal::D,
+            0
+        )));
+    }
+
+    #[test]
+    fn a_concurrent_respell_and_transpose_converge_in_canonical_order() {
+        // Neither sees the other. Both write the pitch's engraved spelling set,
+        // so the canonically-last writer owns it — and both permutations of the
+        // input reduce to the same score, which is the only property that
+        // matters.
+        let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
+        let tx = TransactionId::new(ReplicaId(1), 900);
+
+        let build = || {
+            vec![
+                declare_transaction(1, 0, 10, CausalContext::new(), tx),
+                // Concurrent: replica 2's respell has not seen replica 1's
+                // transpose, and vice versa.
+                transpose_member(1, 1, 11, seen_r1(0), tx, pid, interval(0, 1)),
+                respell_env(2, 0, 12, CausalContext::new(), pid, CmnNominal::D),
+            ]
+        };
+        let mut forward = OperationSet::new();
+        forward.accept_all(build());
+        let a = forward.reduce_onto(&base);
+
+        let mut reversed = OperationSet::new();
+        let mut envs = build();
+        envs.reverse();
+        reversed.accept_all(envs);
+        let b = reversed.reduce_onto(&base);
+
+        assert_eq!(a.score, b.score, "reduction is permutation-invariant");
+        assert_eq!(a.state.canonical_bytes(), b.state.canonical_bytes());
+        // The pitch moved; exactly one authored spelling stands, plus the
+        // propagated record.
+        assert_eq!(cmn_of(&pitch_of(&a.score, pid)), (CmnNominal::C, 1, 4));
+        let atts = attachments_of(&a.score, pid);
+        assert_eq!(
+            atts.iter()
+                .filter(|(s, _, _)| matches!(s, SpellingSource::UserChosen))
+                .count(),
+            1,
+            "one authored spelling: {atts:?}"
+        );
+    }
+
     #[test]
     fn transpose_interval_skips_a_tombstoned_target_but_refuses_a_missing_one() {
         // The skip/refuse distinction: a deleted pitch is not an untransposable

spec/PASS13_CANDIDATES.md

@@ -41,13 +41,16 @@ batch reopens the pass.
 | P13-I2 | `Staff::default_clef` is never consulted: `to_constrained` takes the active clef from the staff instance's `clef_sequence` and falls back to `Clef::default()` (treble), so a bass-clef staff that declares its clef only on the `Staff` engraves as treble. The field is decorative in the projection — is it the fallback, or should it not exist? | `crates/epiphany-layout-ir/DECISIONS.md` ("`Staff::default_clef` is never consulted") | **resolved** (Pass 13: it IS the fallback. `StaffContent` carries it, `active_clef_or` resolves against it, and `editor-core`'s hit-test reads the same function — else a click on a bass staff would resolve its pitch as treble. Removal was rejected: the field is named for its purpose, is encoded on the wire, and dropping it is schema-major) |
 | P13-I3 | `BRAVURA_METRICS`' `NOTEHEAD_ANCHORS` are hand-written, unconsumed, and doubly suspect: they name `stemUpNW`/`stemDownSE` — the corners a normal notehead's stems do *not* attach to, and a pair Bravura's `noteheadBlack` does not define — and their x of `1180` reads like 1.18 staff spaces written in thousandths rather than the table's `1/1024` units (1.18 sp = 1208). They enter only `metrics_hash`, so any correction moves the `GlyphCatalogIdentity` every conformance claim declares. The font is not vendored, so the values cannot be verified in-tree | `crates/epiphany-layout-ir/DECISIONS.md` ("the notehead stem anchors are unusable as written") | **resolved** (Pass 13: deleted. Unverifiable in-tree, unconsumed, and hand-derived where every neighbouring number is machine-extracted. `extract_bravura_outlines.py --anchors` now emits them from the pinned `bravura_metadata.json`, so the table regains them generated rather than remembered; the metadata's SHA-256 is deliberately unpinned and the script refuses until an operator with the font pins it. `GlyphCatalogIdentity` moves once, now, while no conformance claim declares the old one; user "delete them + teach the extractor") |
 
-## Open candidates (Batch 3 not yet open)
+## Batch 3 — OPEN (2026-07-09)
 
-Filed as found; the pass reopens at three (the house rule). Neither is a live
-incorrectness — each is a place where the spec cannot yet support a claim it
-makes about itself.
+Three candidates, so the pass reopens per the house rule. P13-S3 arrived as a
+**live incorrectness** — a Push-4a follow-up audit found that the spelling-set
+chain introduced to make `TransposeInterval` undoable had only one writer, so
+undo erased an ordinary `RespellPitch` on either side of it. It is resolved.
+S1 and S2 remain open.
 
 | Id | One-line statement | Filed in | Status |
 |---|---|---|---|
 | P13-S1 | **169 of core_spec's 207 `requirement` blocks carry no `\label`**, so no conformance claim can cite them. Chapter 4 (`Tuning Systems and Pitch Spaces`) is 9/9 unlabeled and Chapter 11 (`Determinism Contract`) is 15/15, but the gap is universal, not local: `Semantic Operations` 24/27, `The Score Graph` 22/28, `Pitch` 10/13. The requirements *are* normative and *are* implemented; they simply cannot be named. Every `req:*` label the repo cites was added ad hoc by the pass that needed it | this file | **open** (found while auditing Push 4a; the audit that surfaced it scoped it to Chapter 4, which is where it was noticed, not where it lives) |
 | P13-S2 | `cmn-24` is declared in the built-in pitch-space table (`core_spec.tex` §"Built-in Catalog") as "CMN extended with 24-EDO quarter-tone accidentals", but **cannot be represented**: `PitchSpacePosition::Cmn.alteration` is an `i8` documented as *whole semitones*, and a quarter-tone is half of one. Either the space is not `Cmn`-representable (and needs `Integer`/`Registered`), or `alteration` needs a finer unit — a data-model major | `crates/epiphany-core/DECISIONS.md` (Push 4b blockers) | **open** (blocks Push 4b) |
+| P13-S3 | The `engraved_spelling_chain` introduced with `TransposeInterval`'s undo had a **single writer**. `RespellPitch` mutates the same graph attachments but recorded only on `respell_chain`, so (a) undoing a transposed transaction after a prior respell restored the pitch and **erased the respell**, and (b) a respell landing canonically *after* the transaction was invisible to the chain, so a `StrictInverse` undo reported `Applied` and **wiped the newer authoring** instead of refusing as superseded. A `BestEffort` undo could also restore the pre-transpose pitch while leaving a spelling authored against the transposed one | `crates/epiphany-ops/DECISIONS.md` (P13-S3) | **resolved** (both operations now record on the shared key; pitch value + spelling set undo as one unit; new `req:opcat:spelling-set-chain`. The chain stays *physically* separate from `respell_chain`, which is `RespellPitch`'s LWW conflict state — folding transposes in would make a concurrent respell conflict with a transpose and move the canonical bytes of every existing history) |

spec/operation_catalog.tex

@@ -786,12 +786,40 @@ is transposed by \texttt{interval}.
 
 \textbf{Undo semantics.} Nothing is minted. \texttt{TransposeInterval}
 \MUST{} record each transposed pitch's new value into that pitch's value chain,
-and each spelling attachment it rewrote into the corresponding spelling chain, so
-that value-restoring undo recovers the pre-transpose pitch \emph{and} its
-pre-transpose spelling. Restoring the pitch alone would leave a notehead spelled
-for a pitch that no longer exists. This is where \texttt{TransposeInterval}
-departs from the frozen \texttt{Transpose}, which records nothing and is
-therefore not undoable.
+and that pitch's resulting \emph{engraved spelling set} into the spelling-set
+chain, so that value-restoring undo recovers the pre-transpose pitch \emph{and}
+its pre-transpose spelling. Restoring the pitch alone would leave a notehead
+spelled for a pitch that no longer exists. This is where
+\texttt{TransposeInterval} departs from the frozen \texttt{Transpose}, which
+records nothing and is therefore not undoable.
+
+\begin{requirement}
+  \label{req:opcat:spelling-set-chain}
+  The pitch's engraved spelling set is a single undo key with \emph{more than
+  one writer}. Every operation that changes it --- \texttt{RespellPitch} and
+  \texttt{TransposeInterval} alike --- \MUST{} record a write on that key.
+  Consequently a \texttt{RespellPitch} causally prior to a transposed
+  transaction is that transaction's chain-predecessor and is restored by its
+  undo; and a \texttt{RespellPitch} canonically \emph{later} supersedes the
+  transaction's write, so a \texttt{StrictInverse} undo conflicts rather than
+  erasing it, per the general superseded-writer rule.
+
+  A pitch's value and its engraved spelling set \MUST{} undo as one unit: if
+  either is superseded, neither is restored. A \texttt{BestEffort} undo
+  \MUSTNOT{} restore the pre-transpose pitch while leaving a spelling authored
+  against the transposed one.
+\end{requirement}
+
+\begin{rationale}
+  Ratified as P13-S3. An implementation may keep the spelling-set chain
+  physically separate from whatever chain drives \texttt{RespellPitch}'s
+  last-writer-wins conflict detection --- the reference implementation does,
+  because folding transposes into that chain would make a concurrent respell
+  \emph{conflict} with a transpose and would move the canonical bytes of every
+  existing history. What it may not do is let one writer own the key. A chain
+  with a single writer cannot see the other's prior value (so undo erases it) and
+  cannot see the other's later value (so undo overwrites it).
+\end{rationale}
 
 An inverse interval usually exists ($(-d, -c)$), because the reduction never
 saturates --- but not always: $\texttt{i32::MIN}$ has no negation. Undo does not