docs: record Stage 1's landing and the Stage 2 affinity lane

Stage 1 merged as #160 (`main` @ `0827dd1`); the Lean lane header and
branch line now say so, and Stage 2 gets its own subsection.

Edits stay inside the Lean lane. PR #156 is still open against both this
file and `docs/agent-handoff.md`, and it rewrites the snapshot header,
the canonical-base line, and the whole bottom-panel lane — so those are
left alone rather than merged twice. `agent-handoff.md` is untouched for
the same reason plus its own: §1 describes what is on `main`, so it
updates at merge, not during review.

Records the one finding this stage turned up but did not fix:
`ensure_server` never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a
`restart` in `pmacs.lsp.config[lang]` is silently dropped on the
auto-attach path. Pre-existing, and out of scope for a PR whose
acceptance 16 pins existing attach behavior as unchanged.

docs/active-work.md

@@ -54,10 +54,11 @@ git status --short --branch
 The `git log` command must expose `0dd16a5` or a newer intentional main.
 If it does not, stop and repair the remote/fetch configuration.
 
-## Lean 4 lane (Arc 8) — Stage 1 IN REVIEW (PR #160)
+## Lean 4 lane (Arc 8) — Stage 1 MERGED; Stage 2 IN REVIEW (PR #TBD)
 
-- Portable branch: `githubsucks/lean4-stage1`, worked in the shared
-  checkout (no sibling worktree), based on `githubsucks/main` @ `e745068`.
+- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
+  round, all twelve checks green). Branch `githubsucks/lean4-stage1`
+  retained; it was worked in the shared checkout (no sibling worktree).
 - Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as
   the branch's first commit (`a382965`) after three review rounds. **Seven
   stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star:
@@ -113,16 +114,59 @@ If it does not, stop and repair the remote/fetch configuration.
   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 is multi-root LSP server affinity** — pure substrate, no Lean
-  content, and it changes `ensure_server`, which every LSP language
-  shares. It is sequenced next because Lean is the language that makes its
-  absence a correctness failure rather than an inconvenience. Two
-  corrections the framing already carries for it: `root` is computed at
-  `lsp.lua:537`, **after** the reuse loop, so the fix must hoist it; and
-  `project_root_for` never returns nil for a file with a path, so the
-  affinity key must be the root only when a root was actually *detected*,
-  or markerless scratch files fragment into one server per directory for
-  every language.
+### Stage 2 — multi-root LSP server affinity (Q#LN15)
+
+- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout,
+  based on `githubsucks/main` @ `0827dd1`. Named for the substrate, not
+  for Lean: **the diff contains no Lean content**, because `ensure_server`
+  is the one server-affinity function every LSP language shares and a
+  cross-cutting change to it must not be reviewable only as a Lean
+  feature.
+- Three files, no protocol change: `src/lua_bindings/mod.rs` (the
+  `lsp.list()` row builder gains `root_uri` + `cwd`),
+  `builtin/runtime/lsp.lua` (`project_root_for` returns `root, source`;
+  `ensure_server` hoists it above the reuse loop and matches on it),
+  `tests/lsp_multi_root_acceptance.rs` (9 tests, acceptance 13–21).
+- **The rule that keeps this from regressing every other language: the
+  affinity key is the root only when a root was actually FOUND.**
+  `project_root_for` never returns nil for a file with a path — its last
+  resort is the file's own directory — so a naive `(language_id, root)`
+  key gives every directory of loose scratch files its own server, for
+  every language. `source` is `"config" | "detected" | "fallback"` and
+  only the first two become a key.
+- **Wire-identical for the fallback case, and that is provable rather
+  than hoped.** Matching is on the spawned spec's `root_uri` (nil matching
+  nil), so the fallback spawn passes `root_uri = nil`; `cwd` still carries
+  the directory and `build_initialize` derives the identical `rootUri`
+  from `cwd` when the field is None, using a percent-encoder with the same
+  allowed set as Lua's `file_uri_for`. `build_initialize` (`src/lsp.rs`)
+  is the **only** reader of `spec.root_uri` in the tree.
+- Deliberate behavior change, asserted not discovered: a server
+  hand-spawned from `init.lua` with only `cwd` set also reads back nil, so
+  a root-bearing attach will not adopt it.
+- `config[language].root` may now be a `function(path) -> string|nil`,
+  memoized per directory — needed because the hoist puts root resolution
+  on every attach rather than every spawn. The memo is keyed **weakly by
+  the resolver function itself**, so replacing `config[lang].root` cannot
+  serve a root the previous resolver computed. This is Q#LN8's
+  generalization landing early; the Lean resolver that uses it is Stage 3.
+- Bite-verified three ways: 5/9 fail against the pre-change `lsp.lua`,
+  8/9 against the pre-change `mod.rs`, and — the one that matters most —
+  installing the naive always-key-on-root variant fails acceptance 20 and
+  21 exactly as Q#LN15 part 2 predicts. The four that survive the first
+  bite (13, 15, 16, 19) are the regression pins; passing on both sides is
+  their job.
+- Every fixture sets `pmacs.project.set_search_boundary` at its own
+  tempdir root. Without it the marker walk climbs to the filesystem root
+  and a stray `.git` above the temp directory turns the markerless cases
+  into detected ones — the assertions would still pass while testing
+  nothing.
+- **Found but not fixed here (pre-existing, own lane):** `ensure_server`
+  never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a
+  `restart = "never"` in `pmacs.lsp.config[lang]` is silently dropped on
+  the auto-attach path. At least one existing test sets it believing it
+  takes effect. Out of scope for a PR whose acceptance 16 pins existing
+  attach behavior as unchanged.
 
 ## Bottom-panel lane (window placement + side windows) — Stage 1 IN REVIEW