Pass 13 — P13-K1: reject a ModifyEvent introducing a never-minted system pitch

The K3 verdict for a system pitch introduced by a ModifyEvent replacement
(never minted — the collision pre-walk excludes ModifyEvent) differed across a
snapshot cut: in-session it slipped through (system_mints had no entry, so the
P12-K3 identity check saw nothing), yet post-snapshot it read
SystemDerivedContentImmutable once the pitch was re-seeded as a system mint.

Per the user's call ("reject the introduction"): modify_event now refuses a
replacement carrying a never-minted SYSTEM-DERIVED pitch id (replica
SYSTEM_DERIVED, not Live in objects) with TargetMissing, before the identity
check. The verdict no longer depends on the registry — the pitch is not live in
objects in either frame — so both refuse identically, closing the asymmetry.

Scoped to the system namespace, where the asymmetry lives (only system pitches
re-seed as system mints): a user-replica pitch carries no namespace claim and
has no snapshot asymmetry, so ModifyEvent may still introduce user pitch
content (the concurrent-modify tests rely on it).

Regression: a_modify_event_introducing_a_never_minted_system_pitch_is_refused_
p13_k1. 938 tests, convergence/conformance green. PASS13: P13-K1 resolved.

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

crates/epiphany-ops/DECISIONS.md

@@ -965,16 +965,25 @@ each fixed with a regression test:
    `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
+**Pass-13 candidate (P13-K1) — resolved (Pass 13, 2026-07-08; user: "reject
-pitch *introduced by a ModifyEvent replacement value* (never minted — the
+the introduction").** The K3 verdict for a system pitch *introduced by a
-collision pre-walk deliberately excludes ModifyEvent) differs across a
+ModifyEvent replacement value* (never minted — the collision pre-walk excludes
-snapshot cut: in-session the pitch is not Live (`TargetMissing`); after a
+ModifyEvent) differed across a snapshot cut: in-session the pitch was not Live
-snapshot re-seeds objects + registry from the base graph, the same modify
+(slipped through — `system_mints` had no entry, so the identity check saw
-reads `SystemDerivedContentImmutable`. The asymmetry **predates K3** (the
+nothing); after a snapshot re-seeded objects + registry from the base graph,
-same split previously read `TargetMissing` vs a silent `Applied` rewrite) and
+the same modify read `SystemDerivedContentImmutable`.
-is a ModifyEvent-introduction question — whether a replacement value may
+
-introduce never-minted pitch ids at all — batched for Pass 13, not
+Resolved by rejecting the introduction: `modify_event` now refuses a
-improvised here.
+replacement that carries a **never-minted system-derived pitch id** (replica
+`SYSTEM_DERIVED`, absent-or-not-Live in `objects`) with `TargetMissing`,
+*before* the P12-K3 identity check. The verdict no longer depends on the
+registry — the pitch is not live in `objects` in either frame — so both frames
+refuse identically, closing the asymmetry. Scoped to the system namespace
+(where the asymmetry lives: only system pitches are re-seeded as system mints):
+a user-replica pitch carries no namespace claim and has no snapshot asymmetry,
+so `ModifyEvent` may still introduce user pitch content (the concurrent-modify
+tests rely on it). Locked by
+`a_modify_event_introducing_a_never_minted_system_pitch_is_refused_p13_k1`.
 
 ## Schema major 2: minimal stamping (landed with core Phase B, deliberately)
 

crates/epiphany-ops/src/reduce.rs

@@ -5215,11 +5215,37 @@ impl<'a> Reducer<'a> {
             }
             Some(ObjectState::Live) => {}
         }
+        let mut carried = Vec::new();
+        op.event.collect_identified_pitches(&mut carried);
+        // Introduction precondition (P13-K1, ratified: reject the
+        // introduction) before the identity one: a `ModifyEvent` may not
+        // *introduce* a never-minted SYSTEM-DERIVED pitch id — that id lives in
+        // the reserved system namespace and only the system mints it. A carried
+        // system-derived pitch absent from `objects` (never minted) is refused,
+        // consistently across a snapshot cut: this closes the asymmetry where
+        // an introduced system pitch slipped through in-session (`system_mints`
+        // had no entry, so the identity check below saw nothing) yet read
+        // `SystemDerivedContentImmutable` once a snapshot re-seeded it as a
+        // system mint. A user-replica pitch carries no such namespace claim and
+        // has no snapshot asymmetry, so it is untouched here; the event's own
+        // live system pitches are in `objects` (both reduction modes), so an
+        // in-place content rewrite passes.
+        if carried.iter().any(|ip| {
+            ip.id.replica() == ReplicaId::SYSTEM_DERIVED
+                && !matches!(
+                    self.objects.get(&TypedObjectId::Pitch(ip.id)),
+                    Some(ObjectState::Live)
+                )
+        }) {
+            return OperationEffect::NoOp {
+                reason: NoOpReason::PreconditionFailedUnderReduction {
+                    reason: PreconditionFailureReason::TargetMissing,
+                },
+            };
+        }
         // 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))
@@ -9485,6 +9511,62 @@ mod tests {
         );
     }
 
+    #[test]
+    fn a_modify_event_introducing_a_never_minted_system_pitch_is_refused_p13_k1() {
+        // P13-K1 (ratified: reject the introduction). The INTRODUCTION sibling
+        // of the p12_k3 rewrite refusal: a ModifyEvent whose replacement
+        // carries a *never-minted* system-derived pitch id is refused
+        // (`TargetMissing`) — the system namespace is the system's to mint.
+        // Before the fix this slipped through in-session (`system_mints` had no
+        // entry, so the identity check saw nothing) yet read
+        // `SystemDerivedContentImmutable` after a snapshot re-seeded the pitch
+        // as a system mint — the snapshot-cut asymmetry the candidate named.
+        // The verdict no longer depends on the registry: the pitch is not live
+        // in `objects` in either frame, so both refuse identically.
+        use epiphany_core::derive_system_pitch_id;
+        let content = crate::valuegen::pitch_value_nth(3);
+        let system_id = derive_system_pitch_id(&content); // never minted
+
+        // A live, pitchless event modified to CARRY the never-minted system
+        // pitch (an introduction, not an in-place rewrite).
+        let insert = insert(1, 0, 10, 1, 100, 0);
+        let replacement = crate::valuegen::insert_event_value(
+            EventId::new(ReplicaId(1), 100),
+            VoiceId::new(ReplicaId(9), 1),
+            pos(0),
+            epiphany_core::MusicalDuration::whole(),
+            &[system_id],
+        );
+        let modify = prim_env(
+            1,
+            1,
+            20,
+            seen_r1(0),
+            OperationKind::ModifyEvent(ModifyEventOp { event: replacement }),
+        );
+        let mut set = OperationSet::new();
+        set.accept_all(vec![insert, 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::TargetMissing,
+                },
+            }),
+            "a ModifyEvent introducing a never-minted system pitch is refused"
+        );
+        assert!(
+            !state.objects.contains_key(&TypedObjectId::Pitch(system_id)),
+            "the introduced system pitch never enters the ledger"
+        );
+    }
+
     #[test]
     fn a_rank_four_reanchor_records_same_canvas_nearer_p12_c4() {
         // Pass 12 (P12-C4): the rank-4 (same-canvas) proximity survivor has

spec/PASS13_CANDIDATES.md

@@ -7,7 +7,7 @@ this file is the index, not the analysis.
 
 | Id | One-line statement | Filed in | Status |
 |---|---|---|---|
-| P13-K1 | The K3 verdict for a system pitch introduced by a ModifyEvent replacement value differs across a snapshot cut (in-session `TargetMissing` vs post-snapshot `SystemDerivedContentImmutable`); really "may ModifyEvent introduce never-minted pitch ids" | `crates/epiphany-ops/DECISIONS.md` (Pass-12 G-pass code tranche) | open |
+| P13-K1 | The K3 verdict for a system pitch introduced by a ModifyEvent replacement value differs across a snapshot cut (in-session `TargetMissing` vs post-snapshot `SystemDerivedContentImmutable`); really "may ModifyEvent introduce never-minted pitch ids" | `crates/epiphany-ops/DECISIONS.md` (Pass-12 G-pass code tranche) | **resolved** (Pass 13: reject the introduction — modify_event refuses a never-minted system-derived pitch, verdict now snapshot-cut-invariant; user "reject the introduction") |
 | P13-D1 | Undo-driven event tombstones run graph-side re-anchor/cascade but never ledger-side `reanchor_for_tombstone`: structures leave the graph while staying `Live`, no `RepairRecord` — Ch6's same-step recording MUST is unmet for undo-driven tombstones (pre-existing class: slurs/spanners; repeats now too) | `crates/epiphany-ops/DECISIONS.md` (Schema major 2, Phase D) | open |
 | P13-D2 | Cue-cascade recursion re-anchors against the triggering event before its tombstone lands in `objects`: a structure anchored on {X, cue-of-X} can record `Reanchored{to: X}` then `CascadeDeleted` in one effect (contradictory repair trail; plausible by code trace, unexecuted) | `crates/epiphany-ops/DECISIONS.md` (Schema major 2, Phase D) | open |
 | P13-D3 | `CreateCrossCutting` validates only event endpoints (`CrossCuttingValue::endpoints()`), so a SPANNER anchored to a missing region/measure mints dangling past `anchor_target_exists`; and non-event referent tombstones (`DeleteRegion` under a region-anchored spanner/repeat) re-anchor nothing — "every referenced endpoint is live" is events-only as implemented | `crates/epiphany-ops/DECISIONS.md` (Phase D follow-up) | **resolved** (Pass 13: mint fixed via `anchor_object_refs`; non-event referent re-anchoring ratified events-only, user "fix the mint only") |