Agent K M1 review follow-up: correct two doc-accuracy findings

From the M1 review (no correctness bugs found; these are accuracy corrections to
shipped artifacts, not new feature work):

- migration gate: the `v1 == migrated` assertion's comment overclaimed a
  universal inverse. It is round-trip self-consistency over the representative
  corpus (which is built from the same valuegen helpers the migration
  reconstructs values with); the spec-level property is the reduction-equivalence
  asserted alongside it. The ReplaceWithRest rest-voice is the known
  non-invertible field, recovered from the deleted event's placement at reduction.
- operation_catalog §CreateCrossCutting: document that v0→v1 migration covers the
  event-anchored Tie/Slur/Beam; a Spanner (anchor-based) cannot be reconstructed
  from the v0 event-reference and is reported unmigratable (read-only) under M1,
  so the catalog no longer silently implies it round-trips.

Review findings deferred to M2 (per project lead): migrate.rs unit tests for the
untested reconstruction branches, and the valuegen::spelling() mod-7 domain
cleanup. Gates unchanged and green (comment + spec-text only).

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

crates/epiphany-testkit/src/migration.rs

@@ -77,11 +77,18 @@ pub fn run_migration_equivalence(n_ops: usize, seed: u64) {
         "v0->v1 migration changed the canonical reduction state (seed {seed})"
     );
 
-    // The migration faithfully inverts the projection on the representative
-    // payloads (a stronger property than reduction-equivalence alone).
+    // Round-trip self-consistency over *this* corpus: because the corpus is
+    // built from the same `valuegen` helpers the migration reconstructs values
+    // with, `migrate(project(env)) == env` holds exactly here. This is a sharper
+    // check than reduction-equivalence for the corpus, but it is NOT a universal
+    // inverse: the v0 projection drops fields the migration cannot recover (e.g.
+    // a `ReplaceWithRest` rest's own voice — recovered from the deleted event's
+    // placement at reduction, not from the value). The spec-level property is the
+    // reduction-equivalence asserted above; widening `operation_envelopes` to emit
+    // such a payload would surface here and is M2's cue to revisit faithfulness.
     assert_eq!(
         v1, migrated,
-        "migration is not the inverse of projection (seed {seed})"
+        "migration round-trip diverged from the original on this corpus (seed {seed})"
     );
 
     // Deterministic: migrating the same projection against the same context

spec/operation_catalog.tex

@@ -500,6 +500,15 @@ policy.
 \textbf{Re-anchoring.} The structure participates in the re-anchoring rule table
 when one of its endpoints is later tombstoned (see DeleteEvent).
 
+\textbf{Migration coverage.} The v0$\rightarrow$v1 migration
+(Chapter~\ref{ch:migration}) reconstructs the event-anchored \texttt{Tie},
+\texttt{Slur}, and \texttt{Beam} from the v0 reference (id plus event endpoints).
+A \texttt{Spanner} is anchored by \texttt{TimeAnchor}s rather than a fixed pair
+of event endpoints, so its full value is not reconstructable from the v0
+event-reference projection; a \texttt{Spanner}-create is therefore reported
+unmigratable (read-only) under M1, alongside the respell case of P12-K1. A
+faithful spanner migration joins when the projection carries the anchors --- M2.
+
 \section{ChangeRegionTimeModel}
 \label{sec:k0:change-region-time-model}