docs: discharge #245's owed witnesses, and record what the first dispatch found

D3 PASS. Dispatched run 33307137965 on main: all 14 jobs started and
concluded success or failure, none skipped, cancelled or timed_out. The
run's own conclusion was failure, which D3 permits by design --- its
contract is that the matrix RAN, not that it passed.

D2 PASS, with every guard exercised rather than assumed. A reached
in_progress; B was dispatched while A ran; the REQUIRED OVERLAP WAS
OBSERVED, A in_progress and B pending, so this is not the vacuous
version that passes when A finishes first; headSha(A) == headSha(B) ==
7b82e14, so the two really shared ci-<sha>; and A concluded success, not
cancelled. B was cancelled afterwards by hand to save macOS minutes, and
its fate is not part of D2.

An unplanned observation is worth more than either witness: a main PUSH
run was already in_progress at 7b82e14 when the first dispatch was
issued, and the dispatch QUEUED BEHIND IT rather than cancelling it,
starting only once the push finished. That is the same-SHA
push/dispatch interaction the framing described and no witness covered.

The first dispatch also immediately found a red on main, which is what
the lane was built for --- and it is not like anything else in this
registry. rope_matches_crdt_projection_after_arbitrary_edits failed a
proptest assertion at src/buffer.rs:3120, "no-op edit must have crdt_op
= None (Undo)", and SHRANK to a four-operation minimal input. That is a
property violation with a concrete witness, not a load artefact. It is
recorded as its own lane with the selector, the assertion, the shrunken
ops, the regression seed, and the reason a local pass is not evidence:
no .proptest-regressions file is committed, so the failing case is not
replayed and one green local run means nothing.

Not investigated here. This lane's scope was one workflow key.

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

docs/active-work.md

@@ -270,7 +270,77 @@ hazard in a shape that looks committed. **A documented error message
 that never appears is worse than no documentation**, because the reader
 waits for a signal that is not coming.
 
-## Manual CI dispatch — ACTIVE
+## Manual CI dispatch — MERGED as #245 (`7b82e14`); D2 and D3 DISCHARGED
+
+- **MERGED 2026-08-30T10:42:18Z** at approved head `c21eee6`, merge
+  commit `7b82e14`, via `--match-head-commit`. 14/14 CI green on that
+  head; 8-stage local gate green on it too.
+- **D3 PASS** — dispatched run `33307137965` on `main`. **All 14 jobs
+  started and concluded `success` or `failure`**; none `skipped`,
+  `cancelled` or `timed_out`. The run's own conclusion was `failure`,
+  which D3 permits by design: its contract is that the matrix RAN, not
+  that it passed.
+- **D2 PASS**, with every guard the framing demanded actually
+  exercised:
+  - A = `33308891808`, dispatched and reaching `in_progress`;
+  - B = `33308921103`, dispatched while A ran;
+  - **the required overlap was OBSERVED** — A `in_progress`, B
+    `pending` — so the witness is not the vacuous version that passes
+    when A finishes first;
+  - `headSha(A) == headSha(B) == 7b82e14`, so both really shared
+    `ci-<sha>`;
+  - **A concluded `success`, not `cancelled`.**
+  - B was cancelled by hand afterwards to save macOS minutes; B's fate
+    is not part of D2.
+- **An unplanned observation, worth more than either witness.** A
+  `main` PUSH run was already `in_progress` at `7b82e14` when the first
+  dispatch was issued. The dispatch **queued behind it and did not
+  cancel it**, then started when the push finished. That is the
+  same-SHA push/dispatch interaction §5a described and no witness
+  covered.
+- **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
+
+**Found by the first `workflow_dispatch` run**, `33307137965`, job
+`99247616970`, at `main` = `7b82e14`. Log preserved at
+`/home/jeans/build/pmacs-ci-logs/`.
+
+- **Selector:** `--lib --features crdt
+  buffer::tests::proptests::rope_matches_crdt_projection_after_arbitrary_edits`
+- **Assertion:** `src/buffer.rs:3120` —
+  `no-op edit must have crdt_op = None (Undo)`
+- **`2172 passed; 1 failed`**, failing after 17 successes.
+
+**THIS IS NOT LIKE THE OTHER ROWS IN THIS REGISTRY.** Every red this
+session has been timing-dependent and green on rerun. This one is a
+**proptest failure that SHRANK to a minimal input**, which means it is
+a property violation with a concrete witness, not a load artefact:
+
+```
+ops = [ Insert(0, "aa"), Insert(2, "aaa "), Replace(5, 1, " "), Undo ]
+```
+
+proptest also emitted its regression seed:
+`cc fbc94ffbf80519d277eb49aa7ee46c726e1adc3a319d44cf32509d122d6ab5be`
+
+- **It did NOT reproduce in one local `--features crdt` run**, which
+  proves nothing: proptest draws fresh cases each run and **no
+  `.proptest-regressions` file is committed** for `src/buffer.rs`, so
+  the failing case is not replayed automatically.
+- **The reproduction path is therefore known and cheap**: drive the
+  shrunken `ops` sequence directly as a unit test, or commit the
+  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
+a CRDT/undo property violation is nowhere near it. Recorded with
+everything needed to start: selector, assertion, minimal input, seed,
+and the reason a local pass is not evidence.
+
+### Superseded lane state, kept for the record
 
 **Written with the branch's FIRST commit**, per the standing correction
 from #171 and #215.