Merge pull request #179 from levineuwirth/lean4-stage4a-typed-edit-chain

Lean 4 Stage 4a: the typed-edit consumer chain

builtin/runtime/pair.lua

@@ -4,20 +4,30 @@
 -- next char is already `)` steps over it instead of doubling it. The
 -- carrier is a `buffer.after-edit` reaction (Q#AP1): the opener stays
 -- a genuine single-codepoint self-insert — the classification
--- signature help depends on — and this hook inserts (or swallows) the
+-- signature help depends on — and this reaction inserts (or swallows)
--- closer as a second edit. Provenance is the exact one-shot typed-edit
+-- the closer as a second edit. Provenance is the exact one-shot
--- record (`pmacs.editor.take_typed_edit()`, Q#AP9), not buffer-text
+-- typed-edit record (`pmacs.editor.take_typed_edit()`, Q#AP9), not
--- inference: pastes, programmatic edits, manual hook runs, and a stale
+-- buffer-text inference: pastes, programmatic edits, manual hook runs,
--- `this_command` have no record and never pair, and a transformed,
+-- and a stale `this_command` have no record and never pair, and a
--- relocated, or context-switching source self-insert fails closed.
+-- transformed, relocated, or context-switching source self-insert fails
+-- closed.
 --
--- This chunk loads BEFORE lsp.lua (Q#AP7): registration order is hook
+-- Since Arc 8 Stage 4a (Q#LN10) pairing no longer subscribes to
--- execution order, and lsp.lua's after-edit callback synchronously
+-- `buffer.after-edit` itself. It registers on the typed-edit chain
--- flushes didChange on the signature-trigger path — the closer must
+-- (`builtin/runtime/typed_edit.lua`), which owns the single subscriber
--- already be in the buffer when that callback runs. Everything under
+-- and the single one-shot read. Everything above still holds — the
--- `pmacs.lsp` is therefore looked up lazily at callback time.
+-- record is the same record — but the chain, not this file, decides
+-- who sees it and in what order.
 --
--- Framing: docs/auto-pairing-framing.md.
+-- This chunk loads AFTER typed_edit.lua (it registers into it) and
+-- BEFORE lsp.lua (Q#AP7): registration order is hook execution order,
+-- and lsp.lua's after-edit callback synchronously flushes didChange on
+-- the signature-trigger path — the closer must already be in the
+-- buffer when that callback runs. Everything under `pmacs.lsp` is
+-- therefore looked up lazily at callback time.
+--
+-- Framing: docs/auto-pairing-framing.md; Stage 4a in
+-- docs/lean4-mode-framing.md Q#LN10.
 
 pmacs.pair = pmacs.pair or {}
 
@@ -40,7 +50,7 @@ local ed = pmacs.editor
 
 -- Per-buffer on/off switch (Q#CR8's flagship adopter). Read against the
 -- SOURCE buffer of the typed edit, never the currently active one — see
--- the hook body below, which resolves it the same way `set_for` resolves
+-- the consumer body below, which resolves it the same way `set_for` resolves
 -- the buffer's pair set (round 2, finding 2): `rec.buffer`, not
 -- `pmacs.window.buffer()`.
 pmacs.config.define {
@@ -214,28 +224,36 @@ end
 -- Acceptance tests flip `_capture_records` on; each fan-out then
 -- publishes the record it observed (or nil) to `_last_record`, which
 -- is how tests read the exact codepoint / effective triple and prove
--- one-shot-ness (this callback registers first and consumes it).
+-- one-shot-ness (the chain takes the record before any other
+-- `buffer.after-edit` subscriber can, and hands it here).
 pmacs.pair._capture_records = false
 
-pmacs.hook.add("buffer.after-edit", function()
+-- The typed-edit consumer (Arc 8 Stage 4a, Q#LN10). `rec` is the one
+-- record `typed_edit.lua` read for this fan-out — possibly nil, which
+-- is why the capture seam below is updated before the nil guard.
+-- Returns whether pairing CLAIMED the keystroke: true once it has
+-- committed to reacting (a skip-over or a closer insert, landed or
+-- intercept-rejected), false on every decline. Pairing is last of the
+-- builtin consumers, so nothing currently observes that value; it is
+-- stated correctly so it stays correct when something does.
+local function on_typed_edit(rec)
   -- One-shot provenance (Q#AP9). Absence — paste, programmatic edit,
   -- manual hook run, rejected insert, a post-insert mutation by the
   -- command, stale `this_command` — is a silent non-event; only a
   -- live record for a pair-set character that then fails a gate
   -- reports.
-  local rec = ed.take_typed_edit and ed.take_typed_edit()
   if pmacs.pair._capture_records then pmacs.pair._last_record = rec end
-  if not rec then return end
+  if not rec then return false end
-  if not (ed.this_command and ed.this_command() == "buffer.self-insert") then return end
+  if not (ed.this_command and ed.this_command() == "buffer.self-insert") then return false end
 
   -- The master switch, per-buffer (Q#CR4): the SOURCE buffer of the
   -- typed edit, resolved buffer-local -> global -> default(true). A
   -- second buffer of the same language is untouched by a buffer-local
   -- override here (acceptance 29).
-  if not pmacs.config.get("editing.auto-pair", rec.buffer) then return end
+  if not pmacs.config.get("editing.auto-pair", rec.buffer) then return false end
 
   local buf = pmacs.window.buffer()
-  if not buf then return end
+  if not buf then return false end
 
   -- Relevance first (PR #110 round 1, finding 2): pairing has no
   -- interest in characters outside the set, so a transformed or
@@ -247,14 +265,14 @@ pmacs.hook.add("buffer.after-edit", function()
   -- Rust.
   local ch = rec.char
   local openers, closers = maps_for(set_for(rec.buffer))
-  if not (openers[ch] or closers[ch]) then return end
+  if not (openers[ch] or closers[ch]) then return false end
 
   -- Fail closed on a transformed source self-insert (Q#AP3): the
   -- intercept's positional result stands as produced; pairing on top
   -- of a relocated or expanded opener would compound it.
   if not rec.clean then
     ed.set_status("auto-pair skipped: source self-insert transformed")
-    return
+    return false
   end
   -- Fail closed when the source edit's context is no longer current:
   -- an intercept switched window/buffer, or something moved the
@@ -268,14 +286,14 @@ pmacs.hook.add("buffer.after-edit", function()
     or pmacs.window.current() ~= rec.window
     or ed.cursor() ~= rec.post_cursor then
     ed.set_status("auto-pair skipped: source context changed")
-    return
+    return false
   end
   -- Region guard (Q#AP3/Q#AP6): on the dispatch route type-over has
   -- already consumed and cleared the region. A region surviving the
   -- edit means the TUI's selection-blind optimistic gate let a custom
   -- pair char through (named deferral) — reacting would pile a closer
   -- onto an unconsumed region.
-  if ed.region() ~= nil then return end
+  if ed.region() ~= nil then return false end
 
   local cursor = rec.post_cursor
 
@@ -294,19 +312,19 @@ pmacs.hook.add("buffer.after-edit", function()
       if not ok then
         -- The duplicate stays (e.g. `())`); report, no retry.
         ed.set_status("auto-pair skip rejected by buffer intercept")
-        return
+        return true
       end
       if estart ~= cursor or estop ~= cursor + #ch or einserted ~= 0 then
         ed.set_status("auto-pair skip altered by buffer intercept")
         repair_cursor(win0, buf, cursor, estart, estop, einserted)
       end
-      return
+      return true
     end
   end
 
   local closer = openers[ch]
-  if not closer then return end
+  if not closer then return false end
-  if not should_pair(buf, cursor, closers) then return end
+  if not should_pair(buf, cursor, closers) then return false end
 
   local win0 = pmacs.window.current()
   local ok, estart, estop, einserted = pcall(function()
@@ -315,7 +333,7 @@ pmacs.hook.add("buffer.after-edit", function()
   if not ok then
     -- Nothing landed; the opener stands alone.
     ed.set_status("auto-pair closer rejected by buffer intercept")
-    return
+    return true
   end
   if estart ~= cursor or estop ~= cursor or einserted ~= #closer then
     ed.set_status("auto-pair closer altered by buffer intercept")
@@ -324,4 +342,11 @@ pmacs.hook.add("buffer.after-edit", function()
   -- Clean path: no cursor motion — the insert landed at the cursor
   -- and Lua mutators move no cursors, so it already sits between the
   -- pair; the daemon's per-tick CursorByte re-grounds both frontends.
-end)
+  return true
+end
+
+pmacs.typed_edit.add_consumer {
+  name = "auto-pair",
+  priority = 100,
+  fn = on_typed_edit,
+}

builtin/runtime/typed_edit.lua

@@ -0,0 +1,183 @@
+-- typed_edit.lua --- the typed-character consumer chain (Arc 8 Stage 4a).
+--
+-- `pmacs.editor.take_typed_edit()` is ONE-SHOT and per-frontend (Q#AP9):
+-- the first `buffer.after-edit` callback to call it clears the slot, and
+-- every later callback in the same fan-out --- including a nested manual
+-- `pmacs.hook.run` --- sees nil. That was survivable only because
+-- auto-pairing was the sole consumer, which was never a property anyone
+-- chose. A second independent caller gets nil or steals the record from
+-- pairing depending on hook registration order, and registration order
+-- is not a contract.
+--
+-- This module makes it one. It owns the single `buffer.after-edit`
+-- subscriber that reads the record, and offers that one read to
+-- consumers registered through `pmacs.typed_edit.add_consumer`:
+--
+--   local handle = pmacs.typed_edit.add_consumer {
+--     name = "auto-pair",     -- for error reporting
+--     priority = 100,         -- LOWEST runs FIRST
+--     fn = function(rec) ... return claimed end,
+--   }
+--   pmacs.typed_edit.remove_consumer(handle)  -- -> true if it was live
+--
+-- A consumer returns whether it CLAIMED the edit; the first that claims
+-- stops the chain. "Claimed" means the chain stops, not that an edit was
+-- made --- Stage 4b's abbreviation expander claims every keystroke that
+-- extends a pending abbreviation precisely so that auto-pairing does not
+-- also react to it (Q#LN22).
+--
+-- Priority is an explicit number rather than load-order-implied, because
+-- the ordering is load-bearing (Q#LN22: 64 Lean abbreviation keys
+-- contain a character in the `lean4` pair set, and pairing running first
+-- corrupts them) and a reader must be able to check it without
+-- reconstructing `src/editor.rs`'s include list.
+--
+-- ORDERING CONTRACT: this chunk loads BEFORE pair.lua, which registers
+-- into it, and therefore before lsp.lua. That preserves Q#AP7 --- see
+-- pair.lua's header and the load site in `src/editor.rs`.
+--
+-- Framing: docs/lean4-mode-framing.md Q#LN10.
+
+pmacs.typed_edit = pmacs.typed_edit or {}
+
+-- Consumers in run order: lowest `priority` first, registration order
+-- breaking ties. Maintained by ordered INSERTION rather than
+-- `table.sort`, which is not stable in Lua --- equal priorities would
+-- otherwise resolve arbitrarily, and "ties broken by registration
+-- order" is part of the stated contract, not an incidental property.
+local consumers = {}
+
+-- Handles are opaque to callers; only identity matters. An integer
+-- counter is enough because nothing ever reuses one.
+local next_handle = 0
+
+-- `math.huge` is the only portable spelling of infinity available in
+-- both LuaJIT and 5.4, and NaN is the only value not equal to itself.
+local INT32_MIN, INT32_MAX = -2147483648, 2147483647
+
+-- Register a typed-edit consumer; returns an opaque handle for
+-- `remove_consumer`. Argument errors throw: registration happens at
+-- chunk-load or config-load time, where a throw is a visible startup
+-- failure rather than a silently missing feature. Nothing in the
+-- after-edit path throws --- see the fan-out below.
+function pmacs.typed_edit.add_consumer(spec)
+  if type(spec) ~= "table" then
+    error("pmacs.typed_edit.add_consumer: spec must be a table", 2)
+  end
+  local name, priority, fn = spec.name, spec.priority, spec.fn
+  if type(name) ~= "string" or name == "" then
+    error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2)
+  end
+  -- A bare `type(priority) == "number"` admits NaN and the infinities,
+  -- and EVERY ordered comparison against NaN is false --- so a NaN
+  -- consumer silently lands wherever the insertion scan happens to give
+  -- up, and the lowest-first contract other consumers depend on stops
+  -- holding. Bounded integers match `pmacs.completion.register`, whose
+  -- priority is an i32 on the Rust side.
+  if type(priority) ~= "number" or priority ~= priority
+    or priority == math.huge or priority == -math.huge
+    or priority % 1 ~= 0
+    or priority < INT32_MIN or priority > INT32_MAX then
+    error("pmacs.typed_edit.add_consumer: " .. name ..
+      ": priority must be a finite integer in [-2147483648, 2147483647]", 2)
+  end
+  if type(fn) ~= "function" then
+    error("pmacs.typed_edit.add_consumer: " .. name ..
+      ": fn must be a function", 2)
+  end
+
+  -- STRICTLY-greater comparison, so a new consumer lands AFTER every
+  -- already-registered consumer of equal priority. That is exactly the
+  -- registration-order tiebreak; `>=` here would silently reverse it.
+  local at = #consumers + 1
+  for i, c in ipairs(consumers) do
+    if c.priority > priority then
+      at = i
+      break
+    end
+  end
+  next_handle = next_handle + 1
+  local handle = next_handle
+  table.insert(consumers, at,
+    { handle = handle, name = name, priority = priority, fn = fn })
+  return handle
+end
+
+-- Unregister a consumer by the handle `add_consumer` returned. Returns
+-- true if it was registered, false otherwise (so a double-remove is a
+-- reportable no-op rather than a throw). Without this, re-evaluating a
+-- config or reloading a package accumulates callbacks permanently ---
+-- the leak COHERENCE.md §13 already records against `pmacs.hook.add`,
+-- which this chain would otherwise inherit and spread.
+function pmacs.typed_edit.remove_consumer(handle)
+  for i, c in ipairs(consumers) do
+    if c.handle == handle then
+      table.remove(consumers, i)
+      return true
+    end
+  end
+  return false
+end
+
+pmacs.hook.add("buffer.after-edit", function()
+  local ed = pmacs.editor
+  -- ONE read for the whole fan-out (Q#AP9). The record may be nil ---
+  -- paste, programmatic mutation, manual hook run, a replicated CRDT
+  -- op, a stale `this_command` --- and consumers are called ANYWAY,
+  -- with nil. That is deliberate: "this fan-out carried no typed edit"
+  -- is information a consumer acts on. Auto-pairing's test seam
+  -- observes the non-event through it, and Stage 4b abandons a pending
+  -- abbreviation that an unrelated edit invalidated. Skipping the
+  -- fan-out on nil would leave both reading stale state.
+  local rec = ed.take_typed_edit and ed.take_typed_edit()
+
+  -- Iterate a SNAPSHOT. A consumer may register or remove consumers
+  -- while the chain is running, and `table.insert`/`table.remove` on
+  -- the live array shifts indices under `ipairs` --- a consumer that
+  -- registers a lower-priority one shifts itself forward and runs
+  -- twice, and repeating that is unbounded. Registrations and removals
+  -- made during a fan-out therefore take effect on the NEXT fan-out.
+  local snapshot = {}
+  for i, c in ipairs(consumers) do
+    snapshot[i] = c
+  end
+
+  for _, c in ipairs(snapshot) do
+    -- Each consumer gets its OWN copy of the record. The table handed
+    -- out is plain Lua data, so a declining consumer could otherwise
+    -- edit `rec.char` in place and the next consumer would act on the
+    -- forged value --- auto-pairing reads `rec.char` to decide what to
+    -- close, so a rewritten `char` makes it insert a pair the user
+    -- never typed. Every field is a scalar or an opaque id, so a
+    -- shallow copy is a complete snapshot.
+    local mine = nil
+    if rec ~= nil then
+      mine = {}
+      for k, v in pairs(rec) do
+        mine[k] = v
+      end
+    end
+
+    -- Contain the consumer. A throw here would skip every LATER
+    -- consumer in the chain and mark the whole `buffer.after-edit` run
+    -- failed; the other subscribers still run, because all-must-succeed
+    -- collects errors and continues (`src/hook.rs`'s
+    -- `run_all_must_succeed`), but one broken consumer must not be able
+    -- to silently disable the ones behind it. This matches pair.lua's
+    -- existing never-throw-from-after-edit discipline.
+    local ok, claimed = pcall(c.fn, mine)
+    if not ok then
+      -- Rendering is itself protected: a Lua error may be any value,
+      -- including a table whose `__tostring` throws, and an escaping
+      -- error here would defeat the containment above.
+      local shown, rendered = pcall(tostring, claimed)
+      if not shown or type(rendered) ~= "string" then
+        rendered = "<unprintable error>"
+      end
+      pcall(ed.set_status,
+        "typed-edit consumer '" .. c.name .. "' failed: " .. rendered)
+    elseif claimed then
+      return
+    end
+  end
+end)

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.
@@ -14,11 +14,13 @@ backlog.
   machine-local: `origin` may name this canonical URL, a release mirror,
   or something else, and therefore has no authority by name alone.
 - Canonical base at this snapshot:
-  `githubsucks/main` @ `d152120` (the bottom-panel landed-doc refresh #156
+  `githubsucks/main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a
-  atop the inline-math slice #158, dired Stage 1 #165, the GPU terminal
+  #167, the bottom-panel landed-doc refresh #156, the inline-math slice
-  input fix #166, Lean 4 Stage 2 #161, the dired framing #164,
+  #158, dired Stage 1 #165, the GPU terminal input fix #166, Lean 4
-  COHERENCE.md #163, find-file #162, Lean 4 Stage 1 #160, and the minimap
+  Stage 2 #161, the dired framing #164, COHERENCE.md #163, find-file
-  blank-slab fix #159; protocol v20).
+  #162, Lean 4 Stage 1 #160, and the minimap blank-slab fix #159;
+  protocol v20). The previous snapshot named `d152120`; the recovery
+  check below accepts it or anything newer.
 - On the transfer source, `origin/main` named a release mirror at
   `d3fa632` and lagged badly. On the current destination, `origin` names
   the canonical URL. This difference is why all recovery begins by
@@ -55,413 +57,172 @@ git status --short --branch
 The `git log` command must expose `d152120` or a newer intentional main.
 If it does not, stop and repair the remote/fetch configuration.
 
-## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED
+## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4a IN REVIEW
 
-- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
+- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`),
-  round, all twelve checks green). Branch `githubsucks/lean4-stage1`
+  #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full
-  retained; it was worked in the shared checkout (no sibling worktree).
+  histories were pruned from this ledger in round 6, per this file's own
-- Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as
+  instruction to remove entries when their PR merges; the durable facts
-  the branch's first commit (`a382965`) after three review rounds. **Seven
+  now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where
-  stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star:
+  a fresh machine should read them. `docs/lean4-mode-framing.md` rev 8
-  match or exceed VS Code's Lean support.
+  carries the decisions.
-- **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)
 
-- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout,
+### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`)
-  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` (branch `lean4-stage3a-seams`)
+- 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 8**. 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 7 review found one remaining P1 in acceptance 45i.** Rev 7
+  required A's pending abbreviation to survive B editing the same
+  buffer, while Q#LN22 also required an exact buffer-revision advance.
+  Those cannot both hold: revisions are buffer-global and every edit
+  bumps them. Rev 8 keeps the conservative guard and separates
+  ownership from survival — B cannot consume A's record, but B editing
+  the shared buffer invalidates A lazily; B switching buffers or
+  detaching remains frontend-scoped when no shared-buffer edit
+  intervenes.
+- **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
+  change. 4b is the input method. The split is forced by §4's own rule,
+  which Stage 4's risk column ("refactors `pair.lua`'s provenance read")
+  broke while the prose called the stage Lean-only.
+- **This is the SECOND consecutive re-scout to find that rule broken**
+  (round 4 found it for Stage 3). Rev 5 had even noticed the shape and
+  answered it with a commit boundary. **A commit boundary is not a review
+  boundary.** Re-check every remaining stage against §4 at scout time;
+  the rule is not self-enforcing.
+- **Rev 5's expansion semantics were wrong in three ways**, found by
+  reading `leanprover/vscode-lean4` @ `17d1d08` rather than inferring
+  from behavior. Resolution is *shortest key having the input as a
+  prefix* (`\al` → `∀` from `all`, not `alpha`); there is **no
+  terminator list** (`'+ '` is a key, so space extends after `\+`; `'\'`
+  is a key, so `\\` → `\`); and an unmatchable tail is **appended**,
+  not dropped (`\alp7` → `α7`).
+- **There is no cursor-motion hook**, so rev 5's acceptance 43 ("moving
+  the cursor out abandons it") was not buildable. Abandonment is lazy —
+  validated at the next typed edit — and the criterion now asserts what
+  pmacs can actually detect. Upstream drives this off `changeSelections`;
+  that seam does not exist here.
+- **`dispatch_key` is only half the production path for 4b.** The
+  auto-pair suite gets away with dispatch-only because Q#AP1 removed the
+  pair chars from the optimistic classifiers; `\` and the letters are
+  NOT excluded, so on a CRDT frontend the optimistic producer is the real
+  path. That producer is `#[cfg(feature = "crdt")]` and CI never enables
+  `crdt`, and the gate list runs `--features crdt` only for `--lib` — a
+  crdt-gated integration test is **dark twice over**.
+- The whole expansion has cross-peer-degraded undo (Q#LN21): six
+  source-peer optimistic inserts replaced by one daemon-peer op.
+  `set_round_trip_input` would fix it and is rejected — it also disables
+  `dispatch_idle`, so RET stops inserting a newline.
+- Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all
+  keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are
+  proper prefixes of another (so 1,550 expand eagerly), **26** values
+  carry `$CURSOR`, and **119** are multi-codepoint — the 26
+  `$CURSOR`-bearing values plus 93 others.
+- Citation sweep per COHERENCE §25: five live citations moved in the 50
+  commits since rev 5 — `take_typed_edit` 12827→12990,
+  `handle_server_requests` 1549→1815, `fs.stat` 93→133,
+  `detect_buffer_language` 452→457, `send_request`/`send_notification`
+  9342/9361→9507/9527.
+### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch)
 
-- Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @
+- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua`
-  `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first
+  (new), `pair.lua` re-expressed as one consumer,
-  two commits, then the implementation, then a bite-driven correction.
+  `src/editor.rs` +15 (the `include_str!` and its ordering comment), and
-- **Stage 2 merged as #161** (`main` @ `46a1b8f`, 2026-07-25, two review
+  `tests/typed_edit_chain_acceptance.rs` (new, 13 tests).
-  rounds). COHERENCE.md §7 records the slice; §1.2 records the dead
+  **`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat
-  `pmacs.error` channel found landing it.
+  main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is
-- **Framing rev 5 splits Stage 3 into 3a and 3b** because rev 4 broke its
+  criterion 46 checked at the diff, which is the only way it means
-  own §4 rule — the row read "two `lsp.lua` generalizations" under prose
+  anything.
-  claiming Stage 3 was Lean-only. One generalization shipped as Stage 2;
+- **The chain calls consumers even when the record is nil.** This is a
-  the other (Q#LN9's seams) is the shared event drain, so it is now its
+  decision, not an implementation detail: three existing auto-pairing
-  own substrate stage. 3a and 3b are **strictly sequential** — 3b's
+  tests assert `pmacs.pair._last_record == nil` after a record-less
-  subscriber is written against 3a's seam and both touch `lsp.lua`.
+  fan-out (paste, programmatic insert, nested manual `hook.run`), so
-- Ships: `pmacs.lsp.on_notification` / `on_response`, two arms in
+  skipping consumers on nil fails them. Stage 4b needs the same
-  `handle_server_requests`, a pending-response purge, and
+  delivery to abandon a pending abbreviation an unrelated edit
-  `pmacs.fs.canonicalize` (Q#LN20). No protocol change, no Lean content.
+  invalidated.
-- **Two framing claims were corrected during implementation**, both
+- **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and
-  recorded in §0.1 finding 6 and in the round-2 commit:
+  "ties broken by registration order" is a stated contract.
-  1. The reachable leak is **not** a killed buffer. The Rust core fires
+- **The chain `pcall`s each consumer** and reports through
-     exactly five hooks (`buffer.after-edit`, `buffer.after-load`,
+  `set_status`. Rev 7 justified this by claiming an uncontained throw
-     `buffer.after-switch`, `frontend.detached`, `process.after-tick`) —
+  would fail the fan-out for every other subscriber including lsp.lua's
-     **there is no buffer-kill hook**, so nothing tears an attachment
+  didChange flush; **that is wrong** — `run_all_must_succeed`
-     down and the drain keeps reaching that server. The real path is
+  (`src/hook.rs:332`) collects errors and continues, so the other
-     `attach_buffer` dropping a dead sid from `attachments` and
+  subscribers still run. The real consequence is narrower and still
-     rebuilding against a fresh server, which makes `crashed`/`stopped`
+  worth containing: the throw skips every LATER consumer in the chain.
-     the event *least* likely to be drained. Hence the purge polls
+  The rendering is protected too, because a Lua error may be a table
-     `pmacs.lsp.list()` rather than riding the drain.
+  whose `__tostring` throws.
-  2. Acceptance 32 does **not** pin "removed before invocation" —
+- **Round 8 (review) findings, all fixed on this branch:** each consumer
-     `pcall` catches the raise either way, so before/after is
+  now gets its **own shallow copy** of the record (the same table let a
-     unobservable without a re-entrant drain. It pins removal being
+  declining consumer rewrite `rec.char`, which pairing reads — typing
-     **unconditional**; renamed accordingly.
+  `x` could produce `x)`); the fan-out iterates a **snapshot** (a
-- **`pmacs._fs` is installed from `install_async`, not `install_project`**,
+  consumer registering a lower-priority one shifted itself forward under
-  purely for load order: `make_workspace` runs *after* `fs.lua` is
+  `ipairs` and ran twice, unbounded if repeated); `tostring` moved
-  evaluated, so a canonicalizer placed there reads nil. This cost one
+  inside the containment; **non-finite and non-integer priorities are
-  failing run to discover and is the kind of thing to check first.
+  rejected** (NaN is a number and every ordered comparison with it is
-- Bites recorded (all against the committed tree): removal gated on a
+  false, so it landed wherever the insertion scan gave up and silently
-  clean return → acc32 fails 2 != 1; an event-driven purge → the
+  voided the ordering contract); and `add_consumer` now returns a handle
-  no-attachment case fails "never called" while the attached case still
+  with `remove_consumer` beside it, so re-evaluating a config no longer
-  passes; a resolver without `canonicalize` → two servers (34b's own
+  leaks callbacks the way `pmacs.hook.add` does (COHERENCE §13).
-  falsification, which ships as a test).
+- **Every acceptance test is bite-verified by mutation**, per the
-- **Known unpinned:** the purge's generation (`attempt`) check. Reaching
+  standing rule that a test is not evidence until the mutation it
-  it needs a crash *and* its restart to fall in a gap with no
+  targets has been shown to fail it:
-  `_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 (branch `lean4-stage3b-server`)
+  | Mutation | Tests it fails |
+  |---|---|
+  | append instead of ordered insert | 5 chain |
+  | `>=` instead of `>` in the insert scan | 1 chain (tiebreak) |
+  | re-take the record per consumer | 4 chain |
+  | ignore the claim return value | 1 chain |
+  | drop the `pcall` | 1 chain |
+  | skip consumers when `rec == nil` | 1 chain + **3 auto-pair** |
+  | load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) |
+  | hand every consumer the same record table | 1 chain (46f) |
+  | iterate the live array instead of a snapshot | 1 chain (46g) |
+  | render the error outside the `pcall` | 1 chain (46d) |
+  | accept any Lua number as a priority | 1 chain (46h) |
+  | make `remove_consumer` a no-op | 2 chain (46g, 46h) |
 
-- Same worktree `../pmacs-lean-stage3`, **branched off
+  The first attempt at the last bite was WORTHLESS as written: moving
-  `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response
+  only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil
-  seam and `pmacs.fs.canonicalize`, so it is strictly sequential.
+  `add_consumer`, so the runtime failed to load and all 9 tests died —
-  **Retarget PR #170 to `main` BEFORE merging #167, not after** — the
+  loud, but not a test of the flush-ordering property. Moving
-  kill-ring lesson exactly. (Round 1 of this ledger entry stated the
+  `typed_edit.lua` AND `pair.lua` past `lsp.lua` is the faithful
-  reverse in its first sentence and the correct rule in the next; the
+  falsification: registration succeeds, the hook lands late, and exactly
-  review caught it. A safety rule written twice with opposite senses is
+  the three ordering tests fail. **A bite that kills everything has not
-  worse than not written.)
+  isolated anything.**
-- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in
+- Verification on this branch (commit-then-gate, so this describes the
-  `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`,
+  pushed tree): `cargo fmt --check` clean; strict workspace Clippy
-  a `leanprogress` mode plus `waitForDiagnostics` validation on
+  clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45;
-  `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (40 tests).
+  typed-edit chain 13/13 (and 13/13 again under `--no-default-features
-  No protocol change.
+  --features lua54`, since the fixes touch `math.huge`, `%`, and
-- **Stage 1's acceptance 12 is half superseded and was rewritten, not
+  `__tostring` behavior that differs between the backends); M4 121;
-  deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a
+  required GPU 202; **isolated-config workspace sweep 3,332 across 97
-  Stage-3 front-run; 3b is that stage. What survives is the restraint
+  suites, zero failures** with `grep -c basedpyright` = 0; `git diff
-  half — constructing an editor spawns nothing though the config now
+  --check` clean.
-  names `lake`, and opening a Lean buffer with no server configured
+- Stage 4b (the input method) is NOT in this PR and not started.
-  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.)
 
 ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165)
 

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 —
+**Last updated: 2026-07-26, after Lean 4 stages 3a and 3b (#167, #170)
-the first mathematical typesetting in pmacs — following find-file (#162),
+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
+- `main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a #167, the
-  inline-math slice #158, dired Stage 1 #165, the GPU terminal input fix
+  bottom-panel landed-doc refresh #156, the inline-math slice #158,
-  #166, Lean 4 Stage 2 #161, the dired framing #164, COHERENCE.md #163,
+  dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2
-  find-file #162, Lean 4 Stage 1 #160, minimap blank-slab #159,
+  #161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean
-  bottom-panel Stage 1 #155). Protocol unchanged at **v20**. The bullets
+  4 Stage 1 #160, minimap blank-slab #159, bottom-panel Stage 1 #155).
-  below describe the arcs in their own terms; this line is the
+  Protocol unchanged at **v20**. The bullets below describe the arcs in
-  head-of-`main` anchor.
+  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,72 @@ 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.
+  - **Stage 4a (typed-edit consumer chain) is implemented and in review
+    as PR #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev
+    8). It is substrate only: `builtin/runtime/typed_edit.lua` owns the
+    single `buffer.after-edit` subscriber and the single one-shot read,
+    `pair.lua` becomes its first registered consumer, and
+    `tests/auto_pair_acceptance.rs` is unchanged by zero lines
+    (criterion 46, verified at the diff). No protocol change, no Lean
+    content. The three decisions that turned out load-bearing rather
+    than stylistic: consumers are called **even when the record is
+    nil** (three existing auto-pair tests assert the non-event through
+    it, and 4b abandons stale pending state on it); each consumer gets
+    its **own copy** of the record, because pairing reads `rec.char`
+    and a declining consumer could otherwise forge it; and the fan-out
+    iterates a **snapshot**, because a consumer that registers a
+    lower-priority one shifts itself forward under `ipairs` and runs
+    twice.
+  - Remaining: Stage 4b (the Unicode input method) is framed and
+    awaiting approval — not started; 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

src/editor.rs

@@ -415,6 +415,18 @@ impl EditorState {
                 include_str!("../builtin/runtime/listview.lua"),
             )
             .expect("load listview builtin chunk");
+        // The typed-edit consumer chain (Arc 8 Stage 4a, Q#LN10) —
+        // ORDERING CONTRACT: typed_edit.lua must load BEFORE pair.lua,
+        // which registers a consumer into it, and therefore before
+        // lsp.lua. It owns the single `buffer.after-edit` subscriber
+        // that reads the one-shot typed-edit record, so its
+        // registration position is what preserves Q#AP7 below.
+        lua_host
+            .eval(
+                Some("@pmacs/builtin/runtime/typed_edit.lua"),
+                include_str!("../builtin/runtime/typed_edit.lua"),
+            )
+            .expect("load typed_edit builtin chunk");
         // Auto-pairing (Arc 2, Q#AP7) — ORDERING CONTRACT: pair.lua
         // must load BEFORE lsp.lua. Hook callbacks run in registration
         // order, and lsp.lua's `buffer.after-edit` callback flushes
@@ -424,6 +436,9 @@ impl EditorState {
         // the closer stays unsynchronized until the next edit (hook
         // edits don't re-fire the hook). pair.lua's `pmacs.lsp.*`
         // lookups are lazy and nil-guarded for the same reason.
+        // Since Stage 4a the closer is inserted from the chain's
+        // subscriber rather than pair.lua's own, which is registered
+        // one chunk earlier — strictly safer for this contract.
         lua_host
             .eval(
                 Some("@pmacs/builtin/runtime/pair.lua"),

tests/typed_edit_chain_acceptance.rs

@@ -0,0 +1,735 @@
+//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a,
+//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46h).
+//!
+//! The chain owns the single `buffer.after-edit` subscriber that reads
+//! the one-shot typed-edit record (Q#AP9) and offers it to consumers in
+//! priority order. These tests pin the chain's OWN behavior — take-once,
+//! priority ordering, claim-stops-chain, throw containment, per-consumer
+//! record isolation, snapshot iteration under re-entrant registration,
+//! the registration lifecycle, and the Q#AP7 flush ordering it inherited
+//! from `pair.lua`.
+//!
+//! They deliberately do not re-test auto-pairing: criterion 46 requires
+//! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that
+//! suite is the no-behavior-change pin. Pairing appears here only as
+//! the chain's last consumer, which is how 46c observes that a claim
+//! really stopped the chain.
+//!
+//! Dispatch-driven throughout: `dispatch_key` is the producer that arms
+//! the record for a grid frontend.
+
+use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
+use pmacs::editor::EditorState;
+use pmacs::lua_bindings::StateDir;
+use pmacs::protocol::FrontendId;
+use std::path::PathBuf;
+use std::sync::atomic::{AtomicUsize, Ordering};
+use std::time::{Duration, Instant};
+
+fn fresh_state_dir() -> PathBuf {
+    static SEQ: AtomicUsize = AtomicUsize::new(0);
+    let dir = std::env::temp_dir().join(format!(
+        "pmacs-typededit-{}-{}",
+        std::process::id(),
+        SEQ.fetch_add(1, Ordering::Relaxed)
+    ));
+    std::fs::create_dir_all(&dir).unwrap();
+    dir
+}
+
+fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent {
+    KeyEvent {
+        code,
+        modifiers: mods,
+        kind: KeyEventKind::Press,
+        state: KeyEventState::NONE,
+    }
+}
+
+fn type_str(s: &mut EditorState, text: &str) {
+    for ch in text.chars() {
+        s.dispatch_key(
+            FrontendId::LOCAL,
+            key(KeyCode::Char(ch), KeyModifiers::NONE),
+        );
+    }
+}
+
+fn exec(s: &EditorState, src: &str) {
+    s.lua_host.lua().load(src.to_string()).exec().unwrap();
+}
+
+fn eval<T: mlua::FromLuaMulti>(s: &EditorState, src: &str) -> T {
+    s.lua_host.lua().load(src.to_string()).eval().unwrap()
+}
+
+fn buffer_text(s: &EditorState) -> String {
+    let b: mlua::String = eval(
+        s,
+        "local b = pmacs.window.buffer(); return b:slice(0, b:len())",
+    );
+    String::from_utf8_lossy(&b.as_bytes()).into_owned()
+}
+
+fn status(s: &EditorState) -> String {
+    s.core.borrow().status.clone()
+}
+
+/// Fresh scratch-buffer editor, cursor at 0. Scratch pairing uses the
+/// `default` set, so `(` pairs — which is what 46c reads.
+fn editor_with(body: &str) -> EditorState {
+    let s = EditorState::new();
+    if !body.is_empty() {
+        exec(&s, &format!("pmacs.window.buffer():insert(0, {body:?})"));
+    }
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    s
+}
+
+// ---------------------------------------------------------------------------
+// 46a — one read for the whole fan-out
+// ---------------------------------------------------------------------------
+
+#[test]
+fn chain_reads_the_record_once_and_hands_the_same_one_to_every_consumer() {
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.seen = {}
+        local function spy(tag)
+          return function(rec)
+            -- Each consumer independently attempts its own take. Under
+            -- the pre-chain design this is exactly what a second
+            -- consumer would have done, and exactly what would have
+            -- returned nil (or stolen the record from pairing).
+            local own = pmacs.editor.take_typed_edit()
+            _G.seen[#_G.seen + 1] = {
+              tag = tag,
+              char = rec and rec.char,
+              post_cursor = rec and rec.post_cursor,
+              clean = rec and rec.clean,
+              own_take_was_nil = (own == nil),
+            }
+            return false
+          end
+        end
+        pmacs.typed_edit.add_consumer { name = "spy-a", priority = 1, fn = spy("a") }
+        pmacs.typed_edit.add_consumer { name = "spy-b", priority = 2, fn = spy("b") }
+        "#,
+    );
+
+    type_str(&mut s, "x");
+
+    let (n, a_char, b_char, a_pc, b_pc, a_clean, b_clean, a_nil, b_nil): (
+        i64,
+        String,
+        String,
+        i64,
+        i64,
+        bool,
+        bool,
+        bool,
+        bool,
+    ) = eval(
+        &s,
+        "
+        local a, b = _G.seen[1], _G.seen[2]
+        return #_G.seen, a.char, b.char, a.post_cursor, b.post_cursor,
+               a.clean, b.clean, a.own_take_was_nil, b.own_take_was_nil
+        ",
+    );
+
+    assert_eq!(n, 2, "both consumers ran for one typed character");
+    // The same record, not two reads of a slot that only one could win.
+    assert_eq!(a_char, "x");
+    assert_eq!(b_char, "x", "the second consumer sees the record too");
+    assert_eq!((a_pc, b_pc), (1, 1), "identical post_cursor");
+    assert!(a_clean && b_clean, "identical clean verdict");
+    // ...and the chain, not the consumers, did the taking.
+    assert!(
+        a_nil && b_nil,
+        "a consumer's own take_typed_edit() observes nil — the chain \
+         already consumed the one-shot slot (Q#AP9)"
+    );
+}
+
+#[test]
+fn consumers_run_when_the_fan_out_carries_no_record() {
+    // The chain calls consumers with nil rather than skipping them.
+    // Three tests in the auto-pairing suite depend on this (they assert
+    // `_last_record == nil` after a record-less fan-out), so it is a
+    // load-bearing decision and not an implementation detail.
+    let s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.calls, _G.nil_calls = 0, 0
+        pmacs.typed_edit.add_consumer {
+          name = "nil-spy", priority = 1,
+          fn = function(rec)
+            _G.calls = _G.calls + 1
+            if rec == nil then _G.nil_calls = _G.nil_calls + 1 end
+            return false
+          end,
+        }
+        "#,
+    );
+
+    // A manual fan-out arms no record.
+    exec(&s, "pmacs.hook.run(\"buffer.after-edit\")");
+
+    let (calls, nil_calls): (i64, i64) = eval(&s, "return _G.calls, _G.nil_calls");
+    assert_eq!(calls, 1, "the consumer ran");
+    assert_eq!(nil_calls, 1, "and was handed nil, not skipped");
+}
+
+// ---------------------------------------------------------------------------
+// 46b — priority order, not registration order
+// ---------------------------------------------------------------------------
+
+#[test]
+fn consumers_run_in_priority_order_not_registration_order() {
+    let mut s = editor_with("");
+    // Registered HIGH priority first. If the chain honored registration
+    // order (or `include_str!` order, which is the same failure dressed
+    // differently), the observed order would be the registration order.
+    exec(
+        &s,
+        r#"
+        _G.order = {}
+        local function mark(tag)
+          return function() _G.order[#_G.order + 1] = tag; return false end
+        end
+        pmacs.typed_edit.add_consumer { name = "late",  priority = 30, fn = mark("late") }
+        pmacs.typed_edit.add_consumer { name = "early", priority = 10, fn = mark("early") }
+        pmacs.typed_edit.add_consumer { name = "mid",   priority = 20, fn = mark("mid") }
+        "#,
+    );
+
+    type_str(&mut s, "x");
+
+    let order: String = eval(&s, "return table.concat(_G.order, ',')");
+    assert_eq!(
+        order, "early,mid,late",
+        "lowest priority runs first, regardless of when it registered"
+    );
+}
+
+#[test]
+fn equal_priorities_break_by_registration_order() {
+    // The stated tiebreak. Lua's `table.sort` is not stable, so this
+    // bites an implementation that sorts instead of inserting in place.
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.order = {}
+        local function mark(tag)
+          return function() _G.order[#_G.order + 1] = tag; return false end
+        end
+        pmacs.typed_edit.add_consumer { name = "first",  priority = 5, fn = mark("first") }
+        pmacs.typed_edit.add_consumer { name = "second", priority = 5, fn = mark("second") }
+        pmacs.typed_edit.add_consumer { name = "third",  priority = 5, fn = mark("third") }
+        "#,
+    );
+
+    type_str(&mut s, "x");
+
+    let order: String = eval(&s, "return table.concat(_G.order, ',')");
+    assert_eq!(order, "first,second,third");
+}
+
+// ---------------------------------------------------------------------------
+// 46c — a claim stops the chain
+// ---------------------------------------------------------------------------
+
+#[test]
+fn a_claiming_consumer_stops_the_chain() {
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.later_ran = false
+        pmacs.typed_edit.add_consumer {
+          name = "claimer", priority = 1, fn = function() return true end,
+        }
+        pmacs.typed_edit.add_consumer {
+          name = "later", priority = 2,
+          fn = function() _G.later_ran = true; return false end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "(");
+
+    let later_ran: bool = eval(&s, "return _G.later_ran");
+    assert!(!later_ran, "a later consumer must not run after a claim");
+    // Pairing is the chain's last consumer at priority 100, so the
+    // claim is observable in the buffer: no closer was inserted. This
+    // is the assertion that makes the criterion about behavior rather
+    // than about a bookkeeping flag.
+    assert_eq!(
+        buffer_text(&s),
+        "(",
+        "auto-pairing never ran, so the opener stands alone"
+    );
+}
+
+#[test]
+fn a_non_claiming_consumer_does_not_stop_the_chain() {
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.later_ran = false
+        pmacs.typed_edit.add_consumer {
+          name = "passer", priority = 1, fn = function() return false end,
+        }
+        pmacs.typed_edit.add_consumer {
+          name = "later", priority = 2,
+          fn = function() _G.later_ran = true; return false end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "(");
+
+    let later_ran: bool = eval(&s, "return _G.later_ran");
+    assert!(later_ran, "a declining consumer passes the edit along");
+    assert_eq!(
+        buffer_text(&s),
+        "()",
+        "and pairing, still last in the chain, reacted normally"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// 46d — a throwing consumer is contained
+// ---------------------------------------------------------------------------
+
+#[test]
+fn a_throwing_consumer_is_contained_reported_and_does_not_stop_the_chain() {
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.later_ran = false
+        pmacs.typed_edit.add_consumer {
+          name = "boom", priority = 1,
+          fn = function() error("consumer exploded") end,
+        }
+        pmacs.typed_edit.add_consumer {
+          name = "later", priority = 2,
+          fn = function() _G.later_ran = true; return false end,
+        }
+        "#,
+    );
+
+    // An uncontained throw would abandon every LATER consumer in the
+    // chain and mark the whole `buffer.after-edit` run failed. It would
+    // NOT stop the hook's other subscribers — all-must-succeed collects
+    // errors and keeps going (`src/hook.rs`'s `run_all_must_succeed`) —
+    // so what this pins is that one broken consumer cannot silently
+    // disable the ones behind it.
+    type_str(&mut s, "(");
+
+    let later_ran: bool = eval(&s, "return _G.later_ran");
+    assert!(later_ran, "a throwing consumer must not stop the chain");
+    assert_eq!(
+        buffer_text(&s),
+        "()",
+        "and pairing still ran — the fan-out survived the throw"
+    );
+    let st = status(&s);
+    assert!(
+        st.contains("boom") && st.contains("consumer exploded"),
+        "the failure is reported by consumer name and message, got {st:?}"
+    );
+}
+
+#[test]
+fn add_consumer_rejects_malformed_registrations() {
+    let s = editor_with("");
+    for (src, want) in [
+        (
+            "pmacs.typed_edit.add_consumer(\"nope\")",
+            "spec must be a table",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ priority = 1, fn = function() end }",
+            "name must be a non-empty string",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }",
+            "priority must be a finite integer",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }",
+            "fn must be a function",
+        ),
+        // NaN is a number and every ordered comparison with it is
+        // false, so a bare type check lets it land wherever the
+        // insertion scan gives up — and the lowest-first contract the
+        // Lean expander depends on quietly stops holding. The
+        // infinities and non-integers go with it: priority matches
+        // `pmacs.completion.register`'s i32.
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 0/0, \
+             fn = function() end }",
+            "priority must be a finite integer",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", priority = math.huge, \
+             fn = function() end }",
+            "priority must be a finite integer",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", priority = -math.huge, \
+             fn = function() end }",
+            "priority must be a finite integer",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1.5, \
+             fn = function() end }",
+            "priority must be a finite integer",
+        ),
+        (
+            "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 4e9, \
+             fn = function() end }",
+            "priority must be a finite integer",
+        ),
+    ] {
+        let err = s
+            .lua_host
+            .lua()
+            .load(src.to_string())
+            .exec()
+            .expect_err("malformed registration must throw");
+        let msg = err.to_string();
+        assert!(
+            msg.contains(want),
+            "expected {want:?} in the error for {src:?}, got {msg:?}"
+        );
+    }
+}
+
+#[test]
+fn an_error_whose_rendering_throws_is_still_contained() {
+    // A Lua error may be any value, including a table whose
+    // `__tostring` throws. Rendering it outside the containment is a
+    // second, uncontained throw — the chain would stop at exactly the
+    // consumer it was trying to report.
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.later_ran = false
+        local hostile = setmetatable({}, {
+          __tostring = function() error("rendering exploded") end,
+        })
+        pmacs.typed_edit.add_consumer {
+          name = "boom", priority = 1, fn = function() error(hostile) end,
+        }
+        pmacs.typed_edit.add_consumer {
+          name = "later", priority = 2,
+          fn = function() _G.later_ran = true; return false end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "(");
+
+    let later_ran: bool = eval(&s, "return _G.later_ran");
+    assert!(
+        later_ran,
+        "an unrenderable error must not escape the containment"
+    );
+    assert_eq!(buffer_text(&s), "()", "and pairing still ran");
+    let st = status(&s);
+    assert!(
+        st.contains("boom") && st.contains("<unprintable error>"),
+        "the consumer is still named, with a placeholder body, got {st:?}"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// The record a consumer sees is its own
+// ---------------------------------------------------------------------------
+
+#[test]
+fn a_consumers_mutation_of_the_record_cannot_reach_the_next_consumer() {
+    // The record is plain Lua data. Handing every consumer the same
+    // table lets a DECLINING consumer rewrite provenance for the ones
+    // behind it — and pairing decides what to close from `rec.char`,
+    // so a forged `char` makes it insert a pair the user never typed.
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.downstream_char = "unset"
+        pmacs.typed_edit.add_consumer {
+          name = "vandal", priority = 1,
+          fn = function(rec)
+            if rec then rec.char = "("; rec.codepoint = 40 end
+            return false
+          end,
+        }
+        pmacs.typed_edit.add_consumer {
+          name = "witness", priority = 2,
+          fn = function(rec)
+            _G.downstream_char = rec and rec.char or "nil"
+            return false
+          end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "x");
+
+    let downstream: String = eval(&s, "return _G.downstream_char");
+    assert_eq!(
+        downstream, "x",
+        "the next consumer sees the real typed character"
+    );
+    assert_eq!(
+        buffer_text(&s),
+        "x",
+        "and pairing, reading the same field, did not close a forged opener"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Re-entrant registration, and the consumer lifecycle
+// ---------------------------------------------------------------------------
+
+#[test]
+fn registering_or_removing_during_a_fan_out_takes_effect_on_the_next_one() {
+    // The fan-out iterates a snapshot. Iterating the live array instead
+    // lets a consumer that registers a LOWER-priority one shift itself
+    // forward under `ipairs` and run twice in a single fan-out — and
+    // repeating the registration makes that unbounded.
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.order = {}
+        local function mark(tag)
+          return function() _G.order[#_G.order + 1] = tag; return false end
+        end
+        _G.doomed = pmacs.typed_edit.add_consumer {
+          name = "doomed", priority = 50, fn = mark("doomed"),
+        }
+        _G.did_register = false
+        pmacs.typed_edit.add_consumer {
+          name = "a", priority = 10,
+          fn = function()
+            _G.order[#_G.order + 1] = "a"
+            if not _G.did_register then
+              _G.did_register = true
+              pmacs.typed_edit.add_consumer { name = "b", priority = 5, fn = mark("b") }
+              pmacs.typed_edit.remove_consumer(_G.doomed)
+            end
+            return false
+          end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "x");
+    let first: String = eval(&s, "return table.concat(_G.order, ',')");
+    assert_eq!(
+        first, "a,doomed",
+        "`a` runs once even though it registered ahead of itself, and \
+         `doomed` still runs in the fan-out it was removed during"
+    );
+
+    exec(&s, "_G.order = {}");
+    type_str(&mut s, "y");
+    let second: String = eval(&s, "return table.concat(_G.order, ',')");
+    assert_eq!(
+        second, "b,a",
+        "both the registration and the removal land on the next fan-out"
+    );
+}
+
+#[test]
+fn remove_consumer_unregisters_and_reports_whether_it_was_live() {
+    // Without removal, re-evaluating a config or reloading a package
+    // accumulates callbacks permanently — the leak COHERENCE.md §13
+    // already records against `pmacs.hook.add`. A chain with no
+    // teardown would inherit it and spread it to every consumer.
+    let mut s = editor_with("");
+    exec(
+        &s,
+        r#"
+        _G.runs = 0
+        _G.h = pmacs.typed_edit.add_consumer {
+          name = "temporary", priority = 1,
+          fn = function() _G.runs = _G.runs + 1; return false end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "x");
+    let runs: i64 = eval(&s, "return _G.runs");
+    assert_eq!(runs, 1, "registered consumers run");
+
+    let first_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)");
+    let second_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)");
+    assert!(first_removal, "removing a live consumer reports true");
+    assert!(
+        !second_removal,
+        "a double-remove is a reportable no-op, not a throw"
+    );
+
+    type_str(&mut s, "y");
+    let runs: i64 = eval(&s, "return _G.runs");
+    assert_eq!(runs, 1, "the removed consumer no longer runs");
+    // Removal is surgical: the chain itself, and pairing on it, survive.
+    exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())");
+    type_str(&mut s, "(");
+    assert_eq!(
+        buffer_text(&s),
+        "xy()",
+        "the rest of the chain is untouched"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// 46e — the Q#AP7 flush ordering the chain inherited
+// ---------------------------------------------------------------------------
+
+fn fake_lsp_path() -> String {
+    env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned()
+}
+
+fn pump_lua_flag(state: &mut EditorState, flag: &str, secs: u64) -> bool {
+    let deadline = Instant::now() + Duration::from_secs(secs);
+    loop {
+        state.tick_processes();
+        state.tick_lsp();
+        state.tick_async();
+        let done: bool = state
+            .lua_host
+            .lua()
+            .load(format!("return ({flag}) == true"))
+            .eval()
+            .unwrap_or(false);
+        if done {
+            return true;
+        }
+        if Instant::now() >= deadline {
+            return false;
+        }
+        std::thread::sleep(Duration::from_millis(10));
+    }
+}
+
+/// The `text` of every `textDocument/didChange` line in the sink, in
+/// arrival order.
+fn did_change_texts(sink: &std::path::Path) -> Vec<String> {
+    let Ok(raw) = std::fs::read_to_string(sink) else {
+        return Vec::new();
+    };
+    raw.lines()
+        .filter_map(|l| serde_json::from_str::<serde_json::Value>(l).ok())
+        .filter(|v| v.get("method").and_then(|m| m.as_str()) == Some("textDocument/didChange"))
+        .filter_map(|v| v.get("text").and_then(|t| t.as_str()).map(str::to_owned))
+        .collect()
+}
+
+#[test]
+fn a_chain_consumers_edit_reaches_the_first_did_change() {
+    // Q#AP7 generalized from pairing to the chain: lsp.lua's after-edit
+    // callback flushes didChange SYNCHRONOUSLY on the signature-trigger
+    // path, so every reaction to a typed character must already be in
+    // the buffer when it runs. The auto-pairing suite pins this for
+    // pairing; this pins it for the chain itself, which is what now
+    // owns the registration position.
+    //
+    // Falsified by loading typed_edit.lua after lsp.lua in
+    // `src/editor.rs`: the consumer's text would then arrive in the
+    // SECOND didChange, or not at all.
+    let dir = fresh_state_dir();
+    let sink = dir.join("changes.jsonl");
+    let sink_disp = sink.display().to_string();
+    let fake = fake_lsp_path();
+
+    let mut s = EditorState::new();
+    s.lua_host.lua().remove_app_data::<StateDir>();
+    s.lua_host.lua().set_app_data(StateDir(dir.clone()));
+    exec(&s, "pmacs.lsp.config = {}");
+    exec(
+        &s,
+        &format!(
+            "pmacs.lsp.config.rust = {{
+               command = '{fake}',
+               env = {{
+                 PMACS_FAKE_LSP_MODE = 'sighelp',
+                 PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}',
+               }},
+             }}"
+        ),
+    );
+
+    // A consumer that appends a marker of its own, ahead of pairing.
+    // It declines the claim so pairing still runs — the assertion is
+    // about ordering against the flush, not about claiming.
+    exec(
+        &s,
+        r#"
+        pmacs.typed_edit.add_consumer {
+          name = "marker", priority = 1,
+          fn = function(rec)
+            if not rec then return false end
+            if rec.char ~= "(" then return false end
+            local buf = pmacs.window.buffer()
+            buf:insert(buf:len(), "Z")
+            return false
+          end,
+        }
+        "#,
+    );
+
+    let f = dir.join("a.rs");
+    std::fs::write(&f, "\n").unwrap();
+    let fd = f.display().to_string();
+    exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})"));
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    let initialized = "(function() \
+       for _,r in ipairs(pmacs.lsp.list()) do \
+         if r.state and r.state.kind=='initialized' then return true end \
+       end \
+       return false \
+     end)()";
+    assert!(pump_lua_flag(&mut s, initialized, 5), "fake server init");
+
+    type_str(&mut s, "(");
+    assert_eq!(
+        buffer_text(&s),
+        "()\nZ",
+        "both the chain consumer's marker and pairing's closer landed"
+    );
+
+    let deadline = Instant::now() + Duration::from_secs(5);
+    let changes = loop {
+        s.tick_processes();
+        s.tick_lsp();
+        s.tick_async();
+        let c = did_change_texts(&sink);
+        if !c.is_empty() {
+            break c;
+        }
+        assert!(
+            Instant::now() < deadline,
+            "no didChange reached the fake server"
+        );
+        std::thread::sleep(Duration::from_millis(10));
+    };
+    assert_eq!(
+        changes[0], "()\nZ",
+        "the FIRST didChange carries BOTH reactions — the chain ran \
+         before lsp.lua's synchronous flush (Q#AP7)"
+    );
+}