fix(lean4): count fan-outs where a claim cannot skip the count

Round 11 put the nesting count in the expander, which is optional. A
consumer at a lower priority can CLAIM and stop the chain before the
expander runs, while that fan-out's deferred-expansion subscriber still
runs — so the nested pass went uncounted, looked like the outermost
one, expanded early, and outer pairing resumed with a record the
replace had invalidated. `\alp(` gave `α(` again.

The count now comes from a no-op consumer registered at the minimum
priority, which runs first in every chain invocation that reaches any
consumer at all. Its guarantee is exactly the ordering contract the
chain already rests on, and it degrades safely: the only thing that can
skip it is a claim ahead of it, which skips the expander too, so
nothing is queued in that fan-out either.

The other plausible home does not work and the comment now says why: a
subscriber registered beside `run_deferred` is too late, because the
whole nested fan-out completes inside the OUTER chain's subscriber,
before either of them runs.

Acceptance 45o pins the short-circuit path — a consumer at 25 that
claims when the record is nil, so the nested pass never reaches the
expander. 45n passes against this bug, which is why both exist.
Counting in the expander fails 45o and nothing else.

Framing rev 12 also names the shape rounds 10–12 share: each fix was
correct about the failure it was shown and wrong about the boundary of
the mechanism it leaned on — the chain's copy semantics, then its
re-entrancy, then its short-circuit. A queue that outlives the thing
that filled it has to name that thing, not approximate it.

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

builtin/runtime/lean_input.lua

@@ -229,7 +229,7 @@ end
 -- The consumer
 -- ---------------------------------------------------------------------
 
--- Chain-consumer invocations not yet matched by a `run_deferred`.
+-- Chain invocations not yet matched by a `run_deferred`.
 --
 -- `buffer.after-edit` fan-outs NEST: the typed-edit contract explicitly
 -- supports a consumer calling `pmacs.hook.run("buffer.after-edit")`,
@@ -240,15 +240,29 @@ end
 -- bug deferring exists to fix: pairing resumes afterwards holding a
 -- record the replace has invalidated, declines, and the closer is lost.
 --
--- The chain's subscriber and this module's subscriber run exactly once
--- each per fan-out, in that order, so counting invocations of the first
--- and matching them off in the second identifies the nesting level
--- without any new seam in typed_edit.lua. Only the outermost pass
--- performs the expansion; a nested one leaves it queued.
+-- Counting has to happen INSIDE the chain and BEFORE any consumer that
+-- might start a nested fan-out. A subscriber registered alongside
+-- `run_deferred` is too late — the whole nested fan-out completes
+-- inside the outer chain's subscriber, before either of them runs. And
+-- counting in the expander itself is not enough: a lower-priority
+-- consumer may CLAIM and stop the chain before the expander is
+-- reached, so a nested pass would go uncounted while its
+-- `run_deferred` still ran (round 11's fix, round 12's defect).
+--
+-- Hence a separate no-op consumer at the minimum priority, which runs
+-- first in every chain invocation that reaches any consumer at all.
+-- Its guarantee is exactly the ordering contract the chain already
+-- rests on, and it degrades safely: the only thing that can skip it is
+-- a claim ahead of it, which skips the expander too, so nothing is
+-- queued in that fan-out either.
 local depth = 0
 
-local function on_typed_edit(rec)
+local function count_fan_out()
   depth = depth + 1
+  return false
+end
+
+local function on_typed_edit(rec)
   local fid = frontend_id()
   if fid == nil then return false end
 
@@ -426,8 +440,8 @@ local function run_deferred()
   -- Match off this fan-out's chain invocation. `> 1` means the outer
   -- chain is still mid-list — pairing has not had the terminator yet —
   -- so the queued expansion stays queued for the outer pass. The clamp
-  -- keeps this honest if a lower-priority consumer claimed before the
-  -- chain reached ours, in which case there is nothing queued anyway.
+  -- keeps this honest if a claim beat the counting consumer, in which
+  -- case nothing was queued in that fan-out either.
   local level = depth
   if depth > 0 then depth = depth - 1 end
   if level > 1 then return end
@@ -487,6 +501,15 @@ pmacs.hook.add("buffer.after-switch", function()
   if fid ~= nil then pending[fid] = nil end
 end)
 
+-- Runs first in every chain invocation that reaches a consumer at all,
+-- which is what makes the nesting count trustworthy — see `depth`. It
+-- declines, always: it observes, it does not participate.
+pmacs.typed_edit.add_consumer {
+  name = "lean-abbrev-fan-out-counter",
+  priority = -2147483648,
+  fn = count_fan_out,
+}
+
 pmacs.typed_edit.add_consumer {
   name = "lean-abbrev",
   priority = 50,

docs/active-work.md

@@ -175,8 +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 11** (rounds 10 and
-  11 = review of the implementation). Stage
+- Framing `docs/lean4-mode-framing.md` **revision 12** (rounds 10, 11
+  and 12 = 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),
@@ -184,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, 30 tests), and one
+  `tests/lean_input_acceptance.rs` (new, 31 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.
@@ -247,6 +247,7 @@ If it does not, stop and repair the remote/fetch configuration.
   | load lean_input.lua after lsp.lua | 1 |
   | let a nested fan-out consume the deferred slot | 1 |
   | stop counting chain invocations | 1 |
+  | count fan-outs in the expander instead of the sentinel | 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
@@ -278,6 +279,23 @@ If it does not, stop and repair the remote/fetch configuration.
   subscriber and the expander's each run exactly once per fan-out, so
   counting the first and matching it off in the second identifies the
   nesting level with no new seam in merged Stage 4a substrate.
+- **Round 12 found round 11's counter in the wrong place.** It counted
+  invocations of the EXPANDER, which is optional: a lower-priority
+  consumer can claim and stop the chain before the expander runs, while
+  that fan-out's deferred subscriber still runs — so the nested pass
+  went uncounted, looked outermost, expanded early, and outer pairing
+  resumed with an invalidated record. The count now comes from a no-op
+  consumer at the MINIMUM priority, which runs first in every chain
+  invocation that reaches any consumer, and degrades safely: the only
+  thing that can skip it is a claim ahead of it, which skips the
+  expander too. A subscriber registered beside `run_deferred` cannot
+  serve — the whole nested fan-out completes inside the outer chain's
+  subscriber, before it would run.
+- **Rounds 10–12 share a shape worth naming.** Each fix was correct
+  about the failure it was shown and wrong about the boundary of the
+  mechanism it leaned on — first the chain's copy semantics, then its
+  re-entrancy, then its short-circuit. **A queue that outlives the
+  thing that filled it has to name that thing, not approximate it.**
 - 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

docs/agent-handoff.md

@@ -143,7 +143,11 @@ commands, read `docs/active-work.md` immediately after this file.
     owning which fan-out it belongs to**: these fan-outs NEST, so a
     consumer between the expander and pairing that calls
     `pmacs.hook.run` re-enters the deferred subscriber while the outer
-    chain is still mid-list. Its other durable facts:
+    chain is still mid-list, and the count that recognises this has to
+    come from a MINIMUM-PRIORITY consumer — the expander is optional
+    (a claim can stop the chain first) and a subscriber beside the
+    deferred one is too late (the nested fan-out finishes inside the
+    outer chain's subscriber). 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

docs/lean4-mode-framing.md

@@ -46,7 +46,7 @@ during a rebase.
 
 ## 0.1 Revision history
 
-Revision 1 — initial. Current revision: **11**.
+Revision 1 — initial. Current revision: **12**.
 
 ### Round 1 (rev 1 → rev 2)
 
@@ -587,6 +587,26 @@ One P1 in the round-10 fix, and one stale comment.
    which round 10 deliberately stopped doing. The behaviour it asserts
    was correct; only the explanation was stale.
 
+### Round 12 (rev 11 → rev 12)
+
+One P1: round 11's counter was in the wrong place.
+
+1. **The nesting count lived in the expander, which is optional.** A
+   consumer at a lower priority can claim and stop the chain before the
+   expander runs, while that fan-out's deferred-expansion subscriber
+   still runs — so the nested pass went uncounted, looked like the
+   outermost one, expanded early, and outer pairing resumed with an
+   invalidated record. `\alp(` gave `α(` again. The count now comes
+   from a no-op consumer at the minimum priority, which runs first in
+   every chain invocation that reaches any consumer; acceptance 45o
+   pins the short-circuit path that 45n does not reach.
+
+The pattern across rounds 10–12 is worth naming: each fix was correct
+about the failure it was shown and wrong about the boundary of the
+mechanism it relied on — the chain's copy semantics, then its
+re-entrancy, then its short-circuit. **A queue that outlives the thing
+that filled it needs to name that thing, not approximate it.**
+
 ## 1. What ships
 
 Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The
@@ -1815,11 +1835,27 @@ performed the expansion would reproduce the exact bug deferring exists
 to fix, reached through the chain's documented re-entrancy seam instead
 of through claiming.
 
-The chain's subscriber and the expander's subscriber each run exactly
-once per fan-out, in that order, so counting invocations of the first
-and matching them off in the second identifies the nesting level — no
-new seam in typed_edit.lua, which is merged substrate. Only the
-outermost pass expands; a nested one leaves the expansion queued.
+The nesting level is counted by a **no-op consumer registered at the
+minimum priority**, matched off in the expander's subscriber. Only the
+outermost pass expands; a nested one leaves the expansion queued. No
+new seam in typed_edit.lua, which is merged substrate.
+
+Where the count lives is the whole difficulty, and two plausible places
+are both wrong (round 12):
+
+- **A subscriber registered beside the expander's is too late.** The
+  entire nested fan-out completes inside the OUTER chain's subscriber,
+  before any subscriber registered after it runs.
+- **The expander itself is optional.** A lower-priority consumer may
+  claim and stop the chain before the expander is reached, so a nested
+  pass would go uncounted while its `run_deferred` still ran — and
+  would then look like the outermost one.
+
+A minimum-priority consumer runs first in every chain invocation that
+reaches any consumer at all. Its guarantee is exactly the ordering
+contract the chain already rests on, and it degrades safely: the only
+thing that can skip it is a claim ahead of it, which skips the expander
+too, so nothing is queued in that fan-out either.
 
 Two guards this exposes, both of which pairing already carries:
 
@@ -2736,6 +2772,14 @@ criterion 46 requires to stay byte-identical.
     outer chain would then hand pairing a record the replace had
     invalidated — the round-10 failure again, through the chain's
     documented re-entrancy seam rather than through claiming.
+45o. **A nested fan-out that never reaches the expander must not
+    expand early either** (round 12). Same shape as 45n, but the nested
+    pass is short-circuited by a consumer at priority 25 that claims
+    when the record is nil — so the expander never runs on it. Bites
+    against counting fan-outs in the expander, which is optional by
+    construction: the uncounted nested pass looks outermost, expands,
+    and outer pairing resumes with an invalidated record. 45n passes
+    against that bug, which is why both are pinned.
 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.
@@ -2890,7 +2934,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 11)
+### 9.1 Coherence impact — stages 4a and 4b (rev 12)
 
 **Sections served.** §6 (interaction islands) primarily, and in the
 *preventing* direction rather than the fixing one — see below. §11

tests/lean_input_acceptance.rs

@@ -251,6 +251,65 @@ fn a_nested_fan_out_between_the_expander_and_pairing_does_not_expand_early() {
     );
 }
 
+#[test]
+fn a_nested_fan_out_that_never_reaches_the_expander_still_does_not_expand_early() {
+    // The chain's OTHER exit: a consumer may CLAIM and stop the chain
+    // before the expander is reached, while the fan-out's
+    // deferred-expansion subscriber still runs. Counting in the
+    // expander itself therefore misses that pass — it would look like
+    // the outermost one and expand early, and outer pairing would
+    // resume with an invalidated record.
+    //
+    // The sequence, exactly: a consumer at 25 declines on the outer
+    // pass (there is a record) and claims on the nested one (there is
+    // not); a consumer at 75 runs one nested fan-out from between the
+    // expander and pairing.
+    let (mut s, _f) = lean_editor();
+    exec(
+        &s,
+        r#"
+        _G.NESTED, _G.CLAIMED = 0, 0
+        pmacs.typed_edit.add_consumer {
+          name = "claims-only-when-recordless",
+          priority = 25,   -- ahead of the expander at 50
+          fn = function(rec)
+            if rec == nil then
+              _G.CLAIMED = _G.CLAIMED + 1
+              return true   -- stops the chain: the expander never runs
+            end
+            return false
+          end,
+        }
+        pmacs.typed_edit.add_consumer {
+          name = "nested-fan-out",
+          priority = 75,   -- between the expander (50) and pairing (100)
+          fn = function()
+            if _G.NESTED == 0 then
+              _G.NESTED = 1
+              pmacs.hook.run("buffer.after-edit")
+            end
+            return false
+          end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "\\alp(");
+    let (nested, claimed): (i64, i64) = eval(&s, "return _G.NESTED, _G.CLAIMED");
+    assert_eq!(nested, 1, "the nested fan-out must actually have run");
+    assert!(
+        claimed >= 1,
+        "the nested pass must actually have been short-circuited before \
+         the expander, or this pins the same thing as 45n"
+    );
+    assert_eq!(
+        text(&s),
+        "α()",
+        "the nesting count comes from a point that runs before any \
+         consumer can claim, so the nested pass was still recognised"
+    );
+}
+
 #[test]
 fn a_pair_character_outside_a_pending_abbreviation_still_pairs() {
     // The other direction: claiming extensions must not disable pairing