diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua
index da24378..7b205d2 100644
--- a/builtin/runtime/lean_input.lua
+++ b/builtin/runtime/lean_input.lua
@@ -124,6 +124,10 @@ end
 -- TUI-plus-GPU configuration this project ships.
 local pending = {}
 
+-- Expansions the chain consumer decided on but did NOT perform, keyed
+-- the same way. See `run_deferred` below for why they wait.
+local deferred = {}
+
 local function frontend_id()
   local ok, id = pcall(function() return pmacs.frontend.id() end)
   if ok then return id end
@@ -157,19 +161,38 @@ end
 -- Expansion
 -- ---------------------------------------------------------------------
 
--- Replace the pending span with `symbol`, placing the point at
--- `$CURSOR` if the symbol carries one. Returns the byte offset just
--- past the replacement, or nil when the edit was rejected or altered.
+-- Right-gravity translation of `pos` through the effective edit —
+-- pair.lua's shape, for the same reason: the point sits AFTER the
+-- replaced span (on the terminator, or on a closer pairing inserted)
+-- and has to move with it.
+local function translate(pos, estart, estop, einserted)
+  if pos < estart then return pos end
+  if pos > estop then return pos - (estop - estart) + einserted end
+  return estart + einserted
+end
+
+-- Replace the pending span (leader + typed text) with `symbol`.
 --
--- ONE `buf:replace` for the whole expansion: one undo step, one CRDT
--- op, one effective-edit verification. A rejection drops the pending
--- state and does not retry, the same discipline as comment.lua's Q#CT5
--- and pair.lua.
-local function expand(buf, p, symbol, span_end)
+-- The span deliberately STOPS BEFORE the terminator. Including the
+-- terminator would make the expansion and the terminator one edit, but
+-- it would also swallow whatever auto-pairing did with that terminator
+-- — and a pair character is a legal terminator (`\alp(`). One undo
+-- restores the same text either way, because the terminator was its own
+-- insert to begin with.
+--
+-- ONE `buf:replace`: one undo step, one CRDT op, one effective-edit
+-- verification. A rejection drops the pending state and does not retry,
+-- the same discipline as comment.lua's Q#CT5 and pair.lua.
+local function expand(buf, start, span_end, symbol)
   local cursor_at = symbol:find(CURSOR, 1, true)
   local text = cursor_at and (symbol:gsub("%$CURSOR", "", 1)) or symbol
 
-  local start = p.start_offset
+  -- The context to compare against AFTER the edit. A buffer intercept
+  -- may switch window or buffer while the replace runs; the point in
+  -- whatever it switched to is not ours to move.
+  local win0 = pmacs.window.current()
+  local point0 = ed.cursor()
+
   local ok, estart, estop, einserted = pcall(function()
     return buf:replace(start, span_end, text)
   end)
@@ -188,7 +211,17 @@ local function expand(buf, p, symbol, span_end)
   -- the new end. Every later self-insert is then silently rejected and
   -- the editor looks dead. There is no daemon re-grounding that covers
   -- this; that only holds for an edit that lands at the cursor.
-  ed.goto_byte(cursor_at and (start + cursor_at - 1) or (start + #text))
+  --
+  -- Context-guarded exactly as pair.lua's `repair_cursor` is: if the
+  -- intercept switched us elsewhere, `goto_byte` would move the point
+  -- of a buffer that has nothing to do with this expansion.
+  if pmacs.window.current() == win0 and pmacs.window.buffer() == buf then
+    if cursor_at then
+      ed.goto_byte(start + cursor_at - 1)
+    else
+      ed.goto_byte(translate(point0, estart, estop, einserted))
+    end
+  end
   return start + #text
 end
 
@@ -245,6 +278,15 @@ local function on_typed_edit(rec)
     pending[fid] = nil
     return false
   end
+  -- ...and on a source edit whose context is no longer current. The
+  -- buffer and window matching is not enough: a redefined self-insert
+  -- can insert the character and THEN move the point, and expanding
+  -- over a span the user has left teleports them back into it. Pairing
+  -- makes the same three-part check for the same reason.
+  if ed.cursor() ~= rec.post_cursor then
+    pending[fid] = nil
+    return false
+  end
 
   local revision
   do
@@ -287,55 +329,114 @@ local function on_typed_edit(rec)
     p.text = extended
     p.expected_revision = revision
     if eager[extended] then
-      local span_end = p.start_offset + 1 + #extended
       pending[fid] = nil
-      expand(buf, p, best[extended].symbol, span_end)
+      deferred[fid] = {
+        buffer = rec.buffer,
+        window = rec.window,
+        start_offset = p.start_offset,
+        text = extended,
+        symbol = best[extended].symbol,
+        re_arm = false,
+      }
     end
     -- Claimed either way: an extension that has not yet completed must
-    -- NOT reach auto-pairing (`\[` in `\[[]]`).
+    -- NOT reach auto-pairing (`\[` in `\[[]]`), and a completing one is
+    -- part of the abbreviation, not a character pairing should react to.
     return true
   end
 
-  -- `ch` does not extend the abbreviation. Expand what is pending
-  -- FIRST, then let `ch` stand as ordinary text — the terminator is
-  -- retained, not consumed, and it sits inside the replaced span so the
-  -- whole thing is one undo step.
+  -- `ch` does not extend the abbreviation: it TERMINATES it, and a
+  -- terminator is an ordinary character that auto-pairing is entitled
+  -- to react to (`\alp(` must give `α()`). So the expansion is
+  -- DEFERRED to the subscriber below and this returns false, leaving
+  -- pairing a record whose offsets still describe the buffer.
+  --
+  -- Expanding here and returning false would not do: the replace makes
+  -- pairing's copy of the record stale, so pairing declines and the
+  -- closer is silently lost. Expanding here and returning true is
+  -- worse — it is what shipped in the first revision of this file, and
+  -- it makes every pair-character terminator silently unpaired.
   pending[fid] = nil
-  local hit = best[p.text]
-  local after
-  if hit and #p.text > 0 then
-    -- `span_end` covers the terminator: the leader, the pending text,
-    -- and `ch`, which has already landed. What replaces it is the
-    -- symbol followed by `ch` itself.
-    local span_end = p.start_offset + 1 + #p.text + #ch
-    after = expand(buf, p, hit.symbol .. ch, span_end)
+  if best[p.text] and #p.text > 0 then
+    deferred[fid] = {
+      buffer = rec.buffer,
+      window = rec.window,
+      start_offset = p.start_offset,
+      text = p.text,
+      symbol = best[p.text].symbol,
+      -- A terminating `\` re-arms as a NEW leader at its own position
+      -- (`\al\to` → `∀→`). Upstream gets this from `processChange`,
+      -- where a finished abbreviation reports `isAffected = false` and
+      -- so does not suppress the new-leader branch. This is NOT the
+      -- `\\` case: there the pending text is empty, `\` EXTENDS, and
+      -- the result is one literal backslash with nothing left open.
+      re_arm = ch == LEADER,
+    }
+  elseif ch == LEADER then
+    -- Nothing to expand, but the leader still opens a fresh
+    -- abbreviation where it landed.
+    pending[fid] = {
+      buffer = rec.buffer,
+      window = rec.window,
+      start_offset = rec.effective_start,
+      text = "",
+      expected_revision = revision,
+    }
+    return true
   end
 
-  -- A terminating `\` re-arms as a NEW leader at its own position
-  -- (`\alpha\to` → `α→`). Upstream gets this from `processChange`,
-  -- where a finished abbreviation reports `isAffected = false` and so
-  -- does not suppress the new-leader branch. This is not the `\\` case:
-  -- there the pending text is empty, `\` EXTENDS, and the result is one
-  -- literal backslash with no pending state left open.
-  if ch == LEADER then
-    local start = after and (after - #ch) or rec.effective_start
-    local ok, rev = pcall(function() return buf:revision() end)
-    if ok then
+  return false
+end
+
+-- The deferred expansion, on its own `buffer.after-edit` subscriber.
+--
+-- It runs AFTER the whole typed-edit chain — this chunk loads after
+-- typed_edit.lua, and hook callbacks run in registration order — so
+-- auto-pairing has already reacted to the terminator by the time the
+-- expansion rewrites the text in front of it. Pairing's closer lands
+-- after the terminator, outside the replaced span, so it survives.
+--
+-- It must also run BEFORE lsp.lua's subscriber (Q#AP7): that one
+-- flushes `didChange` synchronously on the signature-trigger path, and
+-- a server told about `\alp ` instead of `α ` stays wrong until the
+-- next edit. This chunk loads before lsp.lua for exactly that reason.
+--
+-- A claim by ANY chain consumer stops the chain but not this — which
+-- is the point. Pairing claims the terminator it reacts to.
+local function run_deferred()
+  local fid = frontend_id()
+  if fid == nil then return end
+  local d = deferred[fid]
+  deferred[fid] = nil
+  if not d then return end
+
+  local buf = pmacs.window.buffer()
+  if not buf or buf ~= d.buffer or pmacs.window.current() ~= d.window then
+    return
+  end
+
+  -- The span must still hold exactly what was typed into it. Pairing
+  -- only edits at the point, which is past this span, so in practice
+  -- this holds; a buffer intercept is not obliged to be so polite.
+  local span_end = d.start_offset + 1 + #d.text
+  local ok, actual = pcall(function()
+    return buf:slice(d.start_offset, span_end)
+  end)
+  if not ok or actual ~= LEADER .. d.text then return end
+
+  local after = expand(buf, d.start_offset, span_end, d.symbol)
+  if after and d.re_arm then
+    local rev_ok, rev = pcall(function() return buf:revision() end)
+    if rev_ok then
       pending[fid] = {
-        buffer = rec.buffer,
-        window = rec.window,
-        start_offset = start,
+        buffer = d.buffer,
+        window = d.window,
+        start_offset = after,
         text = "",
         expected_revision = rev,
       }
     end
-    return true
   end
-
-  -- Claimed only if an expansion actually happened. Otherwise `ch` is
-  -- an ordinary character in a Lean buffer and auto-pairing should see
-  -- it — `\zz` leaves `z` free to pair if it ever were a pair char.
-  return after ~= nil
 end
 
 -- Q#KR11's seam: a detached frontend's pending state must not outlive
@@ -343,8 +444,11 @@ end
 -- life of the session.
 pmacs.hook.add("frontend.detached", function(fid)
   pending[fid] = nil
+  deferred[fid] = nil
 end)
 
+pmacs.hook.add("buffer.after-edit", run_deferred)
+
 -- `buffer.after-switch` fires with NO arguments, so it cannot say whose
 -- switch it was. The acting frontend is the one that produced the most
 -- recent dispatched input event, which is what `pmacs.frontend.id()`
diff --git a/docs/active-work.md b/docs/active-work.md
index 034b1fd..f931da1 100644
--- a/docs/active-work.md
+++ b/docs/active-work.md
@@ -175,7 +175,8 @@ If it does not, stop and repair the remote/fetch configuration.
 
 ### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`)
 
-- Framing `docs/lean4-mode-framing.md` **revision 9**, approved. Stage
+- Framing `docs/lean4-mode-framing.md` **revision 10** (round 10 =
+  review of the implementation). Stage
   4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b,
   the Lean content that registers on it.
 - Footprint: `scripts/regen-lean-abbrev` (new, the generator),
@@ -183,7 +184,7 @@ If it does not, stop and repair the remote/fetch configuration.
   from `leanprover/vscode-lean4@17d1d08`, Apache-2.0),
   `builtin/runtime/lean_input.lua` (new, the consumer at priority 50),
   `src/editor.rs` (two `include_str!` blocks),
-  `tests/lean_input_acceptance.rs` (new, 25 tests), and one
+  `tests/lean_input_acceptance.rs` (new, 29 tests), and one
   `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs`
   (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart
   from the load sites and that one test.
@@ -239,11 +240,31 @@ If it does not, stop and repair the remote/fetch configuration.
   | `buffer.after-switch` clears every frontend | 1 |
   | delete the `buffer.after-switch` subscriber | 1 |
   | `frontend.detached` purges every frontend | 1 |
+  | claim the terminator | 1 |
+  | expand inside the chain, then decline | 2 |
+  | drop the `cursor() == post_cursor` check | 1 |
+  | place the point without the context guard | 1 |
+  | load lean_input.lua after lsp.lua | 1 |
 
   Acceptance 45f bit by construction: without a registered window for
   the source frontend it ran six fan-outs with a nil record and proved
   nothing, because `handle_remote_crdt_op` arms nothing unless the
   source's active window displays the buffer.
+- **Round 10 (review) found three defects, all about what happens
+  AROUND the expansion rather than about resolving an abbreviation.** A
+  pair character that TERMINATES an abbreviation never reached pairing
+  (`\alp(` gave `α(`): the first revision claimed the terminator, and
+  merely declining is not enough either, because the chain hands each
+  consumer a copy of the record made before any consumer ran — so
+  expanding inside the chain invalidates pairing's copy and the closer
+  is lost anyway (verified by mutation, not assumed). The expansion now
+  runs on **its own `buffer.after-edit` subscriber** after the chain,
+  with a span that stops before the terminator. That is a new instance
+  of Q#AP7, so it is now pinned with the sighelp fake server.
+  Post-insert point motion was also mistaken for a valid span (the
+  relevance check needs `cursor() == post_cursor`, as pairing's has
+  since #110), and cursor placement could move a buffer an intercept
+  had switched to.
 - Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED,
   named in the module header (Q#LN21): six source-peer optimistic
   inserts replaced by one daemon-peer op. `set_round_trip_input` would
diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md
index 32b1a10..d1dc46b 100644
--- a/docs/agent-handoff.md
+++ b/docs/agent-handoff.md
@@ -132,7 +132,14 @@ commands, read `docs/active-work.md` immediately after this file.
     (branch `lean4-stage4b-input-method`, framing rev 9): a vendored
     1,855-entry table generated from `leanprover/vscode-lean4@17d1d08`
     by `scripts/regen-lean-abbrev`, plus a consumer registered on the
-    Stage 4a chain at priority 50, ahead of pairing. Its durable facts:
+    Stage 4a chain at priority 50, ahead of pairing. **A consumer
+    cannot both edit and let a later consumer act on the same
+    keystroke**: the chain hands each consumer a copy of the record made
+    before any consumer ran, so an edit invalidates every copy still to
+    be used. The expansion therefore runs on a SECOND
+    `buffer.after-edit` subscriber after the chain — which is how a
+    pair character that terminates an abbreviation still pairs
+    (`\alp(` → `α()`). Its other durable facts:
     the table must stay an ORDERED SEQUENCE (equal-length ties resolve
     by source declaration order, which a `pairs`-iterated map cannot
     express); a generator round-trip check must re-read the BYTES ON
diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md
index 72a83fd..482ad84 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. Current revision: **9**.
+Revision 1 — initial. Current revision: **10**.
 
 ### Round 1 (rev 1 → rev 2)
 
@@ -535,6 +535,38 @@ The mechanism (Q#LN11, Q#LN21, Q#LN22) needed no change — these were
 errors in the examples chosen to pin it, which is why a simulation over
 the real data found them and four review rounds over the prose did not.
 
+### Round 10 (rev 9 → rev 10)
+
+Review of the Stage 4b implementation. Three defects in the expander,
+all of them about what happens AROUND the expansion rather than about
+resolving an abbreviation, plus one stale count.
+
+1. **A pair character that terminates an abbreviation never reached
+   auto-pairing.** Q#LN22 already said the terminator is not claimed;
+   the implementation claimed it whenever an expansion succeeded, so
+   `\alp(` gave `α(`. Not claiming is necessary and not sufficient —
+   the chain hands each consumer a copy of the record made before any
+   consumer ran, so expanding inside the chain invalidates the copy
+   pairing is holding and the closer is lost anyway. Q#LN22 now
+   specifies the deferred subscriber and the span that stops before the
+   terminator; acceptance 45j pins all three failure modes.
+2. **Post-insert point motion was mistaken for a valid pending span.**
+   The relevance check compared buffer and window but not
+   `ed.cursor() == rec.post_cursor`, so a redefined self-insert that
+   inserts and then moves the point still expanded — and teleported the
+   point back. Pairing has made this three-part check since #110.
+   Acceptance 45k.
+3. **Cursor placement could move the wrong buffer.** A buffer intercept
+   may switch buffers during `buf:replace`; the unguarded `goto_byte`
+   afterwards moved the switched-to buffer's point. `repair_cursor` is
+   the precedent. Acceptance 45l.
+4. **The coherence census contradicted itself** — nine settings in one
+   paragraph, eight three paragraphs below.
+
+Acceptance 45m was added with them: the expansion now runs on its own
+`buffer.after-edit` subscriber, which is a new instance of Q#AP7 and
+was unpinned.
+
 ## 1. What ships
 
 Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The
@@ -1718,8 +1750,9 @@ reconstruction of it:
 - 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`.
+- If no key extends `text .. c`, `c` TERMINATES the abbreviation: the
+  chain does *not* claim it, and the expansion of `text` is
+  **deferred** until after the chain has run (round 10; see below).
 - **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
@@ -1733,6 +1766,37 @@ reconstruction of it:
   broken by source rank, unmatchable tail appended (`\alp7` → `α7`).
 - `$CURSOR` is stripped from the symbol and its index becomes the point.
 
+**The expansion is deferred past the chain, and its span stops before
+the terminator** (round 10). "Not claiming the terminator" is necessary
+and not sufficient: a pair character is a legal terminator (`\alp(` must
+give `α()`), and the chain hands every consumer a *copy* of the record
+made before any consumer ran. So expanding inside the chain and then
+declining leaves auto-pairing holding offsets the replace has already
+invalidated — pairing declines and the closer is silently lost, which a
+probe confirmed. Claiming the terminator instead suppresses pairing
+outright. Neither is recoverable from inside the chain.
+
+The expander therefore records the pending expansion and performs it on
+its **own `buffer.after-edit` subscriber**, registered after
+typed_edit.lua's and before lsp.lua's. A claim by any consumer stops the
+chain but not a separate subscriber — which is the point, since pairing
+claims the terminator it reacts to. The replaced span covers the leader
+and the typed text only; whatever pairing did lands after it and
+survives untouched. One undo restores the same text either way, because
+the terminator was always its own insert.
+
+Two guards this exposes, both of which pairing already carries:
+
+- The relevance check is **three-part**, not two: buffer, window, **and
+  `ed.cursor() == rec.post_cursor`**. A redefined self-insert can insert
+  the completing character and then move the point, and expanding over a
+  span the user has left teleports them back into it.
+- Cursor placement after the replace is **context-guarded**. A buffer
+  intercept may switch window or buffer while `buf:replace` runs; an
+  unguarded `goto_byte` then moves the point of a buffer that has
+  nothing to do with the expansion. `pair.lua`'s `repair_cursor` is the
+  precedent.
+
 **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
@@ -2490,11 +2554,14 @@ criterion 46 requires to stay byte-identical.
     it assumed `\alpha` takes the finish path when `alpha` is in the
     1,550-key eager set (round 9; see 41).
     - *Finish path.* `\alp` + space yields `α `: the space lands first
-      and the expansion runs in the following `buffer.after-edit`, so
-      the terminator is **retained**, not consumed, and it is inside the
-      replaced span. One undo restores `\alp ` — with its space, not
-      `\al`. Rev 6 wrote the post-undo text without the terminator,
-      which would be true only if the terminator were swallowed.
+      and the expansion runs later in the same `buffer.after-edit`
+      fan-out, so the terminator is **retained**, not consumed. It sits
+      OUTSIDE the replaced span, which covers only the leader and the
+      typed text (round 10) — the observable text and the post-undo
+      text are the same either way, because the terminator was its own
+      insert. One undo restores `\alp ` — with its space, not `\al`.
+      Rev 6 wrote the post-undo text without the terminator, which
+      would be true only if the terminator were swallowed.
     - *Eager path.* `\alpha` yields `α` with no terminator typed, and a
       following space is a **separate** edit. One undo removes the
       space; a second restores `\alpha`. Asserting the finish-path undo
@@ -2598,6 +2665,33 @@ criterion 46 requires to stay byte-identical.
       `$CURSOR` more than once;
     - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`,
       `n`, `setminus`, and the tie cases from 45h.
+45j. **A pair character that TERMINATES an abbreviation still pairs**
+    (round 10). `\alp(` yields `α()` with the point between the pair.
+    Bites three ways, all of which produce different wrong answers:
+    claiming the terminator gives `α(`; expanding inside the chain and
+    then declining also gives `α(`, because the replace invalidates the
+    record copy pairing is holding; and pairing running first gives
+    `\alp()` unexpanded. Criterion 40 is the same collision from the
+    other side, and passing it says nothing about this one.
+45k. **The relevance check is three-part.** A redefined
+    `buffer.self-insert` that inserts the completing character and then
+    moves the point must not expand: `\alph` + `a` under such an
+    override leaves literal `\alpha` with the point where the command
+    put it. Bites against checking only buffer and window — the
+    expansion would otherwise teleport the point back into a span the
+    user has left.
+45l. **Cursor placement is context-guarded.** A buffer intercept that
+    switches buffers during `buf:replace` must not have the
+    switched-to buffer's point moved. Bites against an unguarded
+    `goto_byte`, which translates the LEAN buffer's pre-edit point
+    through the LEAN buffer's edit and applies it to whatever is
+    ambient.
+45m. **Q#AP7 for the deferred subscriber.** The expansion runs on a
+    second `buffer.after-edit` subscriber, so it inherits pairing's
+    flush-ordering obligation: no `didChange` may ever carry the
+    unexpanded text. Pinned with the `sighelp` fake server and `(` as
+    the trigger — the flush carrying the terminator carries `α()`.
+    Falsified by loading lean_input.lua after lsp.lua.
 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.
@@ -2752,7 +2846,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from
 languages other than Lean, and §4's rule is what keeps them out of a Lean
 PR.
 
-### 9.1 Coherence impact — stages 4a and 4b (rev 9)
+### 9.1 Coherence impact — stages 4a and 4b (rev 10)
 
 **Sections served.** §6 (interaction islands) primarily, and in the
 *preventing* direction rather than the fixing one — see below. §11
diff --git a/tests/lean_input_acceptance.rs b/tests/lean_input_acceptance.rs
index 01ee89e..9270f1b 100644
--- a/tests/lean_input_acceptance.rs
+++ b/tests/lean_input_acceptance.rs
@@ -8,10 +8,12 @@
 
 use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
 use pmacs::editor::EditorState;
+use pmacs::lua_bindings::StateDir;
 use pmacs::protocol::FrontendId;
 use pmacs::window::{FrontendView, Layout, Window, WindowId};
 use std::path::PathBuf;
 use std::sync::atomic::{AtomicUsize, Ordering};
+use std::time::{Duration, Instant};
 
 fn fresh_dir() -> PathBuf {
     static SEQ: AtomicUsize = AtomicUsize::new(0);
@@ -49,6 +51,10 @@ fn text(s: &EditorState) -> String {
     String::from_utf8_lossy(&b.as_bytes()).into_owned()
 }
 
+fn cursor(s: &EditorState) -> i64 {
+    eval(s, "return pmacs.editor.cursor()")
+}
+
 fn type_as(s: &mut EditorState, fid: FrontendId, chars: &str) {
     for ch in chars.chars() {
         s.dispatch_key(fid, key(KeyCode::Char(ch)));
@@ -176,6 +182,33 @@ fn a_pending_abbreviation_is_never_corrupted_by_auto_pairing() {
     assert_eq!(text(&s), "⟦⟧", "the full key resolves");
 }
 
+#[test]
+fn a_pair_character_that_terminates_an_abbreviation_still_pairs() {
+    // The other half of the collision, and the one the first revision
+    // of this file got wrong. `(` does not extend `alp`, so it
+    // TERMINATES — and a terminator is an ordinary character that
+    // pairing is entitled to react to.
+    //
+    // Claiming the terminator suppresses pairing entirely (`α(`).
+    // Expanding before declining is no better: the replace makes
+    // pairing's copy of the record stale, so pairing declines and the
+    // closer is silently lost. Only deferring the expansion past the
+    // chain gives both.
+    let (mut s, _f) = lean_editor();
+    type_str(&mut s, "\\alp(");
+    assert_eq!(
+        text(&s),
+        "α()",
+        "the abbreviation expanded AND the terminator paired"
+    );
+    assert_eq!(
+        cursor(&s),
+        3,
+        "and the point sits between the pair — after α (2 bytes) and \
+         the opener"
+    );
+}
+
 #[test]
 fn a_pair_character_outside_a_pending_abbreviation_still_pairs() {
     // The other direction: claiming extensions must not disable pairing
@@ -271,6 +304,93 @@ fn switching_buffers_clears_pending_state_eagerly() {
     );
 }
 
+#[test]
+fn a_self_insert_that_moves_the_point_afterwards_does_not_expand() {
+    // Buffer and window matching is not enough. A redefined
+    // `buffer.self-insert` may insert the completing character and THEN
+    // move the point; expanding over a span the user has left teleports
+    // them back into it. Pairing makes the same three-part check
+    // (`ed.cursor() ~= rec.post_cursor`) for the same reason.
+    let (mut s, _f) = lean_editor();
+    type_str(&mut s, "\\alph");
+    exec(
+        &s,
+        r#"
+        pmacs.command.unregister("buffer.self-insert")
+        pmacs.command.define {
+          name = "buffer.self-insert",
+          description = "test override: insert, then move the point away",
+          fn = function(cp)
+            pmacs.editor.insert_char_over_region(cp)
+            pmacs.editor.goto_byte(0)
+          end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "a");
+    assert_eq!(
+        text(&s),
+        "\\alpha",
+        "the record died with the point that left it — no expansion"
+    );
+    assert_eq!(cursor(&s), 0, "and the point stayed where it was moved to");
+}
+
+#[test]
+fn an_intercept_that_switches_buffers_does_not_move_the_other_points() {
+    // A buffer intercept may switch window or buffer while the replace
+    // runs. An unguarded `goto_byte` afterwards moves the point of
+    // whatever it switched TO — a buffer with nothing to do with this
+    // expansion. Pairing's `repair_cursor` guards the same way.
+    let (mut s, f) = lean_editor();
+    let dir = fresh_dir();
+    let other = dir.join("other.lean");
+    std::fs::write(&other, "0123456789").unwrap();
+    let od = other.display().to_string();
+    let fd = f.display().to_string();
+
+    exec(&s, &format!("pmacs.buffer.find_or_open({od:?})"));
+    exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})"));
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    exec(
+        &s,
+        &format!(
+            r#"
+            _G.SWITCHED = false
+            pmacs.buffer.add_intercept(pmacs.window.buffer(), function(op)
+              if op.kind == "replace" and not _G.SWITCHED then
+                _G.SWITCHED = true
+                pmacs.buffer.find_or_open({od:?})
+              end
+              return nil
+            end)
+            "#
+        ),
+    );
+
+    type_str(&mut s, "\\alpha");
+    let switched: bool = eval(&s, "return _G.SWITCHED");
+    assert!(switched, "the intercept must actually have fired");
+    assert_eq!(
+        text(&s),
+        "0123456789",
+        "we are now in the buffer the intercept switched to"
+    );
+    // Whatever point the switch left in that buffer, the expansion must
+    // not have moved it. Unguarded, `goto_byte` runs against the
+    // ambient buffer and translates the LEAN buffer's pre-edit point
+    // (6) through the LEAN buffer's replace, landing at 2 here — a
+    // number with no meaning in this buffer at all.
+    assert_eq!(
+        cursor(&s),
+        0,
+        "its point is untouched — the expansion's cursor placement is \
+         guarded on the window and buffer still being the ones it \
+         edited"
+    );
+}
+
 // ---------------------------------------------------------------------------
 // 44 / 45 — the setting and the language gate, both on the SOURCE buffer
 // ---------------------------------------------------------------------------
@@ -566,6 +686,127 @@ fn the_vendored_table_is_self_consistent() {
     assert!(!to_eager, "`to` is extended by `top`, `to0`, `toa`, …");
 }
 
+// ---------------------------------------------------------------------------
+// Q#AP7 for the deferred expansion: it must land before lsp.lua flushes
+// ---------------------------------------------------------------------------
+
+#[test]
+fn the_expansion_reaches_the_first_did_change() {
+    // The expansion runs on its OWN `buffer.after-edit` subscriber,
+    // after the typed-edit chain. That makes it a new instance of the
+    // Q#AP7 obligation pairing already carries: lsp.lua's subscriber
+    // flushes `didChange` SYNCHRONOUSLY on the signature-trigger path,
+    // and `(` is a trigger. A server told about `\alp(` instead of
+    // `α()` stays wrong until the next edit — diagnostics, semantic
+    // tokens and inlay hints all frozen at stale byte positions.
+    //
+    // Falsified by loading lean_input.lua after lsp.lua in
+    // `src/editor.rs`: the expansion would then arrive in the SECOND
+    // didChange, or not at all.
+    let dir = fresh_dir();
+    let sink = dir.join("changes.jsonl");
+    let sink_disp = sink.display().to_string();
+    let fake = env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned();
+
+    let f = dir.join("a.lean");
+    std::fs::write(&f, "").unwrap();
+    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.lean4 = {{
+               command = '{fake}',
+               env = {{
+                 PMACS_FAKE_LSP_MODE = 'sighelp',
+                 PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}',
+               }},
+             }}"
+        ),
+    );
+
+    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, "\\alp(");
+    assert_eq!(text(&s), "α()", "precondition: the expansion happened");
+
+    // Wait for the flush that carries the `(` keystroke. Earlier
+    // keystrokes have already produced their own didChanges, so
+    // `changes[0]` is NOT the one under test — asserting on it compares
+    // against `\al` and fails for the wrong reason.
+    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.iter().any(|t| t.contains('α')) {
+            break c;
+        }
+        assert!(
+            Instant::now() < deadline,
+            "no didChange carrying the expansion reached the fake server;              got {:?}",
+            did_change_texts(&sink)
+        );
+        std::thread::sleep(Duration::from_millis(10));
+    };
+    assert!(
+        !changes.iter().any(|t| t == "\\alp("),
+        "no didChange may ever carry the UNEXPANDED text — one would          mean lsp.lua flushed before the deferred expansion ran (Q#AP7).          Got {changes:?}"
+    );
+    assert_eq!(
+        changes.last().map(String::as_str),
+        Some("α()"),
+        "the flush that carries the terminator carries the expansion          and pairing's closer with it"
+    );
+}
+
+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()
+}
+
 // ---------------------------------------------------------------------------
 // 45i — pending state is per frontend
 // ---------------------------------------------------------------------------