diff --git a/builtin/runtime/comment.lua b/builtin/runtime/comment.lua
index 7ee91e8..a9912d6 100644
--- a/builtin/runtime/comment.lua
+++ b/builtin/runtime/comment.lua
@@ -39,6 +39,10 @@ pmacs.comment.strings = {
   sh = "#",
   toml = "#",
   yaml = "#",
+  -- Lean 4 (framing Q#LN5). `--` only: Lean's block comment is `/- -/` and
+  -- its docstring `/-- -/`, but block-comment toggling is the comment arc's
+  -- own named deferral and this lane does not front-run it.
+  lean4 = "--",
 }
 
 -- Start of the line containing `pos`: chunked backward scan for the
diff --git a/builtin/runtime/pair.lua b/builtin/runtime/pair.lua
index 6d014d4..9ed9d1f 100644
--- a/builtin/runtime/pair.lua
+++ b/builtin/runtime/pair.lua
@@ -62,6 +62,22 @@ pmacs.pair.sets = {
   markdown = { "()", "[]", "{}", '""', "``" },
   sh = { "()", "[]", "{}", '""', "''" },
   bash = { "()", "[]", "{}", '""', "''" },
+  -- Lean 4 (framing Q#LN6). `⟨⟩` (anonymous constructor) is among the
+  -- most-typed constructs in Lean and omitting it would make the pair set
+  -- feel broken; `⦃⦄` (strict implicit binder) and `⟮⟯` ride along because
+  -- the Stage 4 input method can produce them (`\{{}}`, `\([])'`) and a
+  -- bracket the pair set does not understand is worse than one it does.
+  --
+  -- All three are OUTSIDE the nine built-in pair chars, so per Q#AP1 their
+  -- opener is a source-peer op and their closer a daemon-peer op: their undo
+  -- is cross-peer-degraded. That is the documented, pre-existing limitation
+  -- of user-extended pairs, whose general fix is chronological cross-peer
+  -- undo arbitration (named substrate work).
+  --
+  -- No `''`: Lean uses `'` as a primed-identifier suffix (`h'`, `foo'`), so
+  -- pairing it would fight the user constantly. Same reasoning that excludes
+  -- it for Rust.
+  lean4 = { "()", "[]", "{}", "⟨⟩", "⦃⦄", "⟮⟯", '""' },
 }
 
 -- Length of the well-formed UTF-8 sequence starting at `s[i]`, or nil
diff --git a/builtin/runtime/syntax.lua b/builtin/runtime/syntax.lua
index 812e621..50dad82 100644
--- a/builtin/runtime/syntax.lua
+++ b/builtin/runtime/syntax.lua
@@ -227,6 +227,11 @@ local default_modeline_aliases = {
   yml = "yaml",
   makefile = "make",
   docker = "dockerfile",
+  -- Lean 4 (framing Q#LN2). The grammar entry is named `lean4` because that
+  -- name becomes the `didOpen` language_id, but an Emacs `-*- mode: lean -*-`
+  -- or a Vim `ft=lean` line is what people actually write, so neither
+  -- spelling strands a file.
+  lean = "lean4",
 }
 for name, language in pairs(default_modeline_aliases) do
   if pmacs.parse.modeline_aliases[name] == nil then
diff --git a/src/highlight.rs b/src/highlight.rs
index 633ec6f..642b0a0 100644
--- a/src/highlight.rs
+++ b/src/highlight.rs
@@ -208,7 +208,12 @@ impl Theme {
             ("constructor", fg(11)),
             ("character", fg(2)),
             ("keyword.conditional", fg_bold(13)),
-            ("warning", fg_bold(1)),
+            // Bold BRIGHT red, deliberately the loudest entry in the table
+            // and deliberately distinct from `number`'s plain `fg(1)`: in a
+            // proof file `sorry` means "this is admitted, not proved", which
+            // is the one thing a reader must never skim past. Plain `fg(1)`
+            // would have collided with every numeric literal on colour alone.
+            ("warning", fg_bold(9)),
         ];
         let by_capture = entries
             .iter()
@@ -1527,6 +1532,17 @@ mod tests {
         src: &str,
         col: u32,
     ) -> pmacs_protocol::cell::Color {
+        painted_style_at(language_name, file, src, col).fg
+    }
+
+    /// As [`painted_fg_at`], but returns the whole style — needed where a
+    /// colour alone does not discriminate (Lean's `warning` vs `number`).
+    fn painted_style_at(
+        language_name: &str,
+        file: &str,
+        src: &str,
+        col: u32,
+    ) -> pmacs_protocol::cell::Style {
         use crate::buffer::{Buffer, BufferId, EditOp};
         use crate::cell::{Cell, CellSize};
         use crate::syntax::{ParseView, SyntaxRegistry};
@@ -1564,7 +1580,7 @@ mod tests {
             folds: None,
         };
         hv.render(&buf, viewport, &mut grid);
-        grid.get(CellCoord::new(0, col)).style.fg
+        grid.get(CellCoord::new(0, col)).style
     }
 
     /// Does `language`'s compiled highlight query use `capture`?
@@ -1576,6 +1592,92 @@ mod tests {
         query.capture_names().contains(&capture)
     }
 
+    #[test]
+    fn lean4_grid_paints_comment_keyword_name_operator_and_number() {
+        // Framing acceptance 5: the grammar plus the crate query plus the
+        // theme table actually produce distinct styles on a painted grid.
+        // Asserted end-to-end rather than at the query level because a
+        // capture that resolves to `Style::default()` is indistinguishable
+        // from no capture at all to a reader.
+        use pmacs_protocol::cell::Color;
+
+        // `-- c` — the whole comment run.
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "-- c\n", 0),
+            Color::Indexed(8),
+            "a Lean line comment paints the comment style"
+        );
+
+        // `def foo : Nat := 42`
+        let src = "def foo : Nat := 42\n";
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 0),
+            Color::Indexed(5),
+            "`def` paints the keyword style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 4),
+            Color::Indexed(4),
+            "the definition's name paints the function style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 14),
+            Color::Indexed(6),
+            "`:=` paints the operator style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 17),
+            Color::Indexed(1),
+            "a numeric literal paints the number style"
+        );
+
+        // A string literal, and `theorem` as a second declaration keyword.
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "def s := \"hi\"\n", 9),
+            Color::Indexed(2),
+            "a string literal paints the string style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "theorem t : True := trivial\n", 0),
+            Color::Indexed(5),
+            "`theorem` paints the keyword style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "theorem t : True := trivial\n", 8),
+            Color::Indexed(4),
+            "the theorem's name paints the function style"
+        );
+    }
+
+    #[test]
+    fn lean4_sorry_paints_the_warning_style_distinctly_from_a_number() {
+        // Framing acceptance 6. `sorry` admits a goal without proving it —
+        // in a proof file it is the single most important token to notice,
+        // and it is why Q#LN4 adds a `warning` entry at all.
+        //
+        // The style is asserted in FULL, not by colour: `number` and the
+        // first-choice `warning` colour were both indexed red, so a
+        // colour-only assertion would have passed with `sorry` painted
+        // exactly like the literal `42` beside it. That is the whole failure
+        // this test exists to prevent.
+        use pmacs_protocol::cell::Color;
+
+        let sorry = painted_style_at("lean4", "a.lean", "theorem t : True := sorry\n", 20);
+        assert_eq!(
+            sorry.fg,
+            Color::Indexed(9),
+            "`sorry` paints the warning colour"
+        );
+        assert!(sorry.bold, "`sorry` is bold");
+
+        let number = painted_style_at("lean4", "a.lean", "def n := 42\n", 9);
+        assert_ne!(
+            (sorry.fg, sorry.bold),
+            (number.fg, number.bold),
+            "`sorry` must be visually distinct from a numeric literal"
+        );
+    }
+
     #[test]
     fn lean4_constructor_capture_retro_paints_the_whole_javascript_family() {
         // Framing acceptance 7 (Q#LN4), the breadth half. `constructor` was
diff --git a/src/syntax.rs b/src/syntax.rs
index edec588..bc6acf9 100644
--- a/src/syntax.rs
+++ b/src/syntax.rs
@@ -251,6 +251,12 @@ pub fn default_injection_aliases() -> HashMap<String, String> {
         ("golang", "go"),
         ("yml", "yaml"),
         ("md", "markdown"),
+        // Lean 4 (framing Q#LN17). A ```lean fence is overwhelmingly Lean 4
+        // in practice, so the Lean 3 spelling is deliberately mapped forward
+        // rather than left unresolved. `lean4` needs no alias — it is the
+        // entry name. `lean4-mode` does the equivalent through
+        // `markdown-code-lang-modes`.
+        ("lean", "lean4"),
     ]
     .into_iter()
     .map(|(a, b)| (a.to_owned(), b.to_owned()))
diff --git a/tests/lean4_stage1_acceptance.rs b/tests/lean4_stage1_acceptance.rs
new file mode 100644
index 0000000..ae65545
--- /dev/null
+++ b/tests/lean4_stage1_acceptance.rs
@@ -0,0 +1,320 @@
+//! Lean 4 mode, Stage 1 acceptance (Arc 8, `docs/lean4-mode-framing.md`).
+//!
+//! Covers the framing's Stage 1 criteria that live above the Rust
+//! substrate — major mode, modeline aliasing, comment toggle, the pair
+//! set, and markdown fence injection. Criteria 1, 2, and the Q#LN4
+//! retro-paint pins (7, 8) are unit tests in `src/syntax.rs` and
+//! `src/highlight.rs`, where the theme table and grammar registry live.
+//!
+//! Dispatch-driven, following `comment_toggle_acceptance`: `M-;` and
+//! typed characters go through `dispatch_key` so the real command
+//! boundary and typed-edit provenance are exercised. Buffers are
+//! file-backed (language detection needs a path); each editor gets a
+//! private tempdir `StateDir` and an emptied `pmacs.lsp.config` so
+//! nothing spawns a language server — Stage 1 has no LSP at all.
+//!
+//! Criterion 12 is the reason this suite touches no process: it must
+//! pass on a machine with no `lean`, no `lake`, and no configured elan
+//! toolchain. That is not hypothetical — the machine this arc was
+//! scouted on has elan installed with no default toolchain, where
+//! `lake --version` itself fails.
+
+use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
+use pmacs::editor::EditorState;
+use pmacs::lua_bindings::StateDir;
+use pmacs::protocol::FrontendId;
+use std::path::PathBuf;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+fn fresh_state_dir() -> PathBuf {
+    static SEQ: AtomicUsize = AtomicUsize::new(0);
+    let dir = std::env::temp_dir().join(format!(
+        "pmacs-lean4-{}-{}",
+        std::process::id(),
+        SEQ.fetch_add(1, Ordering::Relaxed)
+    ));
+    std::fs::create_dir_all(&dir).unwrap();
+    dir
+}
+
+fn editor(state_dir: &std::path::Path) -> EditorState {
+    let s = EditorState::new();
+    s.lua_host.lua().remove_app_data::<StateDir>();
+    s.lua_host
+        .lua()
+        .set_app_data(StateDir(state_dir.to_path_buf()));
+    exec(&s, "pmacs.lsp.config = {}");
+    s
+}
+
+fn write_file(dir: &std::path::Path, name: &str, body: &str) -> String {
+    let p = dir.join(name);
+    std::fs::write(&p, body).unwrap();
+    p.display().to_string()
+}
+
+fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent {
+    KeyEvent {
+        code,
+        modifiers: mods,
+        kind: KeyEventKind::Press,
+        state: KeyEventState::NONE,
+    }
+}
+
+fn alt(s: &mut EditorState, c: char) {
+    s.dispatch_key(FrontendId::LOCAL, key(KeyCode::Char(c), KeyModifiers::ALT));
+}
+
+fn type_str(s: &mut EditorState, text: &str) {
+    for ch in text.chars() {
+        s.dispatch_key(
+            FrontendId::LOCAL,
+            key(KeyCode::Char(ch), KeyModifiers::NONE),
+        );
+    }
+}
+
+fn exec(s: &EditorState, src: &str) {
+    s.lua_host.lua().load(src.to_string()).exec().unwrap();
+}
+
+fn eval<T: mlua::FromLuaMulti>(s: &EditorState, src: &str) -> T {
+    s.lua_host.lua().load(src.to_string()).eval().unwrap()
+}
+
+fn buffer_text(s: &EditorState) -> String {
+    let b: mlua::String = eval(
+        s,
+        "local b = pmacs.window.buffer(); return b:slice(0, b:len())",
+    );
+    String::from_utf8_lossy(&b.as_bytes()).into_owned()
+}
+
+fn cursor(s: &EditorState) -> i64 {
+    eval(s, "return pmacs.editor.cursor()")
+}
+
+/// Fresh editor visiting `name` (created in the state tempdir) with
+/// `body` on disk, cursor at 0.
+fn editor_visiting(name: &str, body: &str) -> EditorState {
+    let dir = fresh_state_dir();
+    let s = editor(&dir);
+    let f = write_file(&dir, name, body);
+    exec(&s, &format!("pmacs.buffer.find_or_open({f:?})"));
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    s
+}
+
+fn major_mode(s: &EditorState) -> Option<String> {
+    eval(s, "return pmacs.buffer.major_mode(pmacs.window.buffer())")
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 3 — major mode
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc3_opening_a_lean_file_sets_the_lean4_major_mode() {
+    let s = editor_visiting("Basic.lean", "def x : Nat := 1\n");
+    assert_eq!(
+        major_mode(&s).as_deref(),
+        Some("lean4"),
+        "a .lean file carries the lean4 major mode"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 4 — modeline aliasing (Q#LN2)
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc4_emacs_and_vim_modelines_spelling_lean_resolve_to_lean4() {
+    // The grammar entry is `lean4`, but `-*- mode: lean -*-` and `ft=lean`
+    // are what people write. Both must land on the same mode, or a file
+    // with an explicit modeline is stranded with no grammar.
+    //
+    // Deliberately on a `.txt` path: if the fixture were `.lean`, the
+    // extension alone would produce `lean4` and the assertion would pass
+    // with the alias table empty — the vacuous shape.
+    for body in [
+        "-- -*- mode: lean -*-\ndef x : Nat := 1\n",
+        "-- vim: ft=lean\ndef x : Nat := 1\n",
+    ] {
+        let s = editor_visiting("modeline.txt", body);
+        assert_eq!(
+            major_mode(&s).as_deref(),
+            Some("lean4"),
+            "modeline {body:?} resolves through the alias to lean4"
+        );
+    }
+}
+
+#[test]
+fn acc4b_the_lean_alias_is_load_bearing() {
+    // Non-vacuity guard for acc4: with the alias removed, the same
+    // fixture resolves to the raw `lean` name instead. If this ever
+    // reports `lean4`, acc4 is proving nothing.
+    let s = editor_visiting("modeline.txt", "x\n");
+    exec(&s, "pmacs.parse.modeline_aliases.lean = nil");
+    let dir = fresh_state_dir();
+    let f = write_file(&dir, "other.txt", "-- -*- mode: lean -*-\ndef x := 1\n");
+    exec(&s, &format!("pmacs.buffer.find_or_open({f:?})"));
+    assert_eq!(
+        major_mode(&s).as_deref(),
+        Some("lean"),
+        "without the alias the modeline name is not normalized"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 9 — comment toggle (Q#LN5)
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc9_comment_toggle_round_trips_with_the_dash_dash_prefix() {
+    let mut s = editor_visiting("Basic.lean", "def x : Nat := 1\ndef y : Nat := 2\n");
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    alt(&mut s, ';');
+    assert_eq!(
+        buffer_text(&s),
+        "-- def x : Nat := 1\ndef y : Nat := 2\n",
+        "M-; comments a Lean line with `-- `"
+    );
+    // Round trip, including the padding space.
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    alt(&mut s, ';');
+    assert_eq!(
+        buffer_text(&s),
+        "def x : Nat := 1\ndef y : Nat := 2\n",
+        "M-; uncomments it exactly"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 10 — pairs (Q#LN6)
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc10_lean_bracket_pairs_close_and_the_prime_does_not() {
+    // The three Unicode brackets are the reason this decision exists: all
+    // are outside the nine built-in pair chars, so they exercise the
+    // user-extended pair path rather than the frontends' optimistic
+    // classifier.
+    for (opener, expected) in [("⟨", "⟨⟩"), ("⦃", "⦃⦄"), ("⟮", "⟮⟯")] {
+        let mut s = editor_visiting("Basic.lean", "");
+        exec(&s, "pmacs.editor.goto_byte(0)");
+        type_str(&mut s, opener);
+        assert_eq!(
+            buffer_text(&s),
+            expected,
+            "typing {opener} inserts the closing half"
+        );
+        assert_eq!(
+            cursor(&s),
+            i64::try_from(opener.len()).expect("opener length fits"),
+            "the point sits between the pair"
+        );
+    }
+}
+
+#[test]
+fn acc10b_the_prime_suffix_does_not_pair_in_lean() {
+    // Lean uses `'` as a primed-identifier suffix (`h'`, `foo'`), so
+    // pairing it would fight the user on nearly every proof.
+    let mut s = editor_visiting("Basic.lean", "");
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    type_str(&mut s, "h'");
+    assert_eq!(
+        buffer_text(&s),
+        "h'",
+        "the prime is a suffix in Lean, not an opener"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 11 — markdown fences (Q#LN17)
+// ---------------------------------------------------------------------------
+
+/// Parse `src` as markdown and return the child layer language names.
+///
+/// Goes through the real `_parse_now` injection path rather than reading
+/// the alias table: `pmacs.parse.injection_aliases` is a documented
+/// WRITE-ONLY proxy (the canonical map lives Rust-side), so an
+/// alias-table read would prove nothing about what the parser does.
+fn markdown_layer_languages(src: &[u8]) -> Vec<String> {
+    let state = EditorState::new();
+    let buf_id = state
+        .lua_host
+        .registry()
+        .borrow_mut()
+        .create_from_bytes("doc.md".to_owned(), src);
+    state
+        .lua_host
+        .lua()
+        .globals()
+        .set("BUF", pmacs::lua_bindings::BufferIdLua(buf_id))
+        .expect("bind BUF");
+    state
+        .lua_host
+        .lua()
+        .load("pmacs.parse._parse_now(BUF, 'markdown')")
+        .exec()
+        .expect("synchronous parse");
+    let bundle = state
+        .syntax_registry
+        .view(buf_id)
+        .and_then(|h| h.current())
+        .expect("installed bundle");
+    bundle
+        .layers
+        .iter()
+        .map(|l| l.language_name.clone())
+        .collect()
+}
+
+#[test]
+fn acc11_lean_and_lean4_markdown_fences_both_inject_the_lean_grammar() {
+    // Both spellings must resolve to the same grammar: `lean4` is the entry
+    // name and `lean` goes through the injection alias. A ```lean fence is
+    // overwhelmingly Lean 4 in practice, which is why the Lean 3 spelling
+    // is mapped forward rather than left unresolved (Q#LN17).
+    for fence in ["lean", "lean4"] {
+        let src = format!("# Doc\n\n```{fence}\ndef x : Nat := 1\n```\n");
+        let langs = markdown_layer_languages(src.as_bytes());
+        assert!(
+            langs.iter().any(|l| l == "lean4"),
+            "```{fence} injects a lean4 child layer; got {langs:?}"
+        );
+    }
+}
+
+#[test]
+fn acc11b_an_unknown_fence_name_still_injects_nothing() {
+    // Non-vacuity guard for acc11: the alias must be what resolves `lean`,
+    // not some catch-all that would light up any fence name.
+    let langs = markdown_layer_languages(b"# Doc\n\n```leen\ndef x := 1\n```\n");
+    assert!(
+        !langs.iter().any(|l| l == "lean4"),
+        "a misspelled fence must not reach the lean4 grammar; got {langs:?}"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 12 — no toolchain required
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc12_stage1_spawns_no_process_and_needs_no_lean_toolchain() {
+    // 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.
+    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");
+}