diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua
index 546e123..6490296 100644
--- a/builtin/runtime/lean.lua
+++ b/builtin/runtime/lean.lua
@@ -133,6 +133,12 @@ local probe = {
                      -- version verdict still has to retire it
   armed = false,     -- the target buffer + primary have been captured
   repaired = {},     -- buffer key -> repair attempted (at most once)
+  repair_attempts = 0, -- COUNT of attach attempts, not distinct buffers:
+                     -- table cardinality cannot tell "once per buffer"
+                     -- from "every tick for one buffer"
+  fallback_installed = false,
+  fallback_watch = nil, -- fallback sid being polled for die-before-init
+  fallback_failed = false,
   saw_initialized = false,
 }
 
@@ -280,12 +286,21 @@ end
 -- Retiring only the server that happened to fail left the others live
 -- and every buffer attached to them stranded on a command the config no
 -- longer names.
-local function retire_all_lean_servers()
+-- Only servers this module's config produced. `ensure_server` labels
+-- every auto-attached server `default-<language>`, so that label is the
+-- derivation discriminator: a server the USER spawned from `init.lua`
+-- carries their own label, is not derived from `pmacs.lsp.config.lean4`,
+-- and must not be stopped because our config changed. Selecting on
+-- `language_id` alone swept those up too — a destructive side effect on
+-- state this module does not own.
+local DERIVED_LABEL = "default-lean4"
+
+local function retire_derived_lean_servers()
   local ok, rows = pcall(pmacs.lsp.list)
   if not ok or not rows then return end
   local ids = {}
   for _, info in ipairs(rows) do
-    if info.language_id == "lean4" then ids[#ids + 1] = info.id end
+    if info.label == DERIVED_LABEL then ids[#ids + 1] = info.id end
   end
   for _, id in ipairs(ids) do retire_server(id) end
 end
@@ -308,7 +323,14 @@ end
 -- on a no-op. Skipping leaves the attempt for a later tick, once the
 -- retirement has actually landed.
 local function repair_active_if_stale()
-  if not probe.latched then return end
+  -- **`fallback_installed`, not `latched`.** When the swap does not
+  -- happen — the config already names the fallback, or it vanished
+  -- before an asynchronous verdict landed — `fire_latch` returns early
+  -- but `latched` stays true. Gating repair on `latched` then retried
+  -- the UNCHANGED configuration and reported the result as a fallback
+  -- failure, which is both a second pointless spawn and a misleading
+  -- message. Repair exists to apply a swap; no swap, nothing to apply.
+  if not probe.fallback_installed then return end
   local buf = pmacs.window.buffer()
   if not buf then return end
   local key = tostring(buf)
@@ -327,10 +349,42 @@ local function repair_active_if_stale()
   if not stale then return end
 
   probe.repaired[key] = true
+  probe.repair_attempts = probe.repair_attempts + 1
   local ok, fresh = pcall(pmacs.lsp._attach_buffer)
   if not ok or not fresh then
     report("LSP: lean4 fallback " .. fallback_name()
       .. " did not start either")
+    return
+  end
+  -- **A successful SPAWN is not a successful START.** The once-per-
+  -- buffer bound stops `_attach_buffer` being called again, but it says
+  -- nothing about the server it produced: `ensure_server` never forwards
+  -- `cfg.restart`, so the fallback inherits `OnCrash`, and an executable
+  -- that dies before `initialize` is respawned by the manager forever
+  -- with no attempt ceiling — silently, because `latched` has already
+  -- disabled the primary's failure poll. Watch this one too, once.
+  if not probe.fallback_watch and not probe.fallback_failed then
+    probe.fallback_watch = fresh.server
+  end
+end
+
+-- The fallback's own die-before-initialize poll. One shot: on failure it
+-- retires the server (which is what actually ends the respawn loop) and
+-- reports, and never re-arms.
+local function poll_fallback()
+  local sid = probe.fallback_watch
+  if not sid then return end
+  local kind = server_state_kind(sid)
+  if kind == "initialized" then
+    probe.fallback_watch = nil
+    return
+  end
+  if kind == nil or kind == "crashed" or kind == "stopped" then
+    probe.fallback_watch = nil
+    probe.fallback_failed = true
+    if kind ~= nil then retire_server(sid) end
+    report("LSP: lean4 fallback " .. fallback_name()
+      .. " started but did not stay up")
   end
 end
 
@@ -343,10 +397,11 @@ local function fire_latch(sid, why)
     -- Still retire: the servers are broken whether or not a replacement
     -- command was installed, and leaving them live would keep the
     -- restart machinery running against a command known to fail.
-    retire_all_lean_servers()
+    retire_derived_lean_servers()
     return
   end
-  retire_all_lean_servers()
+  retire_derived_lean_servers()
+  probe.fallback_installed = true
   report("LSP: lean4 " .. why .. "; falling back to " .. fallback_name())
   -- Repair what is in front of the user now; everything else is
   -- repaired lazily as it becomes active (see `repair_active_if_stale`).
@@ -607,6 +662,7 @@ pmacs.hook.add("process.after-tick", function()
   -- Repair the active buffer if the latch invalidated it. Cheap when
   -- there is nothing to do, and bounded to one attempt per buffer.
   repair_active_if_stale()
+  poll_fallback()
 end)
 
 -- Test seam: acceptance drives the latch deterministically rather than
diff --git a/builtin/runtime/lsp.lua b/builtin/runtime/lsp.lua
index 0749cfa..6081a3d 100644
--- a/builtin/runtime/lsp.lua
+++ b/builtin/runtime/lsp.lua
@@ -871,6 +871,21 @@ local function attached_for_active()
   if not buf then return nil end
   local key = tostring(buf)
   local rec = attachments[key]
+  -- A record whose server is dead is worse than no record: every
+  -- command below issues requests against it and gets silence. Rebuild
+  -- instead, which is what `attach_buffer` does for a stale attachment
+  -- anyway — this just stops the dead record short-circuiting that.
+  --
+  -- Load-bearing for anything that retires a server out from under open
+  -- buffers (Arc 8 Stage 3b's fallback latch retires every Lean server
+  -- at once). Buffers in OTHER frontends get no `buffer.after-switch`
+  -- in this one, so an eager repair sweep keyed on the ambient active
+  -- buffer cannot reach them; healing at the point of USE is
+  -- frontend-agnostic, because whichever frontend runs the command is
+  -- the active one while it runs.
+  if rec and not server_is_live(rec.server) then
+    rec = nil
+  end
   if rec then
     -- Every interactive command resolves its attachment here before
     -- issuing requests; flushing now means the server answers those
@@ -942,6 +957,17 @@ function pmacs.lsp.attachment_for_request()
   local key = tostring(buf)
   local rec = attachments[key]
   if not rec then return nil end
+  -- Same liveness rule as `attached_for_active`: a record naming a dead
+  -- server is worse than none, because the caller issues a request
+  -- against it and waits for a reply that cannot come. Unlike that
+  -- function this one is deliberately non-attaching (it must not
+  -- perturb LSP state), so a dead record reads as "no attachment"
+  -- rather than triggering a rebuild.
+  if not server_is_live(rec.server) then
+    attachments[key] = nil
+    pending_did_change[key] = nil
+    return nil
+  end
   flush_did_change(key)
   return rec
 end
diff --git a/docs/active-work.md b/docs/active-work.md
index e4e1064..6b99985 100644
--- a/docs/active-work.md
+++ b/docs/active-work.md
@@ -265,7 +265,7 @@ If it does not, stop and repair the remote/fetch configuration.
 - Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in
   `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`,
   a `leanprogress` mode plus `waitForDiagnostics` validation on
-  `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (31 tests).
+  `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (36 tests).
   No protocol change.
 - **Stage 1's acceptance 12 is half superseded and was rewritten, not
   deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a
@@ -334,6 +334,31 @@ If it does not, stop and repair the remote/fetch configuration.
   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**.
 - **DURABLE LESSON — "the test that passes" vs "the test that
   discriminates."** Six tests across three rounds were written, run
   green, and only bite-testing showed they pinned nothing. **Carry this
@@ -359,6 +384,11 @@ If it does not, stop and repair the remote/fetch configuration.
   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.
   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
@@ -395,9 +425,9 @@ If it does not, stop and repair the remote/fetch configuration.
   server-failure latch covers the rest.
 - Verification on this branch: `cargo fmt --check` clean; strict
   workspace Clippy clean; 1,826 default + 2,003 CRDT library tests;
-  lean4 server 31/31; lean4 stage 1 9/9; dispatch seams 15/15;
+  lean4 server 36/36; lean4 stage 1 9/9; dispatch seams 15/15;
   multi-root 13/13; M4 121; required GPU 155; **isolated-config
-  workspace sweep 3,220 across 94 suites, zero failures**;
+  workspace sweep 3,225 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
diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs
index 32cdf3e..e28ac8f 100644
--- a/tests/lean4_server_acceptance.rs
+++ b/tests/lean4_server_acceptance.rs
@@ -1371,3 +1371,274 @@ fn r4_attribution_names_the_exact_command_and_its_arguments() {
          want substring: {expected}\n  saw: {status:?}"
     );
 }
+
+// ---------------------------------------------------------------------------
+// Round-5 review. All fail against 7c37bdc.
+// ---------------------------------------------------------------------------
+
+#[test]
+fn r5_a_fallback_that_dies_after_spawning_is_bounded_and_reported() {
+    // The once-per-buffer guard bounds calls to `_attach_buffer`, not
+    // the server it produced. `ensure_server` never forwards
+    // `cfg.restart`, so the fallback inherits `OnCrash` and a binary
+    // that exits before `initialize` is respawned forever — silently,
+    // because `latched` has already disabled the primary's poll. The
+    // prior failing-fallback test used a NONEXISTENT executable, which
+    // only exercises synchronous ENOENT.
+    use std::os::unix::fs::PermissionsExt as _;
+    let fx = Fixture::new();
+    fx.toolchain("pkg", "v4.9.0\n");
+    let file = fx.write("pkg/A.lean", "def a := 1\n");
+    let absent_primary = fx.dir("bin/no-such-lake");
+    let dying_fallback = fx.root.join("bin/dying-lean");
+    std::fs::create_dir_all(dying_fallback.parent().unwrap()).unwrap();
+    std::fs::write(&dying_fallback, "#!/bin/sh\nexit 4\n").unwrap();
+    std::fs::set_permissions(&dying_fallback, std::fs::Permissions::from_mode(0o755)).unwrap();
+
+    let mut state = editor(&fx);
+    exec(
+        &state,
+        &format!(
+            r#"
+            pmacs.lsp.config.lean4.command = "{}"
+            pmacs.lsp.config.lean4.args = {{ "serve" }}
+            pmacs.lean._fallback = {{ command = "{}", args = {{}} }}
+            "#,
+            lua_str(&absent_primary),
+            lua_str(&dying_fallback)
+        ),
+    );
+
+    open(&state, &file);
+    tick_for(&mut state, 1600);
+
+    // Nothing may be respawning: `attempt` counts spawns per server.
+    let worst_attempt: i64 = eval(
+        &state,
+        r"
+        local worst = 0
+        for _, s in ipairs(pmacs.lsp.list()) do
+          local a = s.attempt or 0
+          if a > worst then worst = a end
+        end
+        return worst
+        ",
+    );
+    assert!(
+        worst_attempt <= 1,
+        "a dying fallback must not be respawned indefinitely; saw \
+         attempt {worst_attempt}"
+    );
+    let status = state.core.borrow().status.clone();
+    assert!(
+        status.contains("did not stay up") || status.contains("did not start"),
+        "and the second failure is reported; saw {status:?}"
+    );
+}
+
+#[test]
+fn r5_a_user_spawned_lean_server_is_not_retired_by_the_fallback() {
+    // `retire_*` selected on `language_id == "lean4"`, which also names
+    // servers the user spawned themselves from `init.lua`. Those are not
+    // derived from `pmacs.lsp.config.lean4` and stopping them is a
+    // destructive side effect on state this module does not own.
+    let fx = Fixture::new();
+    fx.toolchain("pkg", "v4.9.0\n");
+    let file = fx.write("pkg/A.lean", "def a := 1\n");
+    let absent = fx.dir("bin/no-such-lake");
+    let mut state = editor(&fx);
+    with_fallback(&state, &absent);
+    exec(
+        &state,
+        &format!(
+            r#"
+            _G.mine = pmacs.lsp.spawn({{
+              label = "my-own-lean",
+              language_id = "lean4",
+              command = "{}",
+              args = {{}},
+            }})
+            "#,
+            fake_lsp_path()
+        ),
+    );
+    settle(&mut state);
+
+    open(&state, &file);
+    tick_for(&mut state, 600);
+
+    let mine_alive: bool = eval(
+        &state,
+        r#"
+        for _, s in ipairs(pmacs.lsp.list()) do
+          if tostring(s.id) == tostring(_G.mine) then
+            local k = s.state and s.state.kind
+            return k ~= "stopped" and k ~= "crashed"
+          end
+        end
+        return false
+        "#,
+    );
+    assert!(
+        mine_alive,
+        "a user-spawned Lean server survives a config-driven fallback — \
+         it was never derived from that config"
+    );
+}
+
+#[test]
+fn r5_no_swap_means_no_repair_attempts() {
+    // When the config already names the fallback, `swap_to_fallback`
+    // returns false and `fire_latch` returns early — but `latched` is
+    // true, so a repair gated on `latched` retried the UNCHANGED
+    // configuration and reported it as a fallback failure.
+    let fx = Fixture::new();
+    fx.toolchain("pkg", "v4.9.0\n");
+    let file = fx.write("pkg/A.lean", "def a := 1\n");
+    let absent = fx.dir("bin/no-such-lean");
+    let mut state = editor(&fx);
+    // Config and fallback are the SAME missing command, so no swap is
+    // possible.
+    exec(
+        &state,
+        &format!(
+            r#"
+            pmacs.lsp.config.lean4.command = "{}"
+            pmacs.lsp.config.lean4.args = {{}}
+            pmacs.lean._fallback = {{ command = "{}", args = {{}} }}
+            "#,
+            lua_str(&absent),
+            lua_str(&absent)
+        ),
+    );
+
+    open(&state, &file);
+    tick_for(&mut state, 400);
+
+    let attempts: i64 = eval(&state, "return pmacs.lean._probe.repair_attempts");
+    assert_eq!(
+        attempts, 0,
+        "no swap happened, so there is nothing to apply and no repair \
+         should be attempted"
+    );
+    let status = state.core.borrow().status.clone();
+    assert!(
+        !status.contains("falling back"),
+        "and nothing claims a fallback occurred; saw {status:?}"
+    );
+}
+
+#[test]
+fn r5_repair_is_attempted_at_most_once_per_buffer_by_count() {
+    // Counting keys in the `repaired` table cannot distinguish
+    // "once per buffer" from "every tick for one buffer" — the
+    // cardinality stays 1 either way. Count the ATTEMPTS.
+    let fx = Fixture::new();
+    fx.toolchain("pkg", "v4.9.0\n");
+    let file = fx.write("pkg/A.lean", "def a := 1\n");
+    let absent_primary = fx.dir("bin/no-such-lake");
+    let absent_fallback = fx.dir("bin/no-such-lean");
+    let mut state = editor(&fx);
+    exec(
+        &state,
+        &format!(
+            r#"
+            pmacs.lsp.config.lean4.command = "{}"
+            pmacs.lsp.config.lean4.args = {{ "serve" }}
+            pmacs.lean._fallback = {{ command = "{}", args = {{}} }}
+            "#,
+            lua_str(&absent_primary),
+            lua_str(&absent_fallback)
+        ),
+    );
+
+    open(&state, &file);
+    // Many ticks; a per-tick retry would climb without bound.
+    tick_for(&mut state, 900);
+
+    let attempts: i64 = eval(&state, "return pmacs.lean._probe.repair_attempts");
+    assert_eq!(
+        attempts, 1,
+        "exactly one repair attempt across many ticks for one buffer"
+    );
+}
+
+#[test]
+fn r5_a_dead_attachment_is_never_handed_to_a_command() {
+    // Buffers live in other frontends get no `buffer.after-switch` here,
+    // so an eager sweep keyed on the ambient active buffer cannot reach
+    // them. Healing at the point of USE is frontend-agnostic:
+    // `attached_for_active` must not return a record whose server is
+    // gone.
+    let fx = Fixture::new();
+    fx.toolchain("pkg", "v4.9.0\n");
+    let file = fx.write("pkg/A.lean", "def a := 1\n");
+    let mut state = editor(&fx);
+    // A working primary, so we get a live attachment first.
+    exec(
+        &state,
+        &format!("pmacs.lsp.config.lean4.command = \"{}\"", fake_lsp_path()),
+    );
+    open(&state, &file);
+    settle(&mut state);
+    let first: String = attached_sid(&state);
+    assert_ne!(first, "none", "precondition: attached");
+
+    // Retire it out from under the buffer, as the latch does globally,
+    // WITHOUT any switch or repair tick.
+    exec(
+        &state,
+        r"
+        local rec = pmacs.lsp.active_attachment()
+        pcall(pmacs.lsp.stop, rec.server)
+        ",
+    );
+    for _ in 0..40 {
+        state.tick_processes();
+        state.tick_lsp();
+        std::thread::sleep(Duration::from_millis(5));
+    }
+
+    // Now a command resolves its attachment. It must not get the dead
+    // one; it must rebuild.
+    // `attachment_for_request` is deliberately non-attaching, so a dead
+    // record must read as "no attachment" rather than being handed over.
+    let for_request: String = eval(
+        &state,
+        r#"
+        local rec = pmacs.lsp.attachment_for_request()
+        if not rec then return "none" end
+        for _, s in ipairs(pmacs.lsp.list()) do
+          if tostring(s.id) == tostring(rec.server) then
+            return tostring(s.state and s.state.kind)
+          end
+        end
+        return "gone"
+        "#,
+    );
+    assert_eq!(
+        for_request, "none",
+        "a non-attaching resolve must not hand back a dead server"
+    );
+
+    // And the attaching path rebuilds rather than returning the corpse.
+    let rebuilt: String = eval(
+        &state,
+        r#"
+        pmacs.lsp._attach_buffer()
+        local rec = pmacs.lsp.active_attachment()
+        if not rec then return "none" end
+        for _, s in ipairs(pmacs.lsp.list()) do
+          if tostring(s.id) == tostring(rec.server) then
+            return tostring(s.state and s.state.kind)
+          end
+        end
+        return "gone"
+        "#,
+    );
+    assert!(
+        rebuilt != "stopped" && rebuilt != "crashed" && rebuilt != "gone" && rebuilt != "none",
+        "the attaching path rebuilds against a live server; saw \
+         {rebuilt:?}"
+    );
+}