docs: the dispatched red is known #157, not a new defect

I recorded the dispatched run's proptest red as "a DETERMINISTIC red",
"not like anything else in this registry --- a property violation with a
concrete witness, not a load artefact", and proposed committing the
proptest seed as the first step. All of that was wrong, and it was wrong
for a plain reason: I recorded a finding without checking whether main
already documented it.

src/buffer.rs:3005 carries an #[ignore]d deterministic fixture,
crdt_undo_of_an_identity_replace_reports_a_no_op_edit_carrying_an_op,
that reduces this exact case. The shrunken input is a randomly sampled
recurrence of it: Replace(5, 1, " ") replaces the trailing space with
itself, a textual no-op but a real CRDT delete-plus-insert, so Undo
emits a version-advancing operation with no visible text change.

Committing the seed was a second error. It duplicates a deterministic
fixture that already exists and would only make a disputed assertion
fail permanently instead of occasionally.

The fixture already verified what I would have re-derived: content stays
correct, replicas stay converged because the op IS broadcast and neither
crdt_op consumer short-circuits on an empty range, and the cursor does
not jump.

The entry now frames the actual decision --- whether a visible text delta
and a CRDT-version delta are independent dimensions of Edit --- and the
evidence a lane owes: that forward textual no-ops still produce no
operation, that any permitted empty-text undo operation carries valid
bytes and preserves remote replay convergence, and an explicit
disposition of derive_replacement_edit reporting the empty range at the
buffer end rather than the edit site.

The interruption is bounded and does not reorder the roadmap. GUI arc 1b
remains the next product lane.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai

docs/active-work.md

@@ -301,44 +301,66 @@ waits for a signal that is not coming.
 - **THE FIRST DISPATCH IMMEDIATELY FOUND A RED ON `main`**, which is
   what this lane was built for. See the proptest entry below.
 
-## CRDT undo proptest — a DETERMINISTIC red on `main` — NEEDS A LANE
+## CRDT identity-replace undo — the proptest invariant may be MIS-SCOPED — NEEDS A LANE
 
-**Found by the first `workflow_dispatch` run**, `33307137965`, job
+**CORRECTION.** An earlier version of this entry called the dispatched
-`99247616970`, at `main` = `7b82e14`. Log preserved at
+run's red "a DETERMINISTIC red" and "not like anything else in this
-`/home/jeans/build/pmacs-ci-logs/`.
+registry — a property violation with a concrete witness, not a load
+artefact", and proposed committing the proptest seed as the first
+step. **All of that was wrong**, and it was wrong because I recorded a
+finding without checking whether `main` already documented it.
 
-- **Selector:** `--lib --features crdt
+**It is a randomly sampled recurrence of known #157 behaviour.**
-  buffer::tests::proptests::rope_matches_crdt_projection_after_arbitrary_edits`
+`src/buffer.rs:3005` carries an `#[ignore]`d deterministic fixture,
-- **Assertion:** `src/buffer.rs:3120` —
+`crdt_undo_of_an_identity_replace_reports_a_no_op_edit_carrying_an_op`,
-  `no-op edit must have crdt_op = None (Undo)`
+which reduces this exact case and records its mechanism:
-- **`2172 passed; 1 failed`**, failing after 17 successes.
 
-**THIS IS NOT LIKE THE OTHER ROWS IN THIS REGISTRY.** Every red this
+1. the inserts produce `aaaaa `;
-session has been timing-dependent and green on rerun. This one is a
+2. `Replace(5, 1, " ")` replaces the trailing space **with itself** — a
-**proptest failure that SHRANK to a minimal input**, which means it is
+   textual no-op but a real CRDT delete-plus-insert;
-a property violation with a concrete witness, not a load artefact:
+3. `Undo` therefore emits a **version-advancing CRDT operation with no
+   visible text change**, and `derive_replacement_edit` yields an empty
+   edit that still carries its `crdt_op`.
 
-```
+**Committing the seed is NOT the first step**, and proposing it was a
-ops = [ Insert(0, "aa"), Insert(2, "aaa "), Replace(5, 1, " "), Undo ]
+second error: it duplicates a deterministic fixture that already
-```
+exists, and its only effect would be to make a disputed assertion fail
+permanently instead of occasionally.
 
-proptest also emitted its regression seed:
+**What the fixture already verified**, so the lane does not redo it:
-`cc fbc94ffbf80519d277eb49aa7ee46c726e1adc3a319d44cf32509d122d6ab5be`
+content stays correct (rope and CRDT projection agree), replicas stay
+converged (**the op IS broadcast** — both `crdt_op` consumers read it
+unconditionally and neither short-circuits on an empty range), and the
+cursor does not jump.
 
-- **It did NOT reproduce in one local `--features crdt` run**, which
+**THE ACTUAL DECISION** is whether a **visible text delta** and a
-  proves nothing: proptest draws fresh cases each run and **no
+**CRDT-version delta** are independent dimensions of `Edit`. The
-  `.proptest-regressions` file is committed** for `src/buffer.rs`, so
+proptest's invariant assumes they are the same dimension. It was
-  the failing case is not replayed automatically.
+written for the FORWARD `apply_edit` short-circuit, which returns
-- **The reproduction path is therefore known and cheap**: drive the
+before producing an op at all — and **CRDT-mode undo/redo never reach
-  shrunken `ops` sequence directly as a unit test, or commit the
+that path**.
-  regression seed so proptest replays it.
-- **Committing that regression file may be the first thing the lane
-  does**, since without it this exact input is only reachable by luck.
 
-**Not investigated here.** This lane's scope was one workflow key, and
+**What the lane owes as evidence:**
-a CRDT/undo property violation is nowhere near it. Recorded with
+
-everything needed to start: selector, assertion, minimal input, seed,
+- **forward textual no-ops still produce NO operation** — whatever the
-and the reason a local pass is not evidence.
+  resolution, the short-circuit the invariant was actually written for
+  must keep holding;
+- **any permitted empty-text undo operation carries valid bytes and
+  preserves remote replay convergence** — permitting the shape must not
+  become permitting a malformed op;
+- **an explicit disposition of the arbitrary artifact**:
+  `derive_replacement_edit` reports the empty range at the **buffer
+  end** rather than at the edit site. The fixture calls this genuinely
+  arbitrary either way; the lane must say which it is choosing, not
+  leave it unexamined.
+
+**Un-ignoring that fixture is the first step of whichever resolution
+wins**, as its own doc comment says.
+
+**Why it is worth a bounded interruption:** a mis-scoped property can
+now randomly redden `main`, and the dispatched run proved it. **It does
+NOT reorder the roadmap** — GUI arc 1b remains the next product lane
+per `COHERENCE.md` §20's priority order.
 
 ### Superseded lane state, kept for the record