Pass 12 G-pass: code tranche (K3/K9/C4/H7) + review fixes

The decided code work behind aff1809, review-hardened (high-effort
multi-agent review; 3 correctness findings fixed pre-commit, all
regression-locked).

epiphany-ops:
- K3: SystemDerivedContentImmutable (12) — modify_event /
  modify_identified_pitch refuse intrinsic-content rewrites of
  SYSTEM_DERIVED pitches, checked against the system_mints registry
  (base-seeded + op mints, so reduce()/reduce_onto() agree).
  REVIEW FIX: Transpose now *skips* system-derived targets like
  tombstoned ones (an in-place alteration shift desynchronized content
  from the derivation registry -> checkpoint-dependent verdicts); an
  all-system transpose reduces as the K3 no-op. Catalog Transpose
  updated.
- K9: RecreateContentMismatch (13) replaces the TargetMissing misnomer
  at both value-retaining re-create sites (CreateStaff, carried
  TimeSignature). Catalog corrected: container creates are plain
  set-union (no value comparison), not K9 sites.
- C4: ReanchorReason::SameCanvasNearer (6); rank-4 recording routes
  through rank_reason. REVIEW FIX: an *unestablished* rank 4
  (unresolvable placement fallthrough in containment_rank) keeps the
  honest ExplicitFallback — selection order unchanged.
- Filed P13-K1 (pre-existing checkpoint asymmetry for ModifyEvent-
  introduced system pitches) in DECISIONS rather than improvising.

epiphany-core (H7, req:pitch:authored-uninferred):
- Authored attachments surface for inference-ineligible targets in
  both pre-passes (best_authored_spelling/_decomposition refactor,
  candidates-first liveness via the existing Score::live_pitch_ids);
  two new taxonomy buckets enter the derivation fingerprint. The old
  test locking the pre-decision mirror is flipped to the ratified
  behavior.

epiphany-testkit (review fixes):
- prepass_harness: spelling-unavailable pitches may carry *authored*
  surfacings (inferred still forbidden); decomposition reconstruction
  invariants scoped to algorithm output (authored entries are
  invariant-15's graph-level jurisdiction); accounting identity gains
  the authored-uninferred bucket.
- generators: the three appended discriminants (12/13/6) now generate.

Full gate green: fmt, clippy -D warnings, rustdoc -D warnings, 30
workspace suites, conformance scale 1 (8/8). Wire goldens + decode
bounds for the appended discriminants; 12 new regression tests.

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

crates/epiphany-core/src/prepass.rs

@@ -116,6 +116,11 @@ pub struct TaxonomyReport {
     /// Pitches whose pitch space declares spelling unavailable (non-`cmn-12`-
     /// determinable positions: JI vectors, non-12 EDOs, registered grammars).
     pub spelling_unavailable: usize,
+    /// Pitches the algorithm produced *no* inferred spelling for whose
+    /// annotation is an authored attachment surfacing on its own
+    /// (`req:pitch:authored-uninferred`, Pass 12 P12-H7). Counted distinctly
+    /// from `spellings_authored` (an authored *override* of inferred output).
+    pub spellings_authored_uninferred: usize,
 
     // --- Decomposition outcomes (over events). ---
     /// Eligible events whose effective decomposition is the pre-pass's inferred
@@ -142,6 +147,12 @@ pub struct TaxonomyReport {
     /// skipped rather than mis-rendered. Expected to be zero for well-formed
     /// metric input.
     pub decomposition_ungriddable: usize,
+    /// Events the pre-pass produced *no* inferred decomposition for
+    /// (ungriddable, non-metric, non-musical, or an inapplicable kind) whose
+    /// annotation is an authored attachment surfacing on its own
+    /// (`req:pitch:authored-uninferred`, Pass 12 P12-H7). Counted distinctly
+    /// from `decompositions_authored` (an authored *override*).
+    pub decompositions_authored_uninferred: usize,
 }
 
 /// The canonical derived annotations for a score under a profile: the effective
@@ -206,12 +217,14 @@ impl DerivedAnnotations {
             t.spellings_inferred,
             t.spellings_authored,
             t.spelling_unavailable,
+            t.spellings_authored_uninferred,
             t.decompositions_inferred,
             t.decompositions_authored,
             t.decomposition_skipped_nonmusical,
             t.decomposition_deferred_nonmetric,
             t.decomposition_inapplicable,
             t.decomposition_ungriddable,
+            t.decompositions_authored_uninferred,
         ] {
             out.extend_from_slice(&(count as u64).to_le_bytes());
         }
@@ -267,6 +280,35 @@ pub fn derive_annotations(score: &Score, profile: &PrePassProfile) -> DerivedAnn
             }
             spellings.insert(pid, resolved);
         }
+        // Authored spellings for pitches the algorithm produced *no* inferred
+        // spelling for (`req:pitch:authored-uninferred`, Pass 12 P12-H7): the
+        // winning authored attachment surfaces on its own — an authored
+        // attachment is precisely how a user notates what the algorithm
+        // cannot infer, and the derived-annotation surface must not render it
+        // invisible. Only pitches that exist in the score surface (an
+        // attachment in tombstoned-target state stays diagnostic-only).
+        // Candidates come from the attachments first, so the common
+        // no-attachments case never walks the arena for the liveness set.
+        let mut uninferred: BTreeSet<PitchId> = BTreeSet::new();
+        for att in &score.spelling_attachments {
+            if let SpellingScope::Pitch(p) = &att.scope {
+                if !spellings.contains_key(p) {
+                    uninferred.insert(*p);
+                }
+            }
+        }
+        if !uninferred.is_empty() {
+            let live_pitches = score.live_pitch_ids();
+            for pid in uninferred {
+                if !live_pitches.contains(&pid) {
+                    continue;
+                }
+                if let Some(resolved) = best_authored_spelling(score, pid, precedence) {
+                    taxonomy.spellings_authored_uninferred += 1;
+                    spellings.insert(pid, resolved);
+                }
+            }
+        }
     }
 
     // --- Decomposition pre-pass. ---
@@ -281,6 +323,23 @@ pub fn derive_annotations(score: &Score, profile: &PrePassProfile) -> DerivedAnn
             }
             decompositions.insert(eid, resolved);
         }
+        // Authored decompositions for events the pre-pass produced *no*
+        // inferred decomposition for — ungriddable, non-metric, non-musical,
+        // or an inapplicable kind (`req:pitch:authored-uninferred`, Pass 12
+        // P12-H7). Mirrors the spelling surfacing above; only events that
+        // exist in the score surface.
+        let mut uninferred: BTreeSet<EventId> = BTreeSet::new();
+        for att in &score.decomposition_attachments {
+            if !decompositions.contains_key(&att.target) && score.events.get(att.target).is_some() {
+                uninferred.insert(att.target);
+            }
+        }
+        for eid in uninferred {
+            if let Some(resolved) = best_authored_decomposition(score, eid) {
+                taxonomy.decompositions_authored_uninferred += 1;
+                decompositions.insert(eid, resolved);
+            }
+        }
     }
 
     DerivedAnnotations {
@@ -722,12 +781,30 @@ pub fn resolve_spelling(
     inferred: PitchSpelling,
     precedence: &SpellingPrecedence,
 ) -> ResolvedSpelling {
+    match best_authored_spelling(score, pitch, precedence) {
+        Some(resolved) => resolved,
+        None => ResolvedSpelling {
+            spelling: inferred,
+            provenance: SpellingProvenance::Inferred,
+        },
+    }
+}
+
+/// The winning authored spelling for `pitch`, if any: engraved layer,
+/// pitch-scoped, explicit, source outranking [`SpellingSourceKind::Inferred`]
+/// in `precedence`. Among candidates, lowest precedence rank wins, then
+/// highest priority; a remaining tie keeps the first candidate in the score's
+/// `spelling_attachments` order, which is canonical (codec-fixed), so the
+/// resolution is deterministic across replicas. Shared by
+/// [`resolve_spelling`] (authored *override* of an inferred spelling) and the
+/// authored-only surfacing path for inference-ineligible pitches
+/// (`req:pitch:authored-uninferred`, Pass 12 P12-H7).
+fn best_authored_spelling(
+    score: &Score,
+    pitch: PitchId,
+    precedence: &SpellingPrecedence,
+) -> Option<ResolvedSpelling> {
     let inferred_rank = precedence.rank(SpellingSourceKind::Inferred);
-    // The best authored override: engraved layer, pitch-scoped, explicit, source
-    // outranking Inferred. Among candidates, lowest precedence rank wins, then
-    // highest priority; a remaining tie keeps the first candidate in the score's
-    // `spelling_attachments` order, which is canonical (codec-fixed), so the
-    // resolution is deterministic across replicas.
     let mut best: Option<(usize, i32, &SpellingAttachment)> = None;
     for att in &score.spelling_attachments {
         if att.layer.is_some() {
@@ -760,22 +837,16 @@ pub fn resolve_spelling(
         };
     }
 
-    match best {
+    best.map(|(_, _, att)| {
-        Some((_, _, att)) => {
+        if let SpellingDirective::Explicit(spelling) = &att.directive {
-            if let SpellingDirective::Explicit(spelling) = &att.directive {
+            ResolvedSpelling {
-                ResolvedSpelling {
+                spelling: spelling.clone(),
-                    spelling: spelling.clone(),
+                provenance: SpellingProvenance::Authored(att.source.kind()),
-                    provenance: SpellingProvenance::Authored(att.source.kind()),
-                }
-            } else {
-                unreachable!("filtered to Explicit directives")
             }
+        } else {
+            unreachable!("filtered to Explicit directives")
         }
-        None => ResolvedSpelling {
+    })
-            spelling: inferred,
-            provenance: SpellingProvenance::Inferred,
-        },
-    }
 }
 
 // ===========================================================================
@@ -1195,6 +1266,17 @@ pub fn resolve_decomposition(
     event: EventId,
     inferred: DecompositionAttachment,
 ) -> DecompositionAttachment {
+    best_authored_decomposition(score, event).unwrap_or(inferred)
+}
+
+/// The winning authored decomposition for `event`, if any: source outranking
+/// [`DecompositionSource::Inferred`] under the fixed default order (ratified
+/// Pass 12, P12-H6 — decomposition precedence is not configurable); lowest
+/// rank wins; a full tie keeps the earlier attachment in the score's
+/// canonical `decomposition_attachments` order. Shared by
+/// [`resolve_decomposition`] (authored *override*) and the authored-only
+/// surfacing path for inference-ineligible events (Pass 12 P12-H7).
+fn best_authored_decomposition(score: &Score, event: EventId) -> Option<DecompositionAttachment> {
     let inferred_rank = decomposition_source_rank(&DecompositionSource::Inferred);
     let mut best: Option<(usize, &DecompositionAttachment)> = None;
     for att in &score.decomposition_attachments {
@@ -1218,10 +1300,7 @@ pub fn resolve_decomposition(
             }
         };
     }
-    match best {
+    best.map(|(_, att)| att.clone())
-        Some((_, att)) => att.clone(),
-        None => inferred,
-    }
 }
 
 #[cfg(test)]

crates/epiphany-core/src/prepass/tests.rs

@@ -1148,6 +1148,185 @@ fn inferred_source_attachment_does_not_outrank_the_prepass() {
     assert_eq!(ann.taxonomy.decompositions_inferred, 2);
 }
 
+#[test]
+fn authored_decomposition_surfaces_for_an_ungriddable_event_p12_h7() {
+    // req:pitch:authored-uninferred (Pass 12, P12-H7): an authored attachment
+    // targeting an event the pre-pass cannot infer for (off-grid position →
+    // ungriddable) surfaces as the resolved annotation on its own, counted in
+    // the dedicated authored-uninferred bucket.
+    let mut captured = None;
+    let mut score = metric_score(|idc, voice| {
+        let eid = idc.mint();
+        captured = Some(eid);
+        let pid = idc.mint::<PitchId>();
+        let ev = pitched(
+            eid,
+            voice,
+            r(1, 3), // off-grid (non-dyadic) position → nothing inferred
+            r(1, 4),
+            vec![IdentifiedPitch {
+                id: pid,
+                pitch: integer_pitch(48),
+            }],
+        );
+        (vec![ev], vec![])
+    });
+    let eid = captured.expect("event minted");
+    let authored = DecompositionAttachment {
+        target: eid,
+        components: vec![NotatedComponent {
+            base_value: NoteValue::Quarter,
+            dots: 0,
+            tuplet: None,
+            tied_to_next: false,
+        }],
+        source: DecompositionSource::UserChosen,
+    };
+    score.decomposition_attachments.push(authored.clone());
+
+    let ann = derive_annotations(&score, &PrePassProfile::default());
+    assert_eq!(
+        ann.decompositions[&eid], authored,
+        "the authored attachment surfaces on its own"
+    );
+    assert_eq!(
+        ann.taxonomy.decomposition_ungriddable, 1,
+        "the event is still honestly classified ungriddable"
+    );
+    assert_eq!(ann.taxonomy.decompositions_authored_uninferred, 1);
+    assert_eq!(
+        ann.taxonomy.decompositions_authored, 0,
+        "not an override — there was nothing inferred to override"
+    );
+    assert_eq!(
+        ann.decompositions.len(),
+        ann.taxonomy.decompositions_inferred
+            + ann.taxonomy.decompositions_authored
+            + ann.taxonomy.decompositions_authored_uninferred,
+        "the harness accounting identity holds"
+    );
+}
+
+#[test]
+fn inferred_source_attachment_does_not_surface_for_ineligible_events_p12_h7() {
+    // The rank gate holds on the authored-only path too: a stored attachment
+    // whose source is `Inferred` does not outrank the pre-pass, so it does
+    // not surface for an inference-ineligible event either.
+    let mut captured = None;
+    let mut score = metric_score(|idc, voice| {
+        let eid = idc.mint();
+        captured = Some(eid);
+        let pid = idc.mint::<PitchId>();
+        let ev = pitched(
+            eid,
+            voice,
+            r(1, 3),
+            r(1, 4),
+            vec![IdentifiedPitch {
+                id: pid,
+                pitch: integer_pitch(48),
+            }],
+        );
+        (vec![ev], vec![])
+    });
+    let eid = captured.expect("event minted");
+    score
+        .decomposition_attachments
+        .push(DecompositionAttachment {
+            target: eid,
+            components: vec![NotatedComponent {
+                base_value: NoteValue::Quarter,
+                dots: 0,
+                tuplet: None,
+                tied_to_next: false,
+            }],
+            source: DecompositionSource::Inferred,
+        });
+
+    let ann = derive_annotations(&score, &PrePassProfile::default());
+    assert!(
+        !ann.decompositions.contains_key(&eid),
+        "an Inferred-source attachment does not surface"
+    );
+    assert_eq!(ann.taxonomy.decompositions_authored_uninferred, 0);
+}
+
+#[test]
+fn authored_spelling_surfaces_for_an_unavailable_pitch_p12_h7() {
+    // The spelling mirror of the surfacing rule: an authored explicit
+    // attachment on a pitch whose pitch space declares spelling unavailable
+    // (JI) surfaces with authored provenance; an attachment targeting a pitch
+    // absent from the score stays diagnostic-only. The derivation stays
+    // deterministic (byte-equal fingerprints).
+    let mut captured = None;
+    let mut score = metric_score(|idc, voice| {
+        let eid = idc.mint();
+        let pid = idc.mint::<PitchId>();
+        captured = Some(pid);
+        let ev = pitched(
+            eid,
+            voice,
+            r(0, 4),
+            r(1, 4),
+            vec![IdentifiedPitch {
+                id: pid,
+                pitch: ji_pitch(),
+            }],
+        );
+        (vec![ev], vec![])
+    });
+    let pid = captured.expect("pitch minted");
+    let authored_spelling = PitchSpelling {
+        nominal: SpellingNominal::Cmn(CmnNominal::D),
+        accidentals: vec![AccidentalId::new("flat")],
+        octave: 4,
+        render_hints: Default::default(),
+    };
+    score.spelling_attachments.push(SpellingAttachment {
+        scope: SpellingScope::Pitch(pid),
+        directive: SpellingDirective::Explicit(authored_spelling.clone()),
+        source: SpellingSource::UserChosen,
+        priority: 0,
+        layer: None,
+    });
+    // A second attachment targeting a pitch that exists nowhere in the score:
+    // preserved canonical state, but it surfaces no annotation.
+    let dangling = PitchId::new(ReplicaId(0xD00D), 1);
+    score.spelling_attachments.push(SpellingAttachment {
+        scope: SpellingScope::Pitch(dangling),
+        directive: SpellingDirective::Explicit(authored_spelling.clone()),
+        source: SpellingSource::UserChosen,
+        priority: 0,
+        layer: None,
+    });
+
+    let ann = derive_annotations(&score, &PrePassProfile::default());
+    let resolved = ann
+        .spellings
+        .get(&pid)
+        .expect("the authored spelling surfaces for the unavailable pitch");
+    assert_eq!(resolved.spelling, authored_spelling);
+    assert_eq!(
+        resolved.provenance,
+        SpellingProvenance::Authored(crate::pitch::SpellingSourceKind::UserChosen)
+    );
+    assert_eq!(ann.taxonomy.spellings_authored_uninferred, 1);
+    assert_eq!(
+        ann.taxonomy.spelling_unavailable, 1,
+        "the pitch is still honestly classified unavailable"
+    );
+    assert!(
+        !ann.spellings.contains_key(&dangling),
+        "an attachment on an absent pitch surfaces nothing"
+    );
+    let again = derive_annotations(&score, &PrePassProfile::default());
+    assert_eq!(
+        ann.canonical_fingerprint(),
+        again.canonical_fingerprint(),
+        "the surfacing path is deterministic"
+    );
+}
+
 #[test]
 fn decomposition_precedence_ranks_sources_then_canonical_order() {
     // UserChosen outranks Imported regardless of attachment order (the spec's
@@ -1210,14 +1389,14 @@ fn derivation_with_authored_decomposition_is_deterministic() {
 }
 
 #[test]
-fn authored_attachment_on_an_ungriddable_event_does_not_surface() {
+fn authored_attachment_on_an_ungriddable_event_surfaces_p12_h7() {
-    // The resolution step mirrors the spelling side: it layers authored
+    // The Pass-12 question this test used to park is DECIDED
-    // overrides above the pre-pass's *inferred* output. An event the pre-pass
+    // (`req:pitch:authored-uninferred`, P12-H7): an authored attachment on an
-    // cannot grid emits nothing to override, so an authored attachment for it
+    // event the pre-pass cannot grid SURFACES as the resolved annotation on
-    // stays in canonical score state without surfacing as a derived annotation,
+    // its own — the pre-decision behavior (staying canonical-but-invisible)
-    // and the event stays honestly counted as ungriddable. (Whether authored
+    // is the one this revision reverses. The event stays honestly counted
-    // decompositions should surface for events the algorithm cannot infer for
+    // ungriddable; the surfacing is counted in the authored-uninferred
-    // is a Pass-12 question — see DECISIONS.md.)
+    // bucket, not as an override.
     let mut ids = Vec::new();
     let mut score = metric_score(|idc, voice| {
         let eid = idc.mint();
@@ -1235,13 +1414,17 @@ fn authored_attachment_on_an_ungriddable_event_does_not_surface() {
         );
         (vec![ev], vec![])
     });
-    score
+    let authored = tied_quarters(ids[0], DecompositionSource::UserChosen);
-        .decomposition_attachments
+    score.decomposition_attachments.push(authored.clone());
-        .push(tied_quarters(ids[0], DecompositionSource::UserChosen));
 
     let ann = derive_annotations(&score, &PrePassProfile::default());
-    assert!(ann.decompositions.is_empty());
+    assert_eq!(
+        ann.decompositions.get(&ids[0]),
+        Some(&authored),
+        "the authored attachment surfaces (P12-H7)"
+    );
     assert_eq!(ann.taxonomy.decomposition_ungriddable, 1);
+    assert_eq!(ann.taxonomy.decompositions_authored_uninferred, 1);
     assert_eq!(ann.taxonomy.decompositions_authored, 0);
     assert_eq!(ann.taxonomy.decompositions_inferred, 0);
 }

crates/epiphany-ops/DECISIONS.md

@@ -940,3 +940,38 @@ selection function). Decided with code to land in the G-pass code tranche:
 already `DeclaredByExtension`). **K8** retired: genesis is outside the
 operation set (catalog K1 slots removed, core Ch5 states it). Catalog
 0.5.0 → 0.6.0; Binary Format 0.3.0 → 0.4.0.
+
+### G-pass code-tranche review findings (2026-07-07, all fixed before commit)
+
+A high-effort review of the code tranche confirmed three correctness findings,
+each fixed with a regression test:
+
+1. **Transpose bypassed P12-K3** — it shifted a `SYSTEM_DERIVED` pitch's
+   alteration in place, desynchronizing content from the id's derivation
+   inputs and making the K3 verdict depend on where a snapshot was cut
+   (a full replay's registry holds the mint content; a post-transpose
+   snapshot's holds the shifted content). Fixed: system-derived targets are
+   **skipped** like tombstoned ones (id-namespace filter, so base-free and
+   graph-aware reduction agree); an all-system-derived transpose reduces as
+   `SystemDerivedContentImmutable`. Catalog §Transpose updated.
+2. **Unestablished rank-4 re-anchors were relabeled `SameCanvasNearer`** —
+   `containment_rank` returns 4 both for the established same-canvas case and
+   as the fallthrough when a voice's placement is unresolvable; the P12-C4
+   append must not launder the latter into a positive proximity claim. Fixed:
+   recording routes through `rank_reason`, which downgrades an unestablished
+   4 to the honest `ExplicitFallback`; **selection order is unchanged** (the
+   rank still compares as 4).
+3. **Vocabulary generators lagged the appends** — testkit
+   `precondition_failure_reason`/`reanchor_reason` never emitted discriminants
+   12/13/6, so fuzz gates could not catch a renumbering regression. Fixed.
+
+**Pass-13 candidate (P13-K1, filed not fixed):** the K3 verdict for a system
+pitch *introduced by a ModifyEvent replacement value* (never minted — the
+collision pre-walk deliberately excludes ModifyEvent) differs across a
+snapshot cut: in-session the pitch is not Live (`TargetMissing`); after a
+snapshot re-seeds objects + registry from the base graph, the same modify
+reads `SystemDerivedContentImmutable`. The asymmetry **predates K3** (the
+same split previously read `TargetMissing` vs a silent `Applied` rewrite) and
+is a ModifyEvent-introduction question — whether a replacement value may
+introduce never-minted pitch ids at all — batched for Pass 13, not
+improvised here.

crates/epiphany-ops/src/decode.rs

@@ -221,6 +221,8 @@ fn precondition_reason(reader: &mut Reader<'_>) -> Result<PreconditionFailureRea
         )?)),
         10 => Ok(PreconditionFailureReason::ContainerNotEmpty),
         11 => Ok(PreconditionFailureReason::TempoMapMalformed),
+        12 => Ok(PreconditionFailureReason::SystemDerivedContentImmutable),
+        13 => Ok(PreconditionFailureReason::RecreateContentMismatch),
         tag => Err(MaterializedDecodeError::InvalidTag {
             kind: "PreconditionFailureReason",
             tag,
@@ -257,6 +259,7 @@ fn reanchor_reason(reader: &mut Reader<'_>) -> Result<ReanchorReason> {
             reader,
             ReanchorReasonRegistryId,
         )?)),
+        6 => Ok(ReanchorReason::SameCanvasNearer),
         tag => Err(MaterializedDecodeError::InvalidTag {
             kind: "ReanchorReason",
             tag,
@@ -600,6 +603,25 @@ mod tests {
         }
     }
 
+    #[test]
+    fn pass12_appended_discriminants_decode() {
+        assert_eq!(
+            exact(&[12], precondition_reason).unwrap(),
+            PreconditionFailureReason::SystemDerivedContentImmutable
+        );
+        assert_eq!(
+            exact(&[13], precondition_reason).unwrap(),
+            PreconditionFailureReason::RecreateContentMismatch
+        );
+        assert_eq!(
+            exact(&[6], reanchor_reason).unwrap(),
+            ReanchorReason::SameCanvasNearer
+        );
+        // The vocabularies stay bounded: one past the append rejects.
+        assert!(exact(&[14], precondition_reason).is_err());
+        assert!(exact(&[7], reanchor_reason).is_err());
+    }
+
     #[test]
     fn decoder_rejects_truncation_and_trailing_bytes() {
         let bytes = MaterializedState::default().canonical_bytes();

crates/epiphany-ops/src/effect.rs

@@ -161,6 +161,16 @@ pub enum PreconditionFailureReason {
     ExtensionPrecondition(ExtensionPreconditionId),
     /// A registered precondition code from a versioned registry.
     Registered(PreconditionFailureRegistryId),
+    /// A modify would rewrite the intrinsic content of a `SYSTEM_DERIVED`-
+    /// namespace object in place, invalidating its content derivation
+    /// (Pass 12, P12-K3; core spec Ch5 §System-Derived Identifiers). The
+    /// sanctioned path is minting a replacement object.
+    SystemDerivedContentImmutable,
+    /// A create re-carried a live id with *differing* content
+    /// (operation_catalog §CreateStaff): the target is not missing, its
+    /// content disagrees (Pass 12, P12-K9 — replaces the `TargetMissing`
+    /// misnomer at the value-retaining re-create sites).
+    RecreateContentMismatch,
 }
 
 impl PreconditionFailureReason {
@@ -180,6 +190,9 @@ impl PreconditionFailureReason {
             PreconditionFailureReason::ContainerNotEmpty => 10,
             // Additive (Phase-3 tranche, SetTempoSegment); appended past 10.
             PreconditionFailureReason::TempoMapMalformed => 11,
+            // Additive (Pass-12 G-pass, P12-K3/P12-K9); appended past 11.
+            PreconditionFailureReason::SystemDerivedContentImmutable => 12,
+            PreconditionFailureReason::RecreateContentMismatch => 13,
         }
     }
 }
@@ -291,6 +304,11 @@ pub enum ReanchorReason {
     SameRegionNearer,
     ExplicitFallback,
     DeclaredByExtension(ReanchorReasonRegistryId),
+    /// A rank-4 (same-canvas) proximity survivor (Pass 12, P12-C4).
+    /// Semantically the next rung after `SameRegionNearer`; its wire
+    /// discriminant is 6 because `DeclaredByExtension` already owned 5
+    /// when it was appended.
+    SameCanvasNearer,
 }
 
 impl ReanchorReason {
@@ -302,6 +320,8 @@ impl ReanchorReason {
             ReanchorReason::SameRegionNearer => 3,
             ReanchorReason::ExplicitFallback => 4,
             ReanchorReason::DeclaredByExtension(_) => 5,
+            // Additive (Pass-12 G-pass, P12-C4); appended past 5.
+            ReanchorReason::SameCanvasNearer => 6,
         }
     }
 }
@@ -397,6 +417,32 @@ mod tests {
         assert_ne!(a.to_canonical_bytes(), b.to_canonical_bytes());
     }
 
+    #[test]
+    fn pass12_appended_discriminants_are_locked() {
+        // Pass-12 G-pass appends (binary_format 0.4.0): the wire bytes are
+        // the appended discriminants, nothing prior moved.
+        assert_eq!(
+            PreconditionFailureReason::SystemDerivedContentImmutable.to_canonical_bytes(),
+            vec![12]
+        );
+        assert_eq!(
+            PreconditionFailureReason::RecreateContentMismatch.to_canonical_bytes(),
+            vec![13]
+        );
+        assert_eq!(
+            ReanchorReason::SameCanvasNearer.to_canonical_bytes(),
+            vec![6]
+        );
+        assert_eq!(
+            PreconditionFailureReason::TempoMapMalformed.to_canonical_bytes(),
+            vec![11]
+        );
+        assert_eq!(
+            ReanchorReason::ExplicitFallback.to_canonical_bytes(),
+            vec![4]
+        );
+    }
+
     #[test]
     fn voice_promotion_repair_round_trips_shape() {
         let r = RepairRecord {

crates/epiphany-ops/src/reduce.rs

@@ -1088,17 +1088,21 @@ struct ReferentContext {
 /// staff instance are excluded from "nearest".
 const PROXIMITY_SAME_STAFF_INSTANCE: u8 = 1;
 
-/// Maps an achieved containment-proximity rank (k1 of the "nearest" ordering)
+/// Maps an *established* containment-proximity rank (k1 of the "nearest"
-/// to the ratified [`ReanchorReason`] vocabulary. Rank 4 (same canvas) has no
+/// ordering) to the ratified [`ReanchorReason`] vocabulary. Rank 4 (same
-/// ratified reason variant, so a beyond-region survivor is recorded as the
+/// canvas) records the appended `SameCanvasNearer` (Pass 12, P12-C4; wire
-/// explicit fallback rather than appending a new discriminant (see
+/// discriminant 6 — `DeclaredByExtension` already owned 5). Callers with a
-/// DECISIONS.md — a spec-vocabulary question, batched for Pass 12).
+/// possibly-*unestablished* rank 4 — `containment_rank` also returns 4 when a
+/// voice's placement is unresolvable, a selection-order tie the recording
+/// must not launder into a positive proximity claim — route through
+/// [`Reduction::rank_reason`], which downgrades those to `ExplicitFallback`.
 fn reason_for_rank(rank: u8) -> ReanchorReason {
     match rank {
         0 => ReanchorReason::SameVoiceNearer,
         1 => ReanchorReason::SameStaffInstanceNearer,
         2 => ReanchorReason::SameStaffNearer,
         3 => ReanchorReason::SameRegionNearer,
+        4 => ReanchorReason::SameCanvasNearer,
         _ => ReanchorReason::ExplicitFallback,
     }
 }
@@ -3475,7 +3479,7 @@ impl<'a> Reducer<'a> {
                 } else {
                     OperationEffect::NoOp {
                         reason: NoOpReason::PreconditionFailedUnderReduction {
-                            reason: PreconditionFailureReason::TargetMissing,
+                            reason: PreconditionFailureReason::RecreateContentMismatch,
                         },
                     }
                 };
@@ -3544,7 +3548,7 @@ impl<'a> Reducer<'a> {
                 } else {
                     Err(OperationEffect::NoOp {
                         reason: NoOpReason::PreconditionFailedUnderReduction {
-                            reason: PreconditionFailureReason::TargetMissing,
+                            reason: PreconditionFailureReason::RecreateContentMismatch,
                         },
                     })
                 }
@@ -4985,6 +4989,37 @@ impl<'a> Reducer<'a> {
     // write, a StructuralFieldCollision. The resolved value is materialized in the
     // graph by reduce_onto. The LWW key/diff uses `last_*_modify` working state.
 
+    /// A `SYSTEM_DERIVED` pitch's intrinsic content is immutable under
+    /// reduction (Pass 12, P12-K3; core spec Ch5 §System-Derived
+    /// Identifiers): its identifier is content-derived, so an in-place
+    /// rewrite would invalidate the derivation. The check compares the
+    /// replacement value's canonical pitch bytes against the id's
+    /// *registered derivation inputs* — the same `system_mints` registry the
+    /// collision pre-walk maintains (base-seeded occupants plus op mints),
+    /// so `reduce()` and `reduce_onto()` agree wherever the registry holds
+    /// the entry. An unregistered id (base-free reduction over a pitch the
+    /// base seeded) is unverifiable and passes, like the other
+    /// graph-aware-only preconditions.
+    ///
+    /// Known residue (filed as a Pass-13 candidate; see DECISIONS.md): a
+    /// system pitch *introduced into the graph by a ModifyEvent replacement*
+    /// (never minted — the pre-walk deliberately excludes ModifyEvent) gets
+    /// this verdict only after a snapshot re-seeds the registry from the
+    /// base graph; in-session it reads `TargetMissing` instead. That
+    /// checkpoint-cut asymmetry for ModifyEvent-introduced content predates
+    /// this precondition (pre-K3 the same split read `TargetMissing` vs a
+    /// silent `Applied` rewrite) and is a ModifyEvent-introduction question,
+    /// not a K3 one.
+    fn system_derived_rewrite(&self, id: PitchId, value: &Pitch) -> bool {
+        if id.replica() != ReplicaId::SYSTEM_DERIVED {
+            return false;
+        }
+        match self.system_mints.get(&(ObjectKind::Pitch, id.counter())) {
+            Some((inputs, _)) => inputs.0 != canonical_pitch_bytes(value),
+            None => false,
+        }
+    }
+
     fn modify_event(&mut self, env: &OperationEnvelope, op: &ModifyEventOp) -> OperationEffect {
         let event_id = op.event_id();
         let ev_obj = TypedObjectId::Event(event_id);
@@ -5003,6 +5038,21 @@ impl<'a> Reducer<'a> {
             }
             Some(ObjectState::Live) => {}
         }
+        // Identity precondition (P12-K3) before the placement precondition:
+        // a replacement value that rewrites a system-derived pitch's
+        // intrinsic content in place is refused outright.
+        let mut carried = Vec::new();
+        op.event.collect_identified_pitches(&mut carried);
+        if carried
+            .iter()
+            .any(|ip| self.system_derived_rewrite(ip.id, &ip.pitch))
+        {
+            return OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::SystemDerivedContentImmutable,
+                },
+            };
+        }
         // A `ModifyEvent` that moves a metric event's span (a trim or move) is now
         // materialized, but it must keep invariant 3 (`VoiceEventsSortedNonOverlap`):
         // refuse a move onto another live event in the voice, or one with a
@@ -5207,7 +5257,26 @@ impl<'a> Reducer<'a> {
                 reason: NoOpReason::TargetTombstoned,
             };
         }
-        for pitch in live {
+        // P12-K3: a SYSTEM_DERIVED pitch's intrinsic content is immutable —
+        // an in-place alteration shift would desynchronize the content from
+        // the id's derivation inputs (and from the `system_mints` registry).
+        // System-derived targets are *skipped* like tombstoned ones (the
+        // shift still applies to the remaining targets); a transpose whose
+        // live targets are all system-derived reduces as a precondition
+        // no-op. The filter reads only the id's namespace, so base-free and
+        // graph-aware reduction agree.
+        let mutable: Vec<PitchId> = live
+            .into_iter()
+            .filter(|pitch| pitch.replica() != ReplicaId::SYSTEM_DERIVED)
+            .collect();
+        if mutable.is_empty() {
+            return OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::SystemDerivedContentImmutable,
+                },
+            };
+        }
+        for pitch in mutable {
             self.graph_transpose_pitch(pitch, op.chromatic_steps);
         }
         OperationEffect::Applied
@@ -5317,6 +5386,15 @@ impl<'a> Reducer<'a> {
             }
             Some(ObjectState::Live) => {}
         }
+        // Identity precondition (P12-K3): a system-derived pitch's intrinsic
+        // content is immutable in place.
+        if self.system_derived_rewrite(op.pitch, &op.value) {
+            return OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::SystemDerivedContentImmutable,
+                },
+            };
+        }
         let prev = self
             .pitch_modify_chain
             .get(&op.pitch)
@@ -5586,9 +5664,11 @@ impl<'a> Reducer<'a> {
                             _ => None,
                         };
                         let reason = match (referent_voice, survivor_voice) {
-                            (Some(referent), Some(survivor)) => {
+                            (Some(referent), Some(survivor)) => self.rank_reason(
-                                reason_for_rank(self.containment_rank(referent, survivor))
+                                self.containment_rank(referent, survivor),
-                            }
+                                referent,
+                                Some(survivor),
+                            ),
                             // No indexed placement for either side (a
                             // non-metric endpoint): the pre-four-key default.
                             _ => ReanchorReason::SameVoiceNearer,
@@ -5703,6 +5783,45 @@ impl<'a> Reducer<'a> {
     /// same staff instance 1, same staff 2, same region 3, same canvas 4.
     /// Computed from the base-free ledger indices, so `reduce()` and
     /// `reduce_onto()` rank identically wherever both represent the scenario.
+    /// Whether a rank-4 verdict from [`Self::containment_rank`] was
+    /// *established* (both voices' placements resolve through instance and
+    /// region, so "same canvas" is a proven fact of the singleton canvas)
+    /// rather than the unresolvable-placement fallthrough. Recording reads
+    /// this so an unestablished 4 stays the honest `ExplicitFallback`
+    /// (Pass 12, P12-C4) — selection order is unaffected either way.
+    fn canvas_rank_established(&self, referent_voice: VoiceId, candidate_voice: VoiceId) -> bool {
+        let (Some(referent), Some(candidate)) = (
+            self.voice_instance(referent_voice),
+            self.voice_instance(candidate_voice),
+        ) else {
+            return false;
+        };
+        self.instance_region_of(referent).is_some() && self.instance_region_of(candidate).is_some()
+    }
+
+    /// The [`ReanchorReason`] to *record* for an achieved rank: ranks 0–3 map
+    /// directly; rank 4 records `SameCanvasNearer` only when the proximity
+    /// was established ([`Self::canvas_rank_established`]), else the honest
+    /// `ExplicitFallback`. `survivor_voice` is `None` when the winning
+    /// candidate's voice is itself unresolvable — never established.
+    fn rank_reason(
+        &self,
+        rank: u8,
+        referent_voice: VoiceId,
+        survivor_voice: Option<VoiceId>,
+    ) -> ReanchorReason {
+        if rank == 4 {
+            let established = survivor_voice
+                .is_some_and(|survivor| self.canvas_rank_established(referent_voice, survivor));
+            return if established {
+                ReanchorReason::SameCanvasNearer
+            } else {
+                ReanchorReason::ExplicitFallback
+            };
+        }
+        reason_for_rank(rank)
+    }
+
     fn containment_rank(&self, referent_voice: VoiceId, candidate_voice: VoiceId) -> u8 {
         if referent_voice == candidate_voice {
             return 0;
@@ -7729,6 +7848,69 @@ mod tests {
         );
     }
 
+    #[test]
+    fn transpose_skips_system_derived_targets_p12_k3() {
+        // Review finding on P12-K3: Transpose must not rewrite a
+        // SYSTEM_DERIVED pitch's intrinsic content in place — that would
+        // desynchronize the content from the id's derivation inputs (and from
+        // the `system_mints` registry the modify preconditions consult),
+        // making the K3 verdict depend on where a snapshot was cut. System
+        // targets are skipped like tombstoned ones; all-system degenerates to
+        // the K3 precondition no-op.
+        use epiphany_core::derive_system_pitch_id;
+        let content = crate::valuegen::pitch_value_nth(1);
+        let system_id = derive_system_pitch_id(&content);
+        let normal = PitchId::new(ReplicaId(9), 501);
+
+        let a = insert_with_pitch_content(1, 0, 10, 1, 100, 0, system_id, &content);
+        let b = insert_with_pitch_content(1, 1, 11, 2, 101, 0, normal, &content);
+        let after_inserts = CausalContext::new().with_seen(ReplicaId(1), 1);
+        // Mixed normal/system targets: the system pitch is skipped, the
+        // normal one shifts, the op applies.
+        let t_mixed = prim_env(
+            3,
+            0,
+            30,
+            after_inserts.clone(),
+            OperationKind::Transpose(TransposeOp {
+                targets: vec![system_id, normal],
+                chromatic_steps: 2,
+            }),
+        );
+        // All targets system-derived: the K3 precondition no-op.
+        let t_system = prim_env(
+            4,
+            0,
+            31,
+            after_inserts,
+            OperationKind::Transpose(TransposeOp {
+                targets: vec![system_id],
+                chromatic_steps: 2,
+            }),
+        );
+        let mut set = OperationSet::new();
+        set.accept_all(vec![a, b, t_mixed.clone(), t_system.clone()]);
+        let state = set.reduce();
+        let effect = |id: OperationId| {
+            state
+                .effects
+                .iter()
+                .find(|(e, _)| *e == id)
+                .map(|(_, eff)| eff)
+                .expect("effect recorded")
+        };
+        assert_eq!(effect(t_mixed.id), &OperationEffect::Applied);
+        assert_eq!(
+            effect(t_system.id),
+            &OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::SystemDerivedContentImmutable,
+                },
+            },
+            "an all-system-derived transpose refuses under P12-K3"
+        );
+    }
+
     #[test]
     fn differing_concurrent_resolves_name_both_resolvers_in_the_meta_conflict() {
         // Chapter 6 §Conflict Resolution Operations: a later differing resolve
@@ -8156,6 +8338,187 @@ mod tests {
         );
     }
 
+    #[test]
+    fn a_system_derived_pitch_content_rewrite_is_refused_p12_k3() {
+        // Pass 12 (P12-K3): a SYSTEM_DERIVED pitch's intrinsic content is
+        // immutable — an in-place rewrite would invalidate the id's content
+        // derivation. A modify carrying the *registered* derivation content
+        // still applies (nothing is rewritten).
+        use epiphany_core::derive_system_pitch_id;
+        let content = crate::valuegen::pitch_value_nth(1);
+        let rewritten = crate::valuegen::pitch_value_nth(2);
+        let system_id = derive_system_pitch_id(&content);
+
+        let mint = insert_with_pitch_content(1, 0, 10, 1, 100, 0, system_id, &content);
+        let rewrite = prim_env(
+            1,
+            1,
+            20,
+            seen_r1(0),
+            OperationKind::ModifyIdentifiedPitch(ModifyIdentifiedPitchOp {
+                pitch: system_id,
+                value: rewritten.clone(),
+            }),
+        );
+        let same = prim_env(
+            1,
+            2,
+            30,
+            seen_r1(1),
+            OperationKind::ModifyIdentifiedPitch(ModifyIdentifiedPitchOp {
+                pitch: system_id,
+                value: content.clone(),
+            }),
+        );
+        let mut set = OperationSet::new();
+        set.accept_all(vec![mint.clone(), rewrite.clone(), same.clone()]);
+        let state = set.reduce();
+
+        let effect_of = |id: OperationId| {
+            state
+                .effects
+                .iter()
+                .find(|(e, _)| *e == id)
+                .map(|(_, eff)| eff)
+        };
+        assert_eq!(
+            effect_of(rewrite.id),
+            Some(&OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::SystemDerivedContentImmutable,
+                },
+            }),
+            "rewriting a system-derived pitch's intrinsic content is refused"
+        );
+        assert_eq!(
+            effect_of(same.id),
+            Some(&OperationEffect::Applied),
+            "a modify carrying the registered derivation content passes"
+        );
+        // Determinism: any permutation reduces to identical bytes.
+        let mut reversed = OperationSet::new();
+        reversed.accept_all(vec![same, rewrite, mint]);
+        assert_eq!(state.canonical_bytes(), reversed.reduce().canonical_bytes());
+    }
+
+    #[test]
+    fn a_modify_event_rewriting_a_system_pitch_is_refused_p12_k3() {
+        // The same identity precondition through the ModifyEvent path: the
+        // replacement event carries the system pitch with rewritten content.
+        use epiphany_core::derive_system_pitch_id;
+        let content = crate::valuegen::pitch_value_nth(1);
+        let rewritten = crate::valuegen::pitch_value_nth(2);
+        let system_id = derive_system_pitch_id(&content);
+
+        let mint = insert_with_pitch_content(1, 0, 10, 1, 100, 0, system_id, &content);
+        let mut replacement = crate::valuegen::insert_event_value(
+            EventId::new(ReplicaId(1), 100),
+            VoiceId::new(ReplicaId(9), 1),
+            pos(0),
+            epiphany_core::MusicalDuration::whole(),
+            &[system_id],
+        );
+        if let Event::Pitched(pe) = &mut replacement {
+            pe.pitches[0].pitch = rewritten;
+        }
+        let modify = prim_env(
+            1,
+            1,
+            20,
+            seen_r1(0),
+            OperationKind::ModifyEvent(ModifyEventOp { event: replacement }),
+        );
+        let mut set = OperationSet::new();
+        set.accept_all(vec![mint, modify.clone()]);
+        let state = set.reduce();
+
+        assert_eq!(
+            state
+                .effects
+                .iter()
+                .find(|(e, _)| *e == modify.id)
+                .map(|(_, eff)| eff),
+            Some(&OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::SystemDerivedContentImmutable,
+                },
+            }),
+            "a ModifyEvent rewriting a carried system pitch is refused"
+        );
+    }
+
+    #[test]
+    fn a_rank_four_reanchor_records_same_canvas_nearer_p12_c4() {
+        // Pass 12 (P12-C4): the rank-4 (same-canvas) proximity survivor has
+        // its own appended reason; ExplicitFallback stays the beyond-ladder
+        // recording only.
+        assert_eq!(reason_for_rank(4), ReanchorReason::SameCanvasNearer);
+        assert_eq!(reason_for_rank(3), ReanchorReason::SameRegionNearer);
+        assert_eq!(reason_for_rank(5), ReanchorReason::ExplicitFallback);
+    }
+
+    #[test]
+    fn an_unestablished_rank_four_reanchor_keeps_the_explicit_fallback() {
+        // Review finding on P12-C4: `containment_rank` also returns 4 when a
+        // voice's staff-instance placement is *unresolvable* (here: base-free
+        // reduction, where inserted voices have no op-created instance), and
+        // that conflated 4 must NOT be recorded as a positive
+        // `SameCanvasNearer` claim — the honest recording stays
+        // `ExplicitFallback`. Selection order is unchanged either way.
+        let e1 = EventId::new(ReplicaId(1), 100);
+        let e2 = EventId::new(ReplicaId(1), 101);
+        let slur = epiphany_core::SlurId::new(ReplicaId(1), 1);
+        let create = prim_env(
+            1,
+            2,
+            12,
+            CausalContext::new().with_seen(ReplicaId(1), 1),
+            create_slur(slur, e1, e2),
+        );
+        let del = prim_env(
+            1,
+            3,
+            13,
+            CausalContext::new().with_seen(ReplicaId(1), 2),
+            OperationKind::DeleteEvent(DeleteEventOp {
+                event: e1,
+                tuplet_compensation: TupletCompensation::NotInTuplet,
+            }),
+        );
+        // Different voices on different staff instances, neither instance
+        // op-created in a region: instance→region never resolves, so
+        // containment_rank falls through to its unestablished 4.
+        let a = insert(1, 0, 10, 1, 100, 0);
+        let mut b = insert(1, 1, 11, 2, 101, 1);
+        if let OperationPayload::Primitive(OperationKind::InsertEvent(ref mut op)) = b.payload {
+            op.staff_instance = StaffInstanceId::new(ReplicaId(9), 1);
+        }
+        let mut set = OperationSet::new();
+        set.accept_all(vec![a, b, create, del.clone()]);
+        let state = set.reduce();
+        let repair = state
+            .effects
+            .iter()
+            .find(|(id, _)| *id == del.id)
+            .and_then(|(_, eff)| match eff {
+                OperationEffect::AppliedWithRepair { repairs } => repairs
+                    .iter()
+                    .find(|r| r.target == TypedObjectId::Slur(slur))
+                    .cloned(),
+                _ => None,
+            })
+            .expect("the slur endpoint deletion records a re-anchor repair");
+        assert_eq!(
+            repair.kind,
+            RepairKind::Reanchored {
+                from: TypedObjectId::Event(e1),
+                to: TypedObjectId::Event(e2),
+                reason: ReanchorReason::ExplicitFallback,
+            },
+            "an unresolvable-placement rank 4 records the honest fallback"
+        );
+    }
+
     // --- ResolveEquivocation (operation_catalog §"ResolveEquivocation"). -----
 
     /// A `RespellPitch` envelope at `id` with an explicit causal context.
@@ -8614,10 +8977,10 @@ mod tests {
             effect_of(differing.id),
             Some(&OperationEffect::NoOp {
                 reason: NoOpReason::PreconditionFailedUnderReduction {
-                    reason: PreconditionFailureReason::TargetMissing,
+                    reason: PreconditionFailureReason::RecreateContentMismatch,
                 },
             }),
-            "a differing value under a live id is a precondition no-op"
+            "a differing value under a live id is a precondition no-op (P12-K9)"
         );
         assert!(matches!(
             state.objects.get(&TypedObjectId::Staff(staff_id)),
@@ -8756,10 +9119,10 @@ mod tests {
                 .map(|(_, eff)| eff),
             Some(&OperationEffect::NoOp {
                 reason: NoOpReason::PreconditionFailedUnderReduction {
-                    reason: PreconditionFailureReason::TargetMissing,
+                    reason: PreconditionFailureReason::RecreateContentMismatch,
                 },
             }),
-            "a differing value under a live signature id is a precondition no-op"
+            "a differing value under a live signature id is a precondition no-op (P12-K9)"
         );
     }
 

crates/epiphany-testkit/src/generators.rs

@@ -410,7 +410,7 @@ pub fn conflict_registry(rng: &mut Rng) -> ConflictRegistry {
 
 /// A typed precondition failure (every core and registered variant).
 pub fn precondition_failure_reason(rng: &mut Rng) -> PreconditionFailureReason {
-    match rng.below(12) {
+    match rng.below(14) {
         0 => PreconditionFailureReason::TargetMissing,
         1 => PreconditionFailureReason::TargetTombstoned,
         2 => PreconditionFailureReason::WrongRegionTimeModel,
@@ -421,7 +421,9 @@ pub fn precondition_failure_reason(rng: &mut Rng) -> PreconditionFailureReason {
         7 => PreconditionFailureReason::VoiceMissing,
         8 => PreconditionFailureReason::ContainerNotEmpty,
         9 => PreconditionFailureReason::TempoMapMalformed,
-        10 => PreconditionFailureReason::ExtensionPrecondition(ExtensionPreconditionId(
+        10 => PreconditionFailureReason::SystemDerivedContentImmutable,
+        11 => PreconditionFailureReason::RecreateContentMismatch,
+        12 => PreconditionFailureReason::ExtensionPrecondition(ExtensionPreconditionId(
             rng.next_u64() as u128,
         )),
         _ => PreconditionFailureReason::Registered(PreconditionFailureRegistryId(
@@ -447,12 +449,13 @@ pub fn no_op_reason(rng: &mut Rng) -> NoOpReason {
 
 /// A re-anchor reason covering every variant.
 pub fn reanchor_reason(rng: &mut Rng) -> ReanchorReason {
-    match rng.below(6) {
+    match rng.below(7) {
         0 => ReanchorReason::SameVoiceNearer,
         1 => ReanchorReason::SameStaffInstanceNearer,
         2 => ReanchorReason::SameStaffNearer,
         3 => ReanchorReason::SameRegionNearer,
         4 => ReanchorReason::ExplicitFallback,
+        5 => ReanchorReason::SameCanvasNearer,
         _ => ReanchorReason::DeclaredByExtension(ReanchorReasonRegistryId(rng.next_u64() as u128)),
     }
 }

crates/epiphany-testkit/src/prepass_harness.rs

@@ -28,10 +28,10 @@
 //!   5 keeps passing with non-trivial pre-pass outputs downstream.
 
 use epiphany_core::{
-    derive_annotations, AccidentalId, AnalysisLayerId, CmnNominal, DerivedAnnotations, Event,
+    derive_annotations, AccidentalId, AnalysisLayerId, CmnNominal, DecompositionSource,
-    EventDuration, MusicalDuration, PitchSpelling, PrePassProfile, RationalTime, Score,
+    DerivedAnnotations, Event, EventDuration, MusicalDuration, PitchSpelling, PrePassProfile,
-    SpellingAttachment, SpellingDirective, SpellingNominal, SpellingProvenance, SpellingScope,
+    RationalTime, Score, SpellingAttachment, SpellingDirective, SpellingNominal,
-    SpellingSource, SpellingSourceKind,
+    SpellingProvenance, SpellingScope, SpellingSource, SpellingSourceKind,
 };
 
 use crate::corpus;
@@ -119,18 +119,26 @@ fn spelling_pitch_class(s: &PitchSpelling) -> Option<i32> {
 }
 
 /// Every *eligible* embedded pitch carries a non-trivial spelling that realizes
-/// its 12-TET pitch class; every spelling-unavailable pitch is left unspelled.
+/// its 12-TET pitch class. A spelling-unavailable pitch is never spelled by the
+/// *algorithm*, but an authored attachment MAY surface for it
+/// (`req:pitch:authored-uninferred`, Pass 12 P12-H7).
 pub fn assert_eligible_pitches_spelled(score: &Score, ann: &DerivedAnnotations) {
     for e in score.events.iter() {
         let mut pitches = Vec::new();
         e.collect_identified_pitches(&mut pitches);
         for ip in pitches {
             match ip.pitch.twelve_tet_class() {
-                None => assert!(
+                None => {
-                    !ann.spellings.contains_key(&ip.id),
+                    // P12-H7: an authored spelling may surface for an
-                    "spelling-unavailable pitch {:?} was spelled anyway",
+                    // unavailable pitch; an *inferred* one is still a bug.
-                    ip.id
+                    if let Some(rs) = ann.spellings.get(&ip.id) {
-                ),
+                        assert!(
+                            matches!(rs.provenance, SpellingProvenance::Authored(_)),
+                            "spelling-unavailable pitch {:?} was inferred-spelled anyway",
+                            ip.id
+                        );
+                    }
+                }
                 Some(class) => {
                     let rs = ann.spellings.get(&ip.id).unwrap_or_else(|| {
                         panic!(
@@ -175,9 +183,15 @@ pub fn assert_eligible_pitches_spelled(score: &Score, ann: &DerivedAnnotations)
     }
 }
 
-/// Every decomposition H emits targets a decomposable event, has a consistent
+/// Every decomposition H's *algorithm* emits targets a decomposable event, has
-/// tie chain, and its components' **sounding** durations reconstruct the event's
+/// a consistent tie chain, and its components' **sounding** durations
-/// musical duration exactly (Chapter 3 invariant 15), recomputed independently.
+/// reconstruct the event's musical duration exactly (Chapter 3 invariant 15),
+/// recomputed independently. Authored entries (overrides and the P12-H7
+/// authored-uninferred surfacings) are exempt from the algorithm-output
+/// invariants: P12-H7 deliberately admits inference-ineligible targets
+/// (non-decomposable kinds, non-musical durations, ungriddable spans), and
+/// authored well-formedness is invariant 15's graph-level jurisdiction, not
+/// the pre-pass gate's.
 pub fn assert_decompositions_reconstruct(score: &Score, ann: &DerivedAnnotations) {
     for (eid, d) in &ann.decompositions {
         assert_eq!(
@@ -191,6 +205,12 @@ pub fn assert_decompositions_reconstruct(score: &Score, ann: &DerivedAnnotations
             .events
             .get(*eid)
             .unwrap_or_else(|| panic!("decomposition targets non-live event {eid:?}"));
+        if !matches!(d.source, DecompositionSource::Inferred) {
+            // Authored entry: surfaced under precedence (override) or P12-H7
+            // (authored-uninferred). The remaining checks are algorithm-output
+            // guarantees and do not apply.
+            continue;
+        }
         assert!(
             matches!(ev, Event::Pitched(_) | Event::Unpitched(_) | Event::Rest(_)),
             "decomposition targets a non-decomposable event kind ({eid:?})"
@@ -232,10 +252,14 @@ pub fn assert_decompositions_reconstruct(score: &Score, ann: &DerivedAnnotations
     // Map and taxonomy counts agree: the effective map is exactly the inferred
     // plus authored-override outcomes (an authored `DecompositionAttachment`
     // outranking `Inferred` replaces the derived one and is counted
-    // distinctly, mirroring the spelling buckets).
+    // distinctly, mirroring the spelling buckets), plus authored-only
+    // surfacings for inference-ineligible events (Pass 12 P12-H7,
+    // `req:pitch:authored-uninferred`).
     assert_eq!(
         ann.decompositions.len(),
-        ann.taxonomy.decompositions_inferred + ann.taxonomy.decompositions_authored,
+        ann.taxonomy.decompositions_inferred
+            + ann.taxonomy.decompositions_authored
+            + ann.taxonomy.decompositions_authored_uninferred,
         "decomposition map size disagrees with the taxonomy counts"
     );
 }

spec/operation_catalog.tex

@@ -619,7 +619,11 @@ undo (Section~\ref{sec:k0:undo}) does not negate it; an inverse-interval undo is
 Phase-3 refinement (P11-C8).
 
 \textbf{Re-anchoring.} Tombstoned targets are skipped (the transpose applies only
-to live pitches).
+to live pitches). \texttt{SYSTEM\_DERIVED}-namespace targets are likewise
+\emph{skipped} (ratified Pass~12, P12-K3): their intrinsic content is immutable,
+and an in-place alteration shift would desynchronize the content from the id's
+derivation inputs. A transpose whose live targets are \emph{all} system-derived
+reduces as a precondition no-op (\texttt{SystemDerivedContentImmutable}).
 
 \section{CreateCrossCutting}
 \label{sec:k0:create-cross-cutting}
@@ -811,9 +815,12 @@ precondition no-op with the appended reason
 \texttt{RecreateContentMismatch} (discriminant 13; ratified Pass~12, closing
 P12-K9 --- the former \texttt{TargetMissing} reuse misnamed the situation:
 the target is not missing, its content disagrees). The same reason applies
-to every differing-value re-create: the carried \texttt{TimeSignature}
+to the carried \texttt{TimeSignature} (Section~\ref{sec:k0:meter-tempo}),
-(Section~\ref{sec:k0:meter-tempo}) and the structural-container creates
+the other re-create site at which the reducer retains the carried value for
-(Section~\ref{sec:k0:structural-containers}). Graph-aware reduction additionally preconditions that the
+comparison. The structural-container creates
+(Section~\ref{sec:k0:structural-containers}) are plain set-union --- any
+repeat create of a live id reads \texttt{AlreadyApplied} without value
+comparison, since the carried value is preconditioned empty of children. Graph-aware reduction additionally preconditions that the
 referenced instrument is live and, when \texttt{group} is present, that the
 staff group resolves --- the mint must leave the graph satisfying the
 reference-resolution invariants.