docs: correct the purge's reachable-leak claim; record the 3a lane

Rev 5 said acceptance 34's second edge was a killed buffer. Implementing
it showed that is false: the Rust core fires exactly five hooks —
buffer.after-edit, buffer.after-load, buffer.after-switch,
frontend.detached, process.after-tick — and there is **no buffer-kill
hook**, so lsp.lua never tears an attachment down and the drain keeps
reaching that server. The premise (the drain builds its sid list from
`attachments`) was right; the inference needed attachments to be removed
on kill, and nothing removes them.

The reachable leak has the same root cause by a different path.
`attach_buffer` drops a sid from `attachments` the moment
`server_is_live` reports false and rebuilds against a fresh server — so
`crashed` / `stopped` is the event *least* likely to be drained, and an
event-driven purge leaks in exactly the case it exists for. The purge
therefore polls `pmacs.lsp.list()`, which enumerates the manager
directly. Acceptance 34's second half now exercises a server in **no**
attachment, which is the shape that discriminates: bitten, an
event-driven purge fails it while the attached case still passes.

§0.1 finding 6, Q#LN9, and acceptance 34 all updated; the wrong wording
is left visible with its correction rather than quietly replaced, since
the mistake is the useful part.

Ledger gains the Stage 3a lane: branch, worktree, what ships, both
corrected claims, the `install_async` load-order trap, the recorded
bites, the one knowingly unpinned guard, and gate results.

docs/active-work.md

@@ -54,7 +54,7 @@ git status --short --branch
 The `git log` command must expose `0dd16a5` or a newer intentional main.
 If it does not, stop and repair the remote/fetch configuration.
 
-## Lean 4 lane (Arc 8) — Stage 1 MERGED; Stage 2 IN REVIEW (PR #161)
+## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; Stage 3a IN REVIEW
 
 - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
   round, all twelve checks green). Branch `githubsucks/lean4-stage1`
@@ -188,6 +188,58 @@ If it does not, stop and repair the remote/fetch configuration.
   suites**; `git diff --check` clean. The sweep needs an isolated
   `XDG_CONFIG_HOME` and `-- --skip basedpyright`.
 
+### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` (branch `lean4-stage3a-seams`)
+
+- Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @
+  `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first
+  two commits, then the implementation, then a bite-driven correction.
+- **Stage 2 merged as #161** (`main` @ `46a1b8f`, 2026-07-25, two review
+  rounds). COHERENCE.md §7 records the slice; §1.2 records the dead
+  `pmacs.error` channel found landing it.
+- **Framing rev 5 splits Stage 3 into 3a and 3b** because rev 4 broke its
+  own §4 rule — the row read "two `lsp.lua` generalizations" under prose
+  claiming Stage 3 was Lean-only. One generalization shipped as Stage 2;
+  the other (Q#LN9's seams) is the shared event drain, so it is now its
+  own substrate stage. 3a and 3b are **strictly sequential** — 3b's
+  subscriber is written against 3a's seam and both touch `lsp.lua`.
+- Ships: `pmacs.lsp.on_notification` / `on_response`, two arms in
+  `handle_server_requests`, a pending-response purge, and
+  `pmacs.fs.canonicalize` (Q#LN20). No protocol change, no Lean content.
+- **Two framing claims were corrected during implementation**, both
+  recorded in §0.1 finding 6 and in the round-2 commit:
+  1. The reachable leak is **not** a killed buffer. The Rust core fires
+     exactly five hooks (`buffer.after-edit`, `buffer.after-load`,
+     `buffer.after-switch`, `frontend.detached`, `process.after-tick`) —
+     **there is no buffer-kill hook**, so nothing tears an attachment
+     down and the drain keeps reaching that server. The real path is
+     `attach_buffer` dropping a dead sid from `attachments` and
+     rebuilding against a fresh server, which makes `crashed`/`stopped`
+     the event *least* likely to be drained. Hence the purge polls
+     `pmacs.lsp.list()` rather than riding the drain.
+  2. Acceptance 32 does **not** pin "removed before invocation" —
+     `pcall` catches the raise either way, so before/after is
+     unobservable without a re-entrant drain. It pins removal being
+     **unconditional**; renamed accordingly.
+- **`pmacs._fs` is installed from `install_async`, not `install_project`**,
+  purely for load order: `make_workspace` runs *after* `fs.lua` is
+  evaluated, so a canonicalizer placed there reads nil. This cost one
+  failing run to discover and is the kind of thing to check first.
+- Bites recorded (all against the committed tree): removal gated on a
+  clean return → acc32 fails 2 != 1; an event-driven purge → the
+  no-attachment case fails "never called" while the attached case still
+  passes; a resolver without `canonicalize` → two servers (34b's own
+  falsification, which ships as a test).
+- **Known unpinned:** the purge's generation (`attempt`) check. Reaching
+  it needs a crash *and* its restart to fall in a gap with no
+  `_async.tick`; the backoff is 500ms, so any tick sees `crashed` first
+  and the absent-or-terminal arm fires. Labelled as defensive in the
+  code rather than left looking covered.
+- Verification on this branch: `cargo fmt --check` clean; strict
+  workspace Clippy clean; 1,826 default + 2,003 CRDT library tests;
+  dispatch seams 14/14; multi-root 13/13; M4 121; required GPU 155;
+  **isolated-config workspace sweep 3,188 across 93 suites, zero
+  failures**; `git diff --check` clean.
+
 ## Dired lane — framing APPROVED; Stage 0 MERGED, Stage 1 next
 
 - Approved framing: `docs/dired-framing.md` (revision 5), landing as its

docs/lean4-mode-framing.md

@@ -241,11 +241,26 @@ Confirmations, recorded because each was load-bearing and unverified:
    narrowing is load-bearing.** `handle_server_requests` builds its sid
    list from `attachments`, and `push_event` appends with no cap. So a
    subscriber fires only for a server with a live attachment, and an
-   unattached server's event queue grows unboundedly. This bites
-   acceptance 34 directly: kill the buffer with a request outstanding
-   and the pending purge never runs — the leak that criterion exists to
-   prevent. Q#LN9 now states the contract and acceptance 34 drives it
-   through the buffer-kill path rather than the server-death path alone.
+   unattached server's event queue grows unboundedly.
+
+   *Corrected during implementation (rev 5, round 2).* Rev 5 first
+   claimed the reachable leak was a killed buffer. **That was wrong.**
+   The Rust core fires exactly five hooks — `buffer.after-edit`,
+   `buffer.after-load`, `buffer.after-switch`, `frontend.detached`,
+   `process.after-tick` — and **there is no buffer-kill hook at all**,
+   so `lsp.lua` never tears an attachment down and the drain keeps
+   reaching that server. The premise was right and the inference was
+   not: it needed attachments to be removed on kill, and nothing
+   removes them.
+
+   The reachable leak is a different path with the same root cause.
+   `attach_buffer` drops a sid from `attachments` the moment
+   `server_is_live` reports false, rebuilding against a fresh server —
+   so the `crashed` / `stopped` event that should trigger a purge is
+   **precisely the one most likely to go undrained**. An event-driven
+   purge leaks exactly when it matters. Q#LN9 therefore drives the
+   purge off `pmacs.lsp.list()`, which enumerates the manager directly
+   and is unaffected by attachment bookkeeping.
 7. **The `cfg.restart` gap is still open** (recorded landing #161):
    `ensure_server` never forwards `pmacs.lsp.config[lang].restart` to
    `pmacs.lsp.spawn`, so the field is silently dropped on auto-attach.
@@ -264,9 +279,9 @@ rather than a bare root), `ensure_server` 527 → **610**,
 12798 → **12827**, `pair.lua` 213 → **229**, and `compile.lua`
 264 → **266**. Verified good and left alone: `listview.lua:138`,
 `src/lsp.rs:264`, `src/diag.rs:50`, `src/process.rs:193`,
-`src/project.rs:145`, and the `mod.rs` binding-block citations. The pre-#161 line numbers inside Q#LN15 are
-left as written: that stage has landed and its citations are historical
-record, not navigation.
+`src/project.rs:145`, and the `mod.rs` binding-block citations. The
+pre-#161 line numbers inside Q#LN15 are left as written: that stage has
+landed and its citations are historical record, not navigation.
 
 ## 1. What ships
 
@@ -1018,13 +1033,24 @@ attachment.** `handle_server_requests` builds its sid list from
 `attachments`, so a server with no attached buffer is never drained — and
 `push_event` appends with no cap, so that server's queue grows
 unboundedly. Both facts are pre-existing and neither is Stage 3a's to
-fix, but the second one turns the first into a leak with a name: **a
-buffer killed while a request is outstanding never runs the purge**,
-because the purge rides the drain that the attachment was gating. That is
-the exact failure acceptance 34 exists to prevent, reachable through the
-ordinary `C-x k`. So the purge is driven from both edges — the server-death
-transition *and* attachment teardown — and acceptance 34 exercises the
-buffer-kill path, which is the one a user can actually reach.
+fix. What they change is where the purge may be wired.
+
+**The purge must not ride the drain.** `attach_buffer` removes a sid
+from `attachments` as soon as `server_is_live` reports false and rebuilds
+the attachment against a fresh server, so a `crashed` / `stopped` event
+is the event *least* likely to be drained — the drain stops visiting
+that server at almost exactly the moment the event is queued. A purge
+triggered by observing that event therefore leaks in the case it exists
+to handle.
+
+So the purge polls **`pmacs.lsp.list()`** after each drain instead. That
+call enumerates the manager directly and is unaffected by attachment
+bookkeeping, which is what makes it the right authority: a sid that is
+absent, terminal, or running a new generation settles its pending
+one-shots with an error, whether or not anything ever drained it.
+Acceptance 34's second half exercises a server that is in **no**
+attachment, because that is the shape an event-driven purge fails and a
+polled one survives.
 
 The uncapped queue is recorded as a named deferral (§6) rather than fixed
 here: bounding it is a policy question about which events may be dropped,
@@ -1629,14 +1655,16 @@ the blast radius.
   registered, `workspace/applyEdit` in the same drain is still handled;
   a raising response handler does not stop later events in that drain.
   Mirrors the notification-side pins above.
-- **34.** **Pending-purge pin, both edges.** A server that dies with a response
-  outstanding invokes the pending one-shot with an error and clears it.
-  **And** — the case round 4 found reachable and rev 4 missed — killing
-  the *buffer* with a request outstanding does the same, rather than
-  stranding the registration behind a drain that no longer runs for
-  that server. The second half must be shown to fail against a
-  purge wired only to the server-death transition; otherwise this
-  criterion is satisfied by the implementation that leaks.
+- **34.** **Pending-purge pin, both edges.** A server that dies with a
+  response outstanding invokes the pending one-shot with an error and
+  clears it. **And** a server that is in **no attachment** does the
+  same, rather than stranding the registration behind a drain that never
+  visits it. The second half must be shown to fail against a purge
+  wired to a death event seen in the drain; otherwise this criterion is
+  satisfied by the implementation that leaks. (Rev 5 first worded the
+  second edge as a killed buffer; there is no buffer-kill hook, so
+  nothing removes the attachment and that path does not leak. Corrected
+  in round 2 — see §0.1 finding 6.)
 - **34a.** **Canonicalizer pin (Q#LN20).** `pmacs.fs.canonicalize` resolves a
   symlinked and dot-segmented path to the same string as the real path,
   and returns nil for a nonexistent one. Fixture builds the symlink