fix(test): make acc12 pin the claim it names (review round 1)

Review finding: acc12's server-list assertion could not fail for the
regression class it was written to catch. The shared `editor()` helper
runs `pmacs.lsp.config = {}` before any buffer opens, so
`#pmacs.lsp.list() == 0` holds for every language regardless of what
Stage 1 ships -- a Stage-3 front-run that added
`pmacs.lsp.config.lean4` in a builtin runtime file would have slipped
straight past it. The same vacuous-assertion shape as #155 R2.

acc12 now asserts the actual claim against a PRISTINE `EditorState`,
before any config wipe: no builtin runtime file defines
`pmacs.lsp.config.lean4`. A non-vacuity check pins that the same lookup
finds `pmacs.lsp.config.rust`, so this cannot pass merely because the
table is empty or absent.

Bite-verified: adding `pmacs.lsp.config.lean4 = ... { command = "lake",
args = { "serve" } }` to `builtin/runtime/lsp.lua` fails the test; the
stub was reverted.

The process-list half is kept and its comment now says why it survives
the wipe: a direct probe spawn from a future `lean.lua` shows up there
whatever `pmacs.lsp.config` contains.

Also fixes a stale column in a `highlight.rs` comment -- the Lua table
brace in `local t = {}` is at col 10, which is what the code already
used.

Gates rerun: fmt and strict workspace clippy clean; 1,826 default +
2,003 CRDT library tests; lean4 Stage 1 9/9; M4 121; required GPU 152;
isolated-config workspace sweep 3,150 across 90 suites; diff check clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

src/highlight.rs

@@ -1737,7 +1737,8 @@ mod tests {
             Color::Indexed(4),
             "a called variant keeps @function, not @constructor"
         );
-        // Lua tags the table-constructor BRACES, not a name: `{` at col 8.
+        // Lua tags the table-constructor BRACES, not a name: `{` at col 10
+        // of `local t = {}`.
         assert_eq!(
             painted_fg_at("lua", "a.lua", "local t = {}\n", 10),
             Color::Indexed(11),

tests/lean4_stage1_acceptance.rs

@@ -305,16 +305,36 @@ fn acc11b_an_unknown_fence_name_still_injects_nothing() {
 // ---------------------------------------------------------------------------
 
 #[test]
-fn acc12_stage1_spawns_no_process_and_needs_no_lean_toolchain() {
+fn acc12_stage1_ships_no_lsp_config_and_spawns_no_process() {
     // Stage 1 is grammar + Lua tables only. Opening a Lean file must not
     // reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and
     // even then it is fallible by design (Q#LN7).
-    //
-    // Asserted through the process supervisor rather than by inspection:
-    // opening the file leaves the child-process list exactly as it was.
+
+    // The load-bearing assertion, and it must run against a PRISTINE editor.
+    // The shared `editor()` helper wipes `pmacs.lsp.config` before any
+    // buffer opens, so an assertion about the server list under that harness
+    // holds for every language regardless of what Stage 1 ships — it could
+    // not fail for the regression it names. This checks the real claim
+    // directly: no builtin runtime file defines a Lean server config. A
+    // Stage-3 front-run adding `pmacs.lsp.config.lean4` fails here.
+    let pristine = EditorState::new();
+    let no_lean_config: bool = eval(&pristine, "return pmacs.lsp.config.lean4 == nil");
+    assert!(
+        no_lean_config,
+        "Stage 1 defines no `pmacs.lsp.config.lean4`; the LSP is Stage 3"
+    );
+    // Non-vacuity: the same lookup finds the configs that DO ship, so this
+    // is not passing because `pmacs.lsp.config` is empty or absent.
+    let rust_config_exists: bool = eval(&pristine, "return pmacs.lsp.config.rust ~= nil");
+    assert!(
+        rust_config_exists,
+        "the config table is populated, so the lean4 absence above is meaningful"
+    );
+
+    // And nothing is spawned by opening the file. This half retains its
+    // value under the wiped config: a direct probe spawn from `lean.lua`
+    // would show up here whatever `pmacs.lsp.config` contains.
     let s = editor_visiting("Basic.lean", "def x : Nat := 1\n");
     let procs: i64 = eval(&s, "return #pmacs.process.list()");
     assert_eq!(procs, 0, "opening a Lean buffer spawns no child process");
-    let servers: i64 = eval(&s, "return #pmacs.lsp.list()");
-    assert_eq!(servers, 0, "Stage 1 attaches no language server");
 }