diff --git a/docs/active-work.md b/docs/active-work.md
index 52d44ba..47c3677 100644
--- a/docs/active-work.md
+++ b/docs/active-work.md
@@ -1,6 +1,6 @@
 # Active work — cross-machine resume ledger
 
-**Snapshot: 2026-07-25.** This file records volatile work that has not
+**Snapshot: 2026-07-26.** This file records volatile work that has not
 landed on `main`. Read it after `docs/agent-handoff.md`. Remove completed
 entries when their PR merges; do not let this become a second permanent
 backlog.
@@ -59,421 +59,40 @@ If it does not, stop and repair the remote/fetch configuration.
 
 ## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING
 
-- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
-  round, all twelve checks green). Branch `githubsucks/lean4-stage1`
-  retained; it was worked in the shared checkout (no sibling worktree).
-- Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as
-  the branch's first commit (`a382965`) after three review rounds. **Seven
-  stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star:
-  match or exceed VS Code's Lean support.
-- **Stage 1 implemented; no wire change (protocol stays v20), no LSP, no
-  frontend change.** Four commits: framing, grammar, theme captures,
-  editing surface + acceptance.
-  - `Cargo.toml` + `src/syntax.rs`: `arborium-lean` 2.18 and one
-    `BUILTIN_LANGUAGES` entry named **`lean4`** (Q#LN2 — the name becomes
-    the `didOpen` language_id), claiming `.lean` only.
-  - `src/highlight.rs`: four capture entries — `constructor`, `character`,
-    `keyword.conditional`, `warning`.
-  - `builtin/runtime/{comment,pair,syntax}.lua`: `--` comments, the
-    `⟨⟩ ⦃⦄ ⟮⟯` pair set, the `lean` → `lean4` modeline alias.
-  - `tests/lean4_stage1_acceptance.rs` plus unit tests in `syntax.rs` /
-    `highlight.rs`: 12 criteria, 17 tests.
-- **Q#LN1's open obligation is discharged.** `tree-sitter-lean4` is
-  unusable (depends on `tree-sitter ^0.25` directly against our 0.26,
-  exports no `LANGUAGE` const despite its README, packages no queries);
-  `arborium-lean` rides `tree-sitter-language 0.1` with a pre-generated
-  ABI-15 parser. `cargo tree -d` shows no duplicate core. The parse smoke
-  pins the failure mode that matters: `→`/`∀`/`≥` must produce
-  `(arrow)`/`(forall)`/`(comparison)`, since a mismatched-core build
-  degrades silently on exactly those characters rather than failing loudly.
-- **Q#LN4 is a deliberate retro-paint of seven language entries**, not
-  four: `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated
-  base-first into javascriptreact/typescript/typescriptreact. Its shape is
-  "every capitalized identifier" (`#match? "^[A-Z]"`) plus every Lua table
-  brace — not "constructors". Pinned in both directions per #146.
-- Implementation findings not in the framing:
-  - `warning` had to move from bold red to bold **bright** red: `number`
-    is plain `fg(1)`, so `sorry` and an adjacent numeric literal were the
-    same colour. Found by writing the test.
-  - `Some(1)` is **not** `@constructor` — in call position a narrower
-    `@function` pattern wins. Only bare or pattern-position capitalized
-    identifiers reach it. Pinned so the blast-radius claim stays honest.
-  - Lean node kinds nest: `module > declaration > def|theorem`.
-  - `pmacs.parse.injection_aliases` is a documented **write-only** Lua
-    proxy (canonical map is Rust-side), so fence tests must drive
-    `_parse_now` and inspect layer languages, never read the table back.
-- **Review round 1 addressed.** The finding: acc12's server-list assertion
-  could not fail for the regression it named — the shared `editor()`
-  helper wipes `pmacs.lsp.config` before any buffer opens, so
-  `#pmacs.lsp.list() == 0` holds for every language regardless of what
-  Stage 1 ships. It now asserts against a **pristine** `EditorState` that
-  `pmacs.lsp.config.lean4` is nil, with a non-vacuity check that the same
-  lookup finds `rust`; bite-verified by adding a `lean4` config to
-  `lsp.lua` and watching it fail. Also fixed a stale column in a
-  `highlight.rs` comment.
-- Verification on this branch: `cargo fmt --check` clean; strict workspace
-  Clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1
-  9/9; comment toggle 14; auto-pair 45; injection 4; M4 121; required GPU
-  152; **isolated-config workspace sweep 3,150 across 90 suites**;
-  `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME`
-  for the reason recorded in the bottom-panel lane below.
-### Stage 2 — multi-root LSP server affinity (Q#LN15)
+- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`),
+  #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full
+  histories were pruned from this ledger in round 6, per this file's own
+  instruction to remove entries when their PR merges; the durable facts
+  now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where
+  a fresh machine should read them. `docs/lean4-mode-framing.md` rev 7
+  carries the decisions.
 
-- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout,
-  based on `githubsucks/main` @ `0827dd1`. Named for the substrate, not
-  for Lean: **the diff contains no Lean content**, because `ensure_server`
-  is the one server-affinity function every LSP language shares and a
-  cross-cutting change to it must not be reviewable only as a Lean
-  feature.
-- Three files, no protocol change: `src/lua_bindings/mod.rs` (the
-  `lsp.list()` row builder gains `root_uri` + `cwd`),
-  `builtin/runtime/lsp.lua` (`project_root_for` returns `root, source`;
-  `ensure_server` hoists it above the reuse loop and matches on it),
-  `tests/lsp_multi_root_acceptance.rs` (9 tests, acceptance 13–21).
-- **The rule that keeps this from regressing every other language: the
-  affinity key is the root only when a root was actually FOUND.**
-  `project_root_for` never returns nil for a file with a path — its last
-  resort is the file's own directory — so a naive `(language_id, root)`
-  key gives every directory of loose scratch files its own server, for
-  every language. `source` is `"config" | "detected" | "fallback"` and
-  only the first two become a key.
-- **Wire-identical for the fallback case, and that is provable rather
-  than hoped.** Matching is on the spawned spec's `root_uri` (nil matching
-  nil), so the fallback spawn passes `root_uri = nil`; `cwd` still carries
-  the directory and `build_initialize` derives the identical `rootUri`
-  from `cwd` when the field is None, using a percent-encoder with the same
-  allowed set as Lua's `file_uri_for`. `build_initialize` (`src/lsp.rs`)
-  is the **only** reader of `spec.root_uri` in the tree.
-- Deliberate behavior change, asserted not discovered: a server
-  hand-spawned from `init.lua` with only `cwd` set also reads back nil, so
-  a root-bearing attach will not adopt it.
-- `config[language].root` may now be a `function(path) -> string|nil`,
-  memoized per directory — needed because the hoist puts root resolution
-  on every attach rather than every spawn. The memo is keyed **weakly by
-  the resolver function itself**, so replacing `config[lang].root` cannot
-  serve a root the previous resolver computed. This is Q#LN8's
-  generalization landing early; the Lean resolver that uses it is Stage 3.
-- Bite-verified three ways: 5/9 fail against the pre-change `lsp.lua`,
-  8/9 against the pre-change `mod.rs`, and — the one that matters most —
-  installing the naive always-key-on-root variant fails acceptance 20 and
-  21 exactly as Q#LN15 part 2 predicts. The four that survive the first
-  bite (13, 15, 16, 19) are the regression pins; passing on both sides is
-  their job.
-- Every fixture sets `pmacs.project.set_search_boundary` at its own
-  tempdir root. Without it the marker walk climbs to the filesystem root
-  and a stray `.git` above the temp directory turns the markerless cases
-  into detected ones — the assertions would still pass while testing
-  nothing.
-- **Found but not fixed here (pre-existing, own lane):** `ensure_server`
-  never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a
-  `restart = "never"` in `pmacs.lsp.config[lang]` is silently dropped on
-  the auto-attach path. At least one existing test sets it believing it
-  takes effect. Out of scope for a PR whose acceptance 16 pins existing
-  attach behavior as unchanged.
-- **Review round 1 addressed.** The blocker was process, not design: the
-  test file was committed *before* `cargo fmt` ran, so the fix sat
-  uncommitted in the working tree and the branch as pushed failed the
-  first gate. The reported "fmt clean" described the worktree, not the
-  branch — gate results are only meaningful when run against the pushed
-  tree. Also added the two pins review asked for (a **string** `config
-  .root` as an affinity key — acc17 only covered the function form; and
-  `root = false` reading as unset), each bite-verified against exactly
-  the mutation it targets and neither against the other. And documented
-  the canonicalization obligation: the `"detected"` arm is canonicalized
-  for free, a **configured** root is not, so on macOS a resolver
-  returning `/var/…` and a detected `/private/var/…` are different keys
-  for one directory. Stage 3's Lean resolver is the first real consumer,
-  so the obligation is written at the point of use.
-- Verification on this branch: `cargo fmt --check` clean; strict
-  workspace Clippy clean; 1,826 default + 2,003 CRDT library tests;
-  multi-root 11/11; M4 121; statusline 7; completion popup 9; auto-pair
-  45; required GPU 155; **isolated-config workspace sweep 3,164 across 91
-  suites**; `git diff --check` clean. The sweep needs an isolated
-  `XDG_CONFIG_HOME` and `-- --skip basedpyright`.
-
-### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` — MERGED #167 (`main` @ `6f348c9`)
-
-- 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 15/15 on Linux (14 on macOS — see below); multi-root
-  13/13; M4 121; required GPU 155; **isolated-config workspace sweep
-  3,189 across 93 suites, zero failures**; `git diff --check` clean.
-- **Two flakes/portability facts from CI round 1, both worth keeping:**
-  1. `composition_overhead_under_ten_percent` tripped once in a local
-     sweep at 18.8% against a 10% budget, then passed 3/3 in isolation
-     here, passed in isolation on main, and passed a full sweep rerun.
-     The tell is in its own output: the same run reported realistic-frame
-     overhead as **-4.6%**, and a negative figure is measurement noise,
-     not added work. Load-sensitive under a parallel `--workspace` run.
-  2. **A non-UTF-8 filename fixture cannot be built on macOS.** APFS
-     enforces valid UTF-8, so `std::fs::write` fails with EILSEQ
-     ("Illegal byte sequence") before the code under test is reached.
-     `#[cfg(unix)]` is NOT sufficient for such a fixture —
-     `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn.
-
-### Stage 3b — the Lean language server — MERGED #170 (`main` @ `d400f30`)
-
-- Same worktree `../pmacs-lean-stage3`, **branched off
-  `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response
-  seam and `pmacs.fs.canonicalize`, so it is strictly sequential.
-  **Retarget PR #170 to `main` BEFORE merging #167, not after** — the
-  kill-ring lesson exactly. (Round 1 of this ledger entry stated the
-  reverse in its first sentence and the correct rule in the next; the
-  review caught it. A safety rule written twice with opposite senses is
-  worse than not written.)
-- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in
-  `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`,
-  a `leanprogress` mode plus `waitForDiagnostics` validation on
-  `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (40 tests).
-  No protocol change.
-- **Stage 1's acceptance 12 is half superseded and was rewritten, not
-  deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a
-  Stage-3 front-run; 3b is that stage. What survives is the restraint
-  half — constructing an editor spawns nothing though the config now
-  names `lake`, and opening a Lean buffer with no server configured
-  spawns nothing — which is what holds Q#LN7's "not at init" promise.
-- **The marker test is wrong in two opposite directions if done naively**
-  and both are pinned: `io.open` SUCCEEDS on a directory (so truthiness
-  accepts a `lean-toolchain` dir), but requiring a non-nil read rejects
-  an EMPTY `lean-toolchain` (a legitimate marker — existence semantics,
-  not content). Discriminator is `read`'s SECOND return; decline only on
-  a non-nil err. Probed on LuaJIT 2.1.
-- **Fifteen bites recorded, each against the committed tree.** R1: bare
-  `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a
-  passes; no canonicalization → symlinked open spawns two servers; no
-  re-attach after the swap → three latch tests fail; hook keyed on the
-  attachment → the missing-`lake` case fails; `waitForDiagnostics`
-  without `version` → acc37 fails with InvalidParams. R2: skip retiring
-  a terminal server → `attempt` reaches 3; no originating-buffer gate →
-  the Lean buffer is left on the `lake` stub; retry-forever → the
-  failing-fallback test fails; version-probe any command → the
-  working-wrapper test fails; no disabled guard → the unconfigured test
-  sees "`nil` could not be started". R3: verdict keyed on `watching` →
-  the late-verdict test finds the buffer still on `lake`; `buf_key`
-  rewritten per load → the second-buffer test fails; hardcoded
-  `lake serve` → the wrapper-naming test fails.
-- **Round-2 review: three more P1 lifecycle defects, suite 20/20 with
-  all of them live.** (1) The crashed primary respawned forever —
-  skipping the retire call avoided corrupting terminal servers but left
-  `next_restart_at` armed. **`forget` is the call for a TERMINAL server**
-  (it requires terminal state and removes the client, dropping the
-  restart timer); `stop` is for a live one and corrupts a terminal one.
-  (2) Re-attachment targeted whatever buffer was active when the async
-  verdict landed; an unrelated Rust attachment satisfied "a different
-  server id". (3) A failing fallback retried every tick forever, silent.
-  Plus two P2s: the Lake version parser was applied to arbitrary wrapper
-  output, and an UNCONFIGURED `config.lean4` was reported as failure and
-  latched, poisoning the session.
-- **Round-3 review: two more P1s, both asynchronous correlation, suite
-  25/25.** (a) `probe.watching` is cleared when the server initializes,
-  so a SLOW version verdict arrived with nil and retired nothing —
-  `_attach_buffer` returned the still-live primary and the retry called
-  it success, so status and config said "fell back" while the buffer
-  stayed put. **That is the round-1 silent no-op reached through a third
-  event ordering.** `probe.primary` is now separate from
-  `probe.watching` and survives initialization. (b) `buf_key` was
-  rewritten on every Lean `after-load`, so a second Lean buffer opened
-  before the verdict became the rebuild target while the latch still
-  watched the first buffer's server. Target buffer and primary server
-  are one fact and are now armed together, once. Plus a P2: the failure
-  message hardcoded `lake serve` after the latch became
-  command-agnostic, sending wrapper users to debug the wrong binary.
-- **Round-4 review: one P1, and it is the same defect a FOURTH time.**
-  `pmacs.lsp.config.lean4` is a single global entry, so swapping its
-  command invalidates **every** Lean buffer and **every** Lean server —
-  Q#LN15 gives one per project root. Rounds 1–3 each fixed the repair
-  for one buffer and one server; round 4 is "repair the armed target,
-  strand the rest". The shape that finally holds: retire ALL `lean4`
-  servers on latch, and repair each buffer **lazily and at most once**
-  when it becomes active (`buffer.after-switch` + the tick), because
-  `_attach_buffer` is active-buffer-only and cannot reach the others.
-  The per-buffer once-only bound is what stops a failing fallback
-  retrying forever — the round-2 defect a naive global repair loop would
-  have reintroduced for every buffer instead of one. Plus a P2: the
-  argument-inclusive attribution was implemented but pinned only by
-  "contains the command name", so a mutation dropping every argument
-  still passed.
-- **Round-5 review: one P1 plus a frontend scope hole, and four more.**
-  (1) A fallback that SPAWNS and then dies retried forever: the
-  once-per-buffer guard bounds `_attach_buffer`, not the server it
-  produced, and `ensure_server` never forwards `cfg.restart` so the
-  fallback inherits `OnCrash` — respawned by the manager with no
-  ceiling, silently, because `latched` had disabled the primary's poll.
-  The fallback now gets its own one-shot die-before-initialize watch.
-  (2) **Simultaneous frontends**: both repair triggers read the ambient
-  `pmacs.window.buffer()`, and the daemon restores `active_frontend` to
-  the last-dispatched one before `tick_processes`, so a Lean buffer
-  active in ANOTHER frontend gets no `after-switch` and stays stale.
-  Fixed at the right seam — **make CONSUMPTION safe**: both
-  `attached_for_active` and `attachment_for_request` now refuse a record
-  whose server is dead (the former rebuilds, the latter reports none,
-  since it must not perturb LSP state). Healing at the point of use is
-  frontend-agnostic, because whichever frontend runs a command is active
-  while it runs. (3) The retirement sweep selected on `language_id`, so
-  it stopped USER-spawned Lean servers too; it now keys on the
-  `default-lean4` label `ensure_server` stamps, which is the derivation
-  discriminator. (4) `probe.latched` gated repair even when NO swap
-  occurred, so an already-fallback config was retried and misreported.
-  Split out `probe.fallback_installed`. (5) The once-per-buffer
-  assertion counted TABLE KEYS, which cannot distinguish "once per
-  buffer" from "every tick for one buffer" — cardinality stays 1 either
-  way. Now a numeric attempt counter; the bite shows **174 vs 1**.
-- **Round-6 review: four P1s and one P2, suite 40/40.** (1) General
-  point-of-use healing treated a crashed OnCrash server as absent and
-  spawned beside it while its old id still had `next_restart_at` armed;
-  `attach_buffer` now forgets a terminal record before replacement.
-  `attachment_for_request` remains non-attaching and preserves the
-  record, so a same-id restart can recover instead of being orphaned.
-  (2) The fallback watch was scalar, while Q#LN15 permits simultaneous
-  per-root servers and lsp.lua can create them without passing through
-  Lean's repair function. Watches are now per-SID and discover every
-  config-driven Lean server from a private origin table. (3) The shipped
-  `lean.wait-for-diagnostics` command bypassed both safe resolvers and
-  still consumed a stopped record; it now uses a command-safe resolver,
-  waits asynchronously for a healed replacement to initialize, and the
-  test requires the real request to finish. (4) When no config swap
-  occurred, one failed root still swept a healthy root; that arm now
-  retires only the SID whose verdict fired. (5) `label` is public and
-  unreserved, therefore not ownership. lsp.lua records successful
-  config-driven spawns privately, and every Lean lifecycle decision keys
-  on that origin fact; the user-server pin deliberately collides on
-  `default-lean4`. All five bites against `19f48d4` discriminate: the
-  old files produce 2 same-root servers, a fallback attempt of 4, a
-  shipped command still targeting `stopped`, retirement of the healthy
-  root, and retirement of the colliding user server, respectively.
-- **DURABLE LESSON — "the test that passes" vs "the test that
-  discriminates."** Green tests across six rounds repeatedly pinned only
-  a nearby helper or an absence, and only biting exposed it. **Carry this
-  to `docs/agent-handoff.md` when the lane lands.** The concrete shapes,
-  all from this branch:
-  1. R1 acceptance 36 asserted "every server is terminal" — pinning the
-     ABSENCE of the fallback it claimed to test.
-  2. "No live non-fallback server" misses a respawn loop: a respawning
-     server sits in `crashed` most of the time. `attempt` counts
-     respawns; liveness does not.
-  3. Returning to a buffer via `find_or_open` re-fires
-     `buffer.after-load`, which repairs the attachment regardless of the
-     code under test. Use `switch_buffer`.
-  4. A MISSING executable fails synchronously inside `after-load`, where
-     the rebuild happens inline — no async race can occur. Only the
-     probe path exercises asynchronous ordering.
-  5. A mutation that RAISES (indexing a nil config) is swallowed by the
-     hook's pcall, so the bite "passes" for the wrong reason. A bite must
-     reproduce the original shape, not merely break the code.
-  6. A fixture whose `serve` sleeps can never let the primary initialize
-     first, so it cannot reach the ordering where a late verdict must
-     retire a LIVE server.
-  7. Asserting on a field that no longer exists (`_probe.reattach_from`
-     after a refactor) reads as nil and passes for nothing. Assert
-     positive facts — a count, a command string — not absences.
-  8. Counting DISTINCT KEYS cannot bound REPEATED WORK: a per-tick retry
-     on one buffer keeps `#repaired == 1` forever. Count the attempts,
-     not the things attempted against (bite: 174 vs 1).
-  9. A NONEXISTENT executable only exercises synchronous ENOENT. To
-     reach "spawned, then died", the fixture must actually spawn.
-  10. Calling the two SAFE HELPERS directly does not pin a shipped
-      command that bypasses both. Drive the command registry entry and
-      require its terminal result — replacing a dead record with a
-      `starting` server is still not success if the request is issued
-      before initialize.
-  Rule: **a test is not evidence until the mutation it targets has been
-  shown to fail it.**
-- **SECOND DURABLE LESSON — a scope error repeats until the scope is
-  named.** The "fallback silently does not happen" defect came back four
-  times: no re-attach; re-attach cleared by an unrelated buffer;
-  re-attach satisfied by the server being replaced; re-attach of one
-  buffer while the others stay stale. Every fix was locally correct and
-  none asked *what does this config swap invalidate?* — the answer being
-  every Lean buffer and every Lean server, because the config entry is
-  global and servers are per-root. **When a change edits shared state,
-  enumerate everything derived from it before repairing anything.**
-- **SUBSTRATE BUG FOUND, not fixed here (framing §6).**
-  `LspManager::stop` on an ALREADY-terminal server takes its
-  not-initialized branch, terminates the dead process and sets
-  `ShuttingDown { .. None }` on the premise that "the next exit
-  observation cleans up" — but the exit already happened, which is what
-  made it `Crashed`. No further event arrives, so the client is stuck in
-  `ShuttingDown` **forever**: `server_is_live` reads it as LIVE, so
-  `attach_buffer` never rebuilds, and `forget` refuses it for not being
-  terminal. **Stopping a dead server is what makes it un-replaceable.**
-  Lean works around it by dispatching on state: `forget` when
-  terminal, `stop` when live. Merely SKIPPING the call is not
-  enough — that leaves `next_restart_at` armed.
-- Round-1 review found four P1s, all real: the latch swapped the config
-  but never spawned or re-attached (and acc36 *asserted every server was
-  terminal*, pinning the absence of the fallback); a missing `lake`
-  bypassed probe and latch entirely because the hook keyed on an
-  attachment that ENOENT prevents; `waitForDiagnostics` omitted the
-  `version` Lean requires; and the ledger stated the dangerous stacking
-  order.
-- The probe's non-zero exit is deliberately NOT a fallback trigger —
-  §2.9's elan shim makes `lake --version` fail where `lake serve` still
-  works. Only a parseable version below 3.1.0 triggers it; the
-  server-failure latch covers the rest.
-- Verification on this branch: `cargo fmt --check` clean; strict
-  workspace Clippy clean; 1,829 default + 2,003 CRDT library tests;
-  lean4 server 40/40; lean4 stage 1 9/9; dispatch seams 15/15;
-  multi-root 13/13; M4 121; required GPU 155; **isolated-config
-  serial workspace sweep 3,229 across 94 suites, zero failures**;
-  `git diff --check` clean. (Round 1 of
-  this entry recorded 17/17 and 3,206 — the PRE-fix counts — after the
-  fixes were pushed. The ledger's protocol is that verification
-  describes the pushed tree; recording it late is the #161 fmt-blocker
-  error in a slower form.)
-
-### Stage 4 — framing rev 6, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`)
+### Stage 4 — framing rev 7, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`)
 
 - Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170**
   (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main
   that had advanced 50 commits mid-review; the only conflict either time
   was this ledger's own lane headings, resolved by keeping both sides.
 - Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`.
-  Framing-only so far: `docs/lean4-mode-framing.md` **revision 6**. No
+  Framing-only so far: `docs/lean4-mode-framing.md` **revision 7**. No
   code. Awaiting user approval before implementation, per the workflow.
+- **Round 6 review found five P1s, four of them internal to rev 6** —
+  facts about pmacs the revision asserted without checking, while its
+  external (upstream) facts held. Fixed in rev 7: Stage 4a's footprint
+  omitted the test file its own acceptance requires; pending
+  abbreviation state was keyed by buffer when pmacs is **multi-frontend**
+  (`EditorCore.views` is per-`FrontendId`, `take_typed_edit` is already
+  frontend-keyed, and `buffer.after-switch` fires with NO arguments, so
+  a buffer-keyed clear lets any frontend discard another's pending
+  state); the shortest-match rule was missing its **tie-break by source
+  declaration order**, which 101 prefixes depend on and a `pairs`-
+  iterated Lua map cannot express; and the generator's "abort on keys
+  needing escaping" rule **rejects the real table** (`\` is a key, `"`
+  begins eleven).
+- **A 404 on a guessed path is not evidence of absence.** Rev 6 declared
+  the upstream package ships no README after fetching the package root,
+  with the directory listing showing `src/README.md` already in hand.
+  The README states the tie rule in one sentence.
 - **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).**
   4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua`
   plus `pair.lua` re-expressed as one registered consumer, no behavior
diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md
index b2d0aeb..a176505 100644
--- a/docs/agent-handoff.md
+++ b/docs/agent-handoff.md
@@ -1,7 +1,8 @@
 # Agent handoff — cross-machine continuity
 
-**Last updated: 2026-07-25, after the inline-math slice (#158) landed —
-the first mathematical typesetting in pmacs — following find-file (#162),
+**Last updated: 2026-07-26, after Lean 4 stages 3a and 3b (#167, #170)
+landed — pmacs' first Lean language server — following the inline-math
+slice (#158), the first mathematical typesetting in pmacs, and find-file (#162),
 the dired arc's Stage 0, and COHERENCE.md (#163), Lean 4 Stage 1 (#160), the
 minimap blank-slab fix (#159), bottom-panel Stage 1 (#155), the
 inline-math re-scout (#154), the vterm PTY-flake fix (#153), and the
@@ -25,15 +26,15 @@ reads it the way you just did.
 For volatile branches, checkpoints, verification, and recovery
 commands, read `docs/active-work.md` immediately after this file.
 
-## 1. Where the project stands (2026-07-25)
+## 1. Where the project stands (2026-07-26)
 
-- `main` @ `d152120` (the bottom-panel landed-doc refresh #156 atop the
-  inline-math slice #158, dired Stage 1 #165, the GPU terminal input fix
-  #166, Lean 4 Stage 2 #161, the dired framing #164, COHERENCE.md #163,
-  find-file #162, Lean 4 Stage 1 #160, minimap blank-slab #159,
-  bottom-panel Stage 1 #155). Protocol unchanged at **v20**. The bullets
-  below describe the arcs in their own terms; this line is the
-  head-of-`main` anchor.
+- `main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a #167, the
+  bottom-panel landed-doc refresh #156, the inline-math slice #158,
+  dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2
+  #161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean
+  4 Stage 1 #160, minimap blank-slab #159, bottom-panel Stage 1 #155).
+  Protocol unchanged at **v20**. The bullets below describe the arcs in
+  their own terms; this line is the head-of-`main` anchor.
 - **`COHERENCE.md` is now required reading and a required framing input
   — #163.** It carries the product-coherence thesis, an audited
   scorecard, per-concern gaps, and §20's priority order, and it is the
@@ -42,6 +43,56 @@ commands, read `docs/active-work.md` immediately after this file.
   interaction islands added, config-registry adoption, background-work
   attribution. Its §2 grades the golden journey **broken at step 3**
   (`pmacs .` exits 1).
+- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b LANDED**
+  (`docs/lean4-mode-framing.md`; #160, #161, #167, #170; merge
+  `d400f30`). pmacs edits Lean 4: `arborium-lean` highlighting, a
+  `lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language
+  server with a Lake-aware outermost root, a lazy toolchain probe, a
+  one-shot `lean --server` fallback, and `waitForDiagnostics`. **No
+  protocol change in any stage** (still v20).
+  - **Two of the four stages contained no Lean at all**, and that is the
+    arc's organizing rule: *no PR mixes a cross-cutting substrate change
+    with Lean feature content.* Stage 2 made LSP server affinity
+    per-project-root (`ensure_server` had been reusing one server across
+    roots — a correctness bug for every language, not just Lean). Stage
+    3a added notification/response subscription seams to
+    `handle_server_requests`, the single shared LSP event drain, plus
+    `pmacs.fs.canonicalize`.
+  - **Two consecutive re-scouts found that rule broken by the stage
+    being scouted** — Stage 3 in round 4, Stage 4 in round 5, each time
+    by a risk column that contradicted its own prose. The rule is not
+    self-enforcing. Re-check every remaining stage's risk column at
+    scout time.
+  - **A configured LSP root must be a canonical absolute path.** It
+    reaches `file_uri_for` verbatim and that URI is the affinity key, so
+    one package opened by two spellings spawns two servers. Stage 3a's
+    `pmacs.fs.canonicalize` is the primitive; it returns nil rather than
+    a lossy path for non-UTF-8 input.
+  - **`LspManager::stop` on an already-terminal client strands it in
+    `ShuttingDown` forever** — `server_is_live` then counts it live so
+    nothing rebuilds against it, and `forget` refuses it for not being
+    terminal. *Stopping a dead server is what makes it un-replaceable.*
+    Stage 3b works around it by dispatching on state (`forget` when
+    terminal, `stop` when live); merely skipping the call leaves
+    `next_restart_at` armed. The real fix is unframed substrate work.
+  - **`elan` shims lie**: `lake --version` and `lean --version` can both
+    fail ("no default toolchain configured") on a machine where Lean
+    otherwise works, so `command -v lake` is worthless as a capability
+    check. Lean acceptance is fake-server; live smokes must be PATH-
+    **and** success-gated.
+  - Stage 3b took six review rounds, and **the same defect appeared four
+    times**: "the fallback silently doesn't happen," as no re-attach,
+    then re-attach cleared by an unrelated buffer, then satisfied by the
+    very server being replaced, then repairing one buffer while the rest
+    stayed stale. Each fix was locally right; none asked what a *global*
+    config swap invalidates. The durable lesson is to heal at
+    **consumption** — the point where a stale record is handed out — not
+    at the moment of the swap.
+  - Remaining: Stage 4a (typed-edit consumer chain) and 4b (the Unicode
+    input method) are framed and awaiting approval; stages 5 (goal
+    panel), 6 (`#eval` output channel), and 7 (module hierarchy) are
+    framed but not scouted against current `main`.
+
 - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3;
   merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU
   frontend. **No protocol change (still v20); the whole slice lives in
diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md
index e39eb36..ca50696 100644
--- a/docs/lean4-mode-framing.md
+++ b/docs/lean4-mode-framing.md
@@ -46,7 +46,7 @@ during a rebase.
 
 ## 0.1 Revision history
 
-Revision 1 — initial.
+Revision 1 — initial. Current revision: **7**.
 
 ### Round 1 (rev 1 → rev 2)
 
@@ -288,11 +288,15 @@ landed and its citations are historical record, not navigation.
 
 Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against `main`
 @ `d400f30` produced **six findings that change the plan** and three
-that confirm it. The pmacs-side facts were verified in a worktree at
+that confirm it. (Round 6 found five more, four of them internal to this
+revision; read that section too before trusting a rev-6 statement.) The pmacs-side facts were verified in a worktree at
 that commit; the upstream facts were verified by downloading and reading
 `leanprover/vscode-lean4` at commit `17d1d08` (2026-05-29) — the
 algorithm, not its documentation, since the `lean4-unicode-input`
-package ships no README.
+package ships no README. *(Round 6: it does, at `src/README.md` — see
+that section. Corrections to round 5's own numbers are marked inline
+below rather than rewritten, per the standing rule that revision
+entries are record, not navigation.)*
 
 1. **Stage 4 violated this document's own splitting rule — the same way
    Stage 3 did.** §4 says "no PR in this arc mixes a cross-cutting
@@ -377,6 +381,14 @@ package ships no README.
    needs a `doNotTrackNewAbbr` guard and why §2.11 records that pmacs
    does not.
 
+   *Corrected in round 6.* **119** symbols are multi-codepoint, of which
+   26 carry `$CURSOR`; "93" was the non-`$CURSOR` subset stated as a
+   total. **Three** values contain a backslash — the `\` → `\` identity
+   entry was missed. And this entry's biggest omission is not a number:
+   the shortest-key rule needs a **tie-break by source declaration
+   order**, which the README round 5 said did not exist states outright.
+   §2.11 and Q#LN11 carry the corrected facts.
+
 Confirmations, recorded because each was load-bearing and unverified:
 
 7. **`take_typed_edit`'s one-shot contract is unchanged**
@@ -404,6 +416,70 @@ Citation drift repaired per COHERENCE §25, on the same terms as round
 and the revision-history entries above, which are historical record
 rather than navigation.
 
+### Round 6 (rev 6 → rev 7)
+
+The 4a/4b split held; five P1s against the revision's own content, all
+real, all reproduced. Four share a root: **rev 6 verified its external
+facts and under-verified its internal ones.**
+
+1. **Stage 4a's declared footprint excluded the tests its acceptance
+   required.** Q#LN10 listed three production files while 46a–46e demand
+   chain-specific tests that cannot live in
+   `tests/auto_pair_acceptance.rs` — criterion 46 requires that file
+   byte-identical. Footprint now names
+   `tests/typed_edit_chain_acceptance.rs` and adds it to the PR's gates.
+2. **Pending state had the wrong owner.** §2.11 reasoned "no
+   multi-cursor, therefore one point" and Q#LN22 keyed pending
+   abbreviations by buffer. pmacs is multi-frontend: `EditorCore.views`
+   is per-`FrontendId` with its own active window, `take_typed_edit` is
+   *already* frontend-keyed, and `pmacs.frontend.id()` exists. Two
+   frontends on one Lean buffer — the TUI-plus-GPU case this project
+   ships — would share one slot. Worse, `buffer.after-switch` takes no
+   arguments, so a buffer-keyed clear-on-switch lets any frontend
+   discard another's pending abbreviation. Now keyed
+   `(frontend, buffer)` with a window check, frontend-scoped
+   after-switch clearing, a `frontend.detached` purge, and acceptance
+   45i — which the buffer-keyed design passes every other criterion
+   without.
+3. **The shortest-match rule was missing its tie-break, and rev 6's
+   research method is why.** Upstream keeps declaration order among
+   equal-length shortest keys. The README states it in one sentence —
+   and rev 6 asserted "the package ships no README" after a 404 on the
+   package root, without checking the directory listing it had already
+   fetched, which shows `README.md` under `src/`. **A 404 on a guessed
+   path is not evidence of absence.** The rule is load-bearing: 101
+   prefixes have equal-shortest candidates resolving to *different*
+   symbols (`f` → `f<` not `f>`; `"` picks `"A` from eleven). A `pairs`-
+   iterated Lua map cannot express it, so Q#LN11 now emits an ordered
+   sequence and Q#LN22 sorts by `(#key, source rank)`.
+4. **The generator's rejection rule rejected the current table.** "Abort
+   on keys needing Lua escaping" would reject `\` and the eleven `"X`
+   keys — and acceptance 45d requires `\` to work. Replaced with
+   canonical lossless escaping; the generator aborts only on duplicate
+   keys, invalid UTF-8, and a failed self-round-trip. Relatedly, 45g
+   claimed the suite compares against `abbreviations.json`, which is not
+   shipped; it now pins self-consistency properties and leaves
+   source fidelity to the generator, where the source is in hand.
+5. **Durable and volatile state were not reconciled** —
+   `docs/agent-handoff.md` still anchored `main` at `d152120` with
+   neither #167 nor #170, while `docs/active-work.md` kept full merged
+   Stage 3a/3b histories against its own instruction to remove merged
+   entries, under a stale July 25 snapshot date. Round 5 updated the
+   ledger and skipped the handoff; per CLAUDE.md both are required
+   reading, and the one that outranks the other was the one left wrong.
+
+Corrections carried in the same revision, each verified against the
+data: the README exists (finding 3); there are **119** multi-codepoint
+symbols, of which 26 carry `$CURSOR` — rev 6's "93" was the
+non-`$CURSOR` subset reported as a total; **three** values contain a
+backslash (`\`, `n`, `setminus`), not two; Q#LN22 now states the rule
+acceptance 45d depended on, that an unclaimed terminating `\` is
+reprocessed as a new leader; acceptance 38 now says the terminator is
+retained, so undo restores `\alpha ` with its space; the coherence
+section cites golden-journey **step 5** ("Edit immediately"), not step
+4; and §8's config-registry prior art points at Q#LN22, where the gate
+now lives.
+
 ## 1. What ships
 
 Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The
@@ -828,8 +904,15 @@ them from the store needs a Rust-side policy, not a Lua filter. Q#LN18.
 Scouted 2026-07-26 against `leanprover/vscode-lean4` @ `17d1d08`,
 package `lean4-unicode-input`, files `AbbreviationProvider.ts`,
 `TrackedAbbreviation.ts`, `AbbreviationRewriter.ts`,
-`AbbreviationConfig.ts`, and `abbreviations.json`. The package ships no
-README, so the algorithm below is read off the source. Apache-2.0.
+`AbbreviationConfig.ts`, `abbreviations.json`, and — round 6 — the
+package README at `lean4-unicode-input/src/README.md`. Apache-2.0.
+
+**Rev 6 first claimed this package ships no README. It does**, at
+`src/README.md` rather than the package root, and the 404 on the root
+path was taken as absence without checking the directory listing that
+was already in hand. That cost the tie rule below: the README states it
+in one sentence, and reading only the code left it as an inference from
+`Array.prototype.sort`'s stability rather than a documented contract.
 
 **Resolution.** `findSymbolsByAbbreviationPrefix(p)` collects every key
 having `p` as a prefix, sorts them by **key length ascending**, and maps
@@ -845,6 +928,32 @@ Verified against the table: `alpha` → `α`, `alp` → `α` (via `alpha`),
 surprising enough to be worth an acceptance criterion), `alp7` → `α7`
 via rule 2, `a` → `α` (`a` is itself a key, among 29 prefix matches).
 
+**The tie rule, and why it is a constraint on the vendored format.**
+When several shortest keys have equal length, upstream takes **the one
+declared first in `abbreviations.json`**. The README says so outright;
+the code achieves it because `Object.keys()` yields JSON insertion order
+and `Array.prototype.sort` is stable. Ties are not rare: **101 prefixes
+have equal-shortest candidates that resolve to *different* symbols**.
+`f` picks `f<` → `‹` over `f>` → `›`; `"` picks `"A` → `Ä` from eleven
+equal-length candidates; `(` picks `()` over `(=`, `(b`, `((`, `([`.
+
+A Lua table iterated with `pairs` has no order at all, so **a generated
+`{ [key] = symbol }` map cannot express this contract** — it would
+resolve these 101 prefixes nondeterministically, and worse, *stably
+wrong* per build. Q#LN11 therefore carries source rank alongside the
+symbol.
+
+**Two things the README explains that the code does not.** `Tab` is the
+manual early-replacement trigger upstream binds, which is why
+`getReplacementText`'s shortest-prefix rule is user-visible at all
+rather than an internal detail. And the `[]_`/`{}_` entries in the table
+are not symbols anyone types — they are **decoys**, added so that `\[`
+is not uniquely-and-completely matching and therefore does not eagerly
+expand before the user can type the second `[`. That is the same
+collision Q#LN22 handles from the pairing side, solved upstream by
+editing the data. Anyone regenerating the table must not "clean up"
+those entries.
+
 **Tracking.** The leader `\` is inserted into the buffer like any other
 character, and the tracked range starts after it; the replaced range
 spans the leader inclusive (`abbreviationRange.moveKeepEnd(-1)`). So the
@@ -881,8 +990,10 @@ abbreviation the cursor has left. pmacs has no cursor-motion hook
 (round-5 finding 3), so this seam does not exist here and Q#LN22 makes
 abandonment lazy instead.
 
-**The re-arm guard pmacs does not need.** `setminus` → `\` and `n` →
-`\n`, so an expansion can insert a backslash; upstream sets
+**The re-arm guard pmacs does not need.** Three values contain a
+backslash — `\` → `\`, `n` → `\n`, and `setminus` → `\` (rev 6 first
+said two, dropping the `\` → `\` identity entry) — so an expansion can
+insert a backslash; upstream sets
 `doNotTrackNewAbbr` across the replace so that backslash does not open a
 new abbreviation. In pmacs the expansion is a programmatic `buf:replace`
 that arms no typed-edit record, so the chain sees nothing and cannot
@@ -891,9 +1002,25 @@ contract, not by accident — and the acceptance must pin it, because a
 future consumer that inferred from buffer text rather than provenance
 would reintroduce the bug.
 
-**What pmacs does not have to carry.** Multi-cursor. Upstream tracks a
-`Set<TrackedAbbreviation>` and sorts changes bottom-up for that reason;
-pmacs has one point, so one pending abbreviation per buffer.
+**What pmacs does not have to carry.** Multi-cursor within a frontend.
+Upstream tracks a `Set<TrackedAbbreviation>` and sorts changes bottom-up
+for that reason; pmacs has one point per frontend view.
+
+**What pmacs has instead, and rev 6 got wrong.** Rev 6 read "no
+multi-cursor" as "one point" and keyed pending state by buffer alone.
+**pmacs is multi-frontend**: `EditorCore.views` is a
+`HashMap<FrontendId, FrontendView>`, each with its own active window and
+cursor; `take_typed_edit` is already keyed by frontend
+(`typed_edit_armed: Option<(FrontendId, TypedEditRecord)>`, matched
+against `active_frontend`); the record carries `window` as well as
+`buffer`; and `pmacs.frontend.id()` is exposed to Lua. Two frontends
+editing the same Lean buffer — the ordinary TUI-plus-GPU case, not an
+exotic one — would share a single buffer-keyed pending slot, so one
+could extend, expand, or silently clear the other's half-typed
+abbreviation. `buffer.after-switch` makes it worse: it fires with no
+arguments, so a buffer-keyed clear-on-switch would let *any* frontend's
+navigation discard a pending abbreviation belonging to another. Q#LN22
+keys the state accordingly.
 
 ## 3. Decisions
 
@@ -1340,11 +1467,27 @@ claim a reader must be able to check without reconstructing
 `src/editor.rs`'s include list.
 
 **Stage 4a ships this and nothing else.** Its whole content is:
-`typed_edit.lua`, `pair.lua` re-expressed as one registered consumer,
-and the `include_str!` line. Round 5's finding 1 is why this is a PR and
-not a first commit — `pair.lua` is every language's auto-pairing, and a
-reviewer looking at a Lean PR should not have to also review a rewrite
-of it.
+
+| File | Change |
+|---|---|
+| `builtin/runtime/typed_edit.lua` | new — the chain owner |
+| `builtin/runtime/pair.lua` | re-expressed as one registered consumer |
+| `src/editor.rs` | one `include_str!` line, before `pair.lua`'s |
+| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46e |
+| `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** |
+
+Rev 6 listed only the first three and then required criteria 46a–46e,
+which no existing suite can host: the auto-pairing suite must stay
+untouched (that is the whole point of criterion 46), so the chain's own
+behavior — take-once, priority order, claim-stops-chain, throw
+containment — has nowhere to live. A declared footprint that excludes
+the tests its own acceptance demands is not a footprint. The new suite
+joins the required gate list for this PR alongside
+`tests/auto_pair_acceptance.rs`.
+
+Round 5's finding 1 is why this is a PR and not a first commit —
+`pair.lua` is every language's auto-pairing, and a reviewer looking at a
+Lean PR should not have to also review a rewrite of it.
 
 **The no-behavior-change claim must be pinned, not asserted.** The full
 `tests/auto_pair_acceptance.rs` suite is a required gate for 4a and must
@@ -1377,10 +1520,24 @@ file rather than estimated:
 | 305 keys that are proper prefixes of another | which keys can expand eagerly |
 | 1,550 keys uniquely-and-completely matching | the eager-expansion set |
 | 26 values containing `$CURSOR` | point placement |
-| 93 multi-codepoint values | the replace is not one-char-for-many |
+| 119 multi-codepoint symbols (26 of them `$CURSOR`-bearing) | the replace is not one-char-for-many |
+| 101 prefixes with disagreeing equal-shortest ties | why the format carries source rank |
+
+(Rev 6 gave the multi-codepoint figure as 93, which was the count
+*excluding* the `$CURSOR` entries — a subset reported as a total.)
 
 vscode-lean4 is Apache-2.0.
 
+**Format: an ordered array, not a map.** §2.11's tie rule makes source
+order semantic, and a Lua `{ [key] = symbol }` table iterated with
+`pairs` cannot carry it. The generated file emits a **sequence** —
+`{ {key, symbol}, ... }` in `abbreviations.json` order — plus a derived
+`key → index` lookup built at load time for the exact-match case.
+Resolution sorts candidates by `(#key, index)`, so the 101 ties resolve
+the way upstream resolves them and the file's own line order is the
+audit trail. A map-shaped emit would be nondeterministic across builds
+and, once a hash order happened to be stable, *stably wrong*.
+
 Vendor it as a generated `builtin/runtime/lean_abbrev.lua` with a header
 recording source repo, commit, license, entry count, and the
 regeneration command — the `builtin/queries/latex/highlights.scm`
@@ -1405,12 +1562,29 @@ so the file is self-describing to whoever next touches it. A refresh is
 an ordinary PR with a visible diff — which is the point: the diff is the
 review.
 
-**The generator must reject a table it cannot faithfully encode.** Keys
-are ASCII today but nothing upstream promises that; a key containing a
-character the emitted Lua would have to escape, or a duplicate after
-normalization, aborts the regeneration rather than silently emitting a
-table that disagrees with its source. Same discipline as Q#LN20's
-refusal to hand back a lossy path.
+**Escaping is canonical and lossless, not a rejection trigger.** Rev 6
+said the generator aborts on "a key containing a character the emitted
+Lua would have to escape." **That rule rejects the current table**: `\`
+is a key, `"` begins eleven keys (`"A` → `Ä` …), and acceptance 45d
+requires `\` to work. The generator instead emits every key and symbol
+through one canonical Lua string escaper — `\\`, `\"`, `\n`, `\r`,
+`\t`, and `\ddd` for any other control byte, everything else literal
+UTF-8 — chosen so the emit is byte-deterministic across runs.
+
+What the generator *does* abort on, because these are real corruption
+rather than syntax:
+
+- a duplicate key after decoding (JSON permits it; the table must not),
+- a key or symbol that is not well-formed UTF-8,
+- a round-trip mismatch: the generator re-parses its own output and
+  compares the full ordered sequence against the source, entry for
+  entry, and fails if they differ anywhere.
+
+That last check is what makes the artifact trustworthy, and it belongs
+in the generator rather than in the acceptance suite — the suite cannot
+see `abbreviations.json`, which is not shipped. Same discipline as
+Q#LN20's refusal to hand back a lossy path: refuse rather than emit
+something plausible.
 
 ### Q#LN21 — Stage 4b: the expansion's undo is cross-peer-degraded; ship it, name it
 
@@ -1466,23 +1640,54 @@ that an edit was made.
 reconstruction of it:
 
 - `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer,
-  start_offset, text = "" }`, one per buffer, keyed on `rec.buffer`.
+  window, start_offset, text = "" }`, keyed on **`(frontend, buffer)`** —
+  see below.
 - A subsequent self-insert `c` is claimed iff at least one key has
   `text .. c` as a prefix; then `text = text .. c`. If it is also
   uniquely-and-completely matching (one of the 1,550), expand now.
 - If no key extends `text .. c`, expand `text` **first**, then let `c`
   land normally — the chain does *not* claim `c`.
-- Expansion resolves through §2.11's three-rule `getReplacementText`,
-  including the suffix rule (`\alp7` → `α7`).
+- **A terminating `c` that is itself `\` is then reprocessed as a new
+  leader**, opening a fresh pending abbreviation at its position. This
+  is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6
+  specified the acceptance without specifying the rule; upstream gets it
+  from `processChange`, where a `finished` abbreviation reports
+  `isAffected = false` and so does not suppress the new-leader branch.
+  Note this is *not* the `\\` case: there the pending text is empty, `\`
+  extends rather than terminates, and the result is one literal
+  backslash with no pending state left open.
+- Expansion resolves through §2.11's rules — shortest key wins, ties
+  broken by source rank, unmatchable tail appended (`\alp7` → `α7`).
 - `$CURSOR` is stripped from the symbol and its index becomes the point.
 
+**Ownership is per frontend, not per buffer** (§2.11). The key is
+`(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still
+match `rec.window` for the state to be usable — a frontend that moved
+the same buffer into a different window is no longer typing where the
+pending span is. Two consequences the buffer-only design got wrong:
+
+- `buffer.after-switch` fires with **no arguments**, so it cannot say
+  whose switch it was. The subscriber reads `pmacs.frontend.id()` at
+  callback time — documented as "the frontend that produced the most
+  recent dispatched input event" — and clears **only that frontend's**
+  entries. A blanket clear would let one frontend's navigation discard
+  another's half-typed abbreviation.
+- `frontend.detached` fires with the raw frontend id and is the purge
+  seam, exactly as `killring.lua` uses it (Q#KR11). Without it a
+  detached frontend's pending state leaks for the life of the session.
+
+This costs one table level and buys correctness in the ordinary
+TUI-plus-GPU configuration, which is not an exotic setup — it is the
+one this project ships two frontends for.
+
 **Abandonment is lazy, because there is no cursor-motion hook** (round-5
 finding 3). Pending state is validated at the next typed edit and
-discarded when any of these no longer holds: the record's buffer is the
-pending buffer; `rec.effective_start` equals `start_offset + 1 +
-#text` (the point is still at the end of the pending span); and the
-buffer's `revision()` advanced by exactly the pending edit. `buffer.
-after-switch` clears it eagerly since that hook *does* exist. The
+discarded when any of these no longer holds: the record's buffer and
+window are the pending ones; `rec.effective_start` equals `start_offset
++ 1 + #text` (the point is still at the end of the pending span); and
+the buffer's `revision()` advanced by exactly the pending edit.
+`buffer.after-switch` clears the acting frontend's entries eagerly,
+since that hook *does* exist. The
 practical difference from upstream: a user who clicks away mid-`\alp`
 and types elsewhere gets the pending state dropped rather than expanded.
 Upstream expands it. **This is a deliberate divergence** — expanding
@@ -2138,6 +2343,11 @@ substrate pin, filed under Stage 4 only because Stage 4 was one stage.
 Per the no-renumbering rule above, round 5's additions take letter
 suffixes on both sides of the split.
 
+46a–46e live in a **new `tests/typed_edit_chain_acceptance.rs`**, which
+is part of Stage 4a's declared footprint (Q#LN10) and a required gate
+for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which
+criterion 46 requires to stay byte-identical.
+
 46. **Provenance-refactor pin:** the full `tests/auto_pair_acceptance.rs`
     suite passes **unmodified**. A suite edited to accommodate the
     refactor proves nothing; the diff for 4a must show zero lines
@@ -2164,8 +2374,12 @@ suffixes on both sides of the split.
 
 **Stage 4b — the Unicode input method**
 
-38. `\alpha` + space yields `α`; the whole expansion is a single undo
-    step, and one undo restores `\alpha` rather than `\alph`.
+38. `\alpha` + space yields `α ` — the space lands first and the
+    expansion runs in the following `buffer.after-edit`, so the
+    terminator is **retained**, not consumed. The expansion is a single
+    undo step: one undo restores `\alpha ` (with its space), not
+    `\alph`. Rev 6 wrote the post-undo text as `\alpha`, which would be
+    true only if the terminator were swallowed.
 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR`
     placeholder.
 40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is
@@ -2211,6 +2425,14 @@ suffixes on both sides of the split.
     because the expansion is a programmatic replace that arms no record.
     Bites against a future consumer that infers pending state from
     buffer text instead of provenance.
+45i. **Pending state is per frontend (Q#LN22).** Two frontends attached
+    to the same `lean4` buffer: A types `\al`, B types `\to` + space in
+    the same buffer. B's expansion yields `→` and leaves A's `\al`
+    pending and intact; A then typing `l` + space still yields `∀`.
+    Plus: B switching buffers does not clear A's pending state, and a
+    `frontend.detached` for B purges B's entries only. Bites against the
+    buffer-keyed design rev 6 specified — which passes every
+    single-frontend criterion above.
 45f. **Both producers, and the CI-darkness stated.** The dispatch path
     is pinned by the criteria above. The optimistic CRDT producer
     (round-5 finding 4) is pinned by a separate criterion driving
@@ -2222,11 +2444,30 @@ suffixes on both sides of the split.
     verified only locally and name the command. Silence here is the
     failure mode — a green CI would otherwise read as covering the path
     most users take.
-45g. **Table integrity.** The generated `lean_abbrev.lua` round-trips:
-    its entry count matches the header's declared count, and a spot set
-    of entries (`alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`) matches
-    `abbreviations.json` byte-for-byte. Bites against a generator that
-    silently drops or mangles keys (Q#LN11).
+45g. **Table integrity — what the suite can actually check.**
+    `abbreviations.json` is not shipped, so the suite cannot diff
+    against it and rev 6's "matches byte-for-byte" was unbuildable; a
+    count plus seven spot entries could not prove 1,855 round-trip
+    anyway. The full source-fidelity check belongs to the generator
+    (Q#LN11: re-parse own output, compare the ordered sequence entry for
+    entry, fail on any difference). What the suite pins instead are
+    self-consistency properties that a corrupt emit breaks:
+    - the loaded sequence's length equals the header's declared count,
+      and equals the declared count for the recorded upstream commit;
+    - every key is unique, and the derived `key → index` lookup has the
+      same cardinality as the sequence (a collision would silently drop
+      entries);
+    - every key and symbol is well-formed UTF-8, and no symbol contains
+      `$CURSOR` more than once;
+    - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`,
+      `n`, `setminus`, and the tie cases from 45h.
+45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` —
+    `f<` and `f>` are both length 2, and `f<` is declared first. Same
+    for `\"` + space → `Ä`, first of eleven equal-length candidates.
+    **This is the criterion that bites a map-shaped vendored table**:
+    with `pairs` iteration it passes or fails by hash order, so it must
+    also be run against a deliberately reversed sequence and shown to
+    fail. 101 prefixes are exposed to this rule.
 
 **Stage 5 — the goal view**
 
@@ -2294,7 +2535,7 @@ suffixes on both sides of the split.
   discipline on transformed source edits, and Q#AP1's optimistic-classifier
   limitation. Stage 4a generalizes the first; 4b is built on all three.
 - **#127 (config registry)** — `pmacs.config.define` and the
-  source-buffer-resolution correction. Q#LN10's gate follows
+  source-buffer-resolution correction. Q#LN22's gate follows
   `editing.auto-pair` exactly.
 - **#129 (mode system)** — mode-scoped keymaps for Stage 5.
 - **#155 (bottom panel)** — `pmacs.window.display` and the panel adopter
@@ -2381,9 +2622,10 @@ PR.
 (config registry) secondarily, by adding one option in the established
 shape rather than a new switch mechanism.
 
-**Golden journey (§2).** No step is touched by 4a. 4b improves step 4
-(editing) for Lean specifically and changes nothing for any other
-language: the pending-abbreviation state exists only in `lean4` buffers.
+**Golden journey (§2).** No step is touched by 4a. 4b improves **step 5
+("Edit immediately")** for Lean specifically and changes nothing for any
+other language — rev 6 cited step 4, which is "Understand the visible
+interface" and is untouched by both stages: the pending-abbreviation state exists only in `lean4` buffers.
 Neither stage changes launch, open, or attach.
 
 **Interaction islands (§6).** **None added, and this is the load-bearing