diff --git a/python/lean_pool/exposition/SCHEMA.md b/python/lean_pool/exposition/SCHEMA.md
index e96b29a200..31760d6f14 100644
--- a/python/lean_pool/exposition/SCHEMA.md
+++ b/python/lean_pool/exposition/SCHEMA.md
@@ -114,6 +114,42 @@ Link recipes: `doi` → `https://doi.org/<doi>`, `arxiv` →
 `https://arxiv.org/abs/<arxiv>`, `url` as-is, `github_repo` →
 `https://github.com/<github_repo>`.
 
+### Minimal-Lean-file fields (schema 1.2, additive)
+
+The shard gains `commit` (the exact commit its data was extracted from —
+raw-source fetches for the minimal-file builder pin to it) and a
+`moduleData` array parallel to `modules`:
+
+```json
+"moduleData": [{"imports": ["Mathlib.Order.Basic", …],   // external imports
+                "uses": [3, 7],                           // same-project imports (module indices)
+                "contexts": [[20, "namespace Foo"], …]},  // (line, text) of replayable top-level
+               …]                                         //   context commands
+```
+
+`modules` may list more entries than declarations reference: modules pulled
+in only through `uses` (notation-/attribute-only files) are appended so
+their contexts can be replayed.
+
+Per-declaration additions:
+
+```json
+"stmtEnd": [436, 69],   // theorem/lemma only: statement/body boundary (line, col)
+"tdeps": [124, 164],    // theorem/lemma only: statement-only dependencies ⊆ deps
+"span": [15, 18],       // mutual members: the whole block's line span
+"host": 12,             // generated decls: the source declaration containing them
+"prefix": "open Classical in"  // bare `… in` prefix excluded from Lean's range
+```
+
+The minimal-file builder (`static/assets/minimal.js`, shared verbatim with
+the node validation harness) follows `tdeps` through theorems (proofs become
+`:= sorry`) and full `deps` elsewhere, replays module contexts in import
+order, prunes `variable`/`attribute`/`export` contexts that reference
+declarations outside the cone, and grows the cone with lemmas named in
+`simp only [...]`-style tactic lists (invisible to term-level dependency
+extraction). `build()` may return `{pending: [moduleIndex…]}` when that
+closure needs sources not yet fetched; callers fetch and retry (≤ 4 rounds).
+
 ## `data/index.json`
 
 ```json
diff --git a/python/lean_pool/exposition/generate.py b/python/lean_pool/exposition/generate.py
index 935e49cf6a..8fa85a0575 100644
--- a/python/lean_pool/exposition/generate.py
+++ b/python/lean_pool/exposition/generate.py
@@ -23,7 +23,12 @@
 import yaml
 
 from lean_pool.exposition.layout import compute_layout
-from lean_pool.exposition.source_text import SourceFile, statement_slice
+from lean_pool.exposition.source_text import (
+    ModuleSkeleton,
+    SourceFile,
+    module_skeleton,
+    statement_slice,
+)
 
 logger = logging.getLogger(__name__)
 
@@ -201,14 +206,18 @@ def _sorted_records(records: list[dict]) -> list[dict]:
     )
 
 
-def _remap_dependencies(records: list[dict]) -> list[list[int]]:
-    """Map dependency ids to shard-local indices, dropping dangling/self refs."""
+def _remap_dependencies(records: list[dict], key: str = "deps") -> list[list[int]]:
+    """Map dependency ids under ``key`` to shard-local indices.
+
+    Dangling and self references are dropped. Records without the key yield
+    an empty list.
+    """
     index_of = {record["id"]: index for index, record in enumerate(records)}
     dependency_lists: list[list[int]] = []
     for index, record in enumerate(records):
         indices = {
             index_of[dependency]
-            for dependency in record.get("deps", [])
+            for dependency in record.get(key, [])
             if dependency in index_of
         }
         indices.discard(index)
@@ -218,19 +227,90 @@ def _remap_dependencies(records: list[dict]) -> list[list[int]]:
 
 def _refined_kind_and_statement(
     record: dict, source: SourceFile | None
-) -> tuple[str, str]:
+) -> tuple[str, str, tuple[int, int] | None]:
     """Refine the extractor kind and slice the statement from the source."""
     if source is None:
-        return record["k"], ""
+        return record["k"], "", None
     return statement_slice(source, record["r"], record["s"], record["k"])
 
 
+# Declarations whose proofs the minimal Lean file replaces with `sorry`.
+PROOF_KINDS = frozenset({"theorem", "lemma"})
+
+
+def _attach_minimal_file_fields(
+    nodes: list[dict],
+    skeletons: dict[int, ModuleSkeleton | None],
+) -> None:
+    """Add per-node minimal-file fields: ``span`` and ``host`` (schema 1.2).
+
+    ``span`` widens a node's verbatim slice to its enclosing top-level
+    ``mutual`` block. ``host`` points a generated declaration (mid-line
+    range, blanked statement) at the human-written declaration whose source
+    contains it, so the builder can emit the host instead.
+    """
+    by_module: dict[int, list[int]] = {}
+    for node_id, node in enumerate(nodes):
+        by_module.setdefault(node["module"], []).append(node_id)
+    for module_index, node_ids in by_module.items():
+        skeleton = skeletons.get(module_index)
+        if skeleton is not None:
+            for start_line, end_line in skeleton.mutual_spans:
+                for node_id in node_ids:
+                    node = nodes[node_id]
+                    if start_line <= node["line"] and node["endLine"] <= end_line:
+                        node["span"] = [start_line, end_line]
+        if skeleton is not None and skeleton.prefix_blocks:
+            # Lean's declaration range excludes a bare `open/set_option/
+            # attribute … in` prefix on the preceding lines; reattach it.
+            # The prefix's following command may start inside the node's
+            # range at a later line than node["line"] when a doc comment
+            # sits between them, hence the range check. Chains supported.
+            prefix_by_next_line = {
+                next_line: (line, text)
+                for line, next_line, text in skeleton.prefix_blocks
+            }
+            for node_id in node_ids:
+                node = nodes[node_id]
+                chain_end = None
+                for line, next_line, text in skeleton.prefix_blocks:
+                    if node["line"] <= next_line <= node["endLine"]:
+                        chain_end = (line, text)
+                        break
+                if chain_end is None:
+                    continue
+                parts = [chain_end[1]]
+                cursor = chain_end[0]
+                while cursor in prefix_by_next_line:
+                    line, text = prefix_by_next_line[cursor]
+                    parts.append(text)
+                    cursor = line
+                node["prefix"] = "\n".join(reversed(parts))
+        for node_id in node_ids:
+            node = nodes[node_id]
+            generated = node["statement"] == "" and "stmtEnd" not in node
+            if not generated:
+                continue
+            host = None
+            for other_id in node_ids:
+                other = nodes[other_id]
+                if other_id == node_id or other["statement"] == "":
+                    continue
+                if other["line"] <= node["line"] <= other["endLine"]:
+                    if host is None or other["line"] >= nodes[host]["line"]:
+                        host = other_id
+            if host is not None:
+                node["host"] = host
+
+
 def _build_node(
     record: dict,
     kind: str,
     statement: str,
+    statement_end: tuple[int, int] | None,
     module_index: int,
     dependencies: list[int],
+    type_dependencies: list[int] | None,
     layer: int,
     order: int,
 ) -> dict:
@@ -245,9 +325,13 @@ def _build_node(
     if "d" in record:
         node["doc"] = record["d"]
     node["statement"] = statement
+    if statement_end is not None and kind in PROOF_KINDS:
+        node["stmtEnd"] = list(statement_end)
     if record.get("p"):
         node["private"] = True
     node["deps"] = dependencies
+    if type_dependencies is not None and kind in PROOF_KINDS:
+        node["tdeps"] = type_dependencies
     node["ext"] = record.get("ext", 0)
     node["layer"] = layer
     node["order"] = order
@@ -260,33 +344,67 @@ def _kind_counts(kinds: list[str]) -> dict[str, int]:
     return dict(sorted(counts.items(), key=lambda item: (-item[1], item[0])))
 
 
+def _closed_module_list(
+    slug: str, project_modules: list[str], source_cache: SourceCache
+) -> tuple[list[str], dict[int, ModuleSkeleton | None]]:
+    """Close the module list under same-project imports; return skeletons.
+
+    Modules without exposed declarations (notation- or attribute-only files)
+    still contribute context commands, so the minimal-file builder needs
+    their skeletons too; they are appended after the declaration-bearing
+    modules.
+    """
+    modules = list(project_modules)
+    known = set(modules)
+    project_prefix = f"LeanPool.{slug}."
+    skeletons: dict[int, ModuleSkeleton | None] = {}
+    index = 0
+    while index < len(modules):
+        source = source_cache.get(modules[index])
+        skeleton = module_skeleton(source) if source else None
+        skeletons[index] = skeleton
+        if skeleton is not None:
+            for imported in skeleton.local_imports:
+                if imported.startswith(project_prefix) and imported not in known:
+                    known.add(imported)
+                    modules.append(imported)
+        index += 1
+    return modules, skeletons
+
+
 def build_project_shard(
     slug: str,
     records: list[dict],
     card: ProjectCard | None,
     source_cache: SourceCache,
+    commit: str = "main",
 ) -> dict:
     """Build one ``data/projects/<Project>.json`` payload per SCHEMA.md."""
     ordered = _sorted_records(records)
-    modules = sorted({record["m"] for record in ordered})
+    declaration_modules = sorted({record["m"] for record in ordered})
+    modules, skeletons = _closed_module_list(slug, declaration_modules, source_cache)
     module_indices = {module: index for index, module in enumerate(modules)}
     dependency_lists = _remap_dependencies(ordered)
+    type_dependency_lists = _remap_dependencies(ordered, key="tdeps")
     layout = compute_layout(dependency_lists)
     nodes = []
     for index, record in enumerate(ordered):
         source = source_cache.get(record["m"])
-        kind, statement = _refined_kind_and_statement(record, source)
+        kind, statement, statement_end = _refined_kind_and_statement(record, source)
         nodes.append(
             _build_node(
                 record,
                 kind,
                 statement,
+                statement_end,
                 module_indices[record["m"]],
                 dependency_lists[index],
+                type_dependency_lists[index] if "tdeps" in record else None,
                 layout.node_layers[index],
                 layout.node_orders[index],
             )
         )
+    _attach_minimal_file_fields(nodes, skeletons)
     node_count = len(nodes)
     average = sum(layout.node_layers) / node_count if node_count else 0.0
     stats = {
@@ -297,15 +415,34 @@ def build_project_shard(
         "kinds": _kind_counts([node["kind"] for node in nodes]),
     }
     main_results = _resolve_main_results(card, nodes)
+    module_data = []
+    for index in range(len(modules)):
+        skeleton = skeletons[index]
+        uses = sorted(
+            module_indices[imported]
+            for imported in (skeleton.local_imports if skeleton else [])
+            if imported in module_indices
+        )
+        module_data.append(
+            {
+                "imports": skeleton.external_imports if skeleton else [],
+                "uses": uses,
+                "contexts": [list(entry) for entry in skeleton.contexts]
+                if skeleton
+                else [],
+            }
+        )
     return {
         "schema": 1,
         "project": slug,
+        "commit": commit,
         "title": card.title if card else None,
         "provenance": card.provenance if card else None,
         "card": card.card if card and card.card else None,
         "mainResults": main_results,
         "stats": stats,
         "modules": modules,
+        "moduleData": module_data,
         "layers": layout.layer_sizes,
         "decls": nodes,
     }
@@ -419,7 +556,7 @@ def generate_site(
     cards = load_project_cards(Path(repo_root) / "LeanPool" / "projects.yml")
     source_cache = SourceCache(Path(repo_root))
     shards = {
-        slug: build_project_shard(slug, records, cards.get(slug), source_cache)
+        slug: build_project_shard(slug, records, cards.get(slug), source_cache, commit)
         for slug, records in grouped.items()
     }
     index = build_index(shards, commit)
diff --git a/python/lean_pool/exposition/source_text.py b/python/lean_pool/exposition/source_text.py
index 0437154521..a13195ee93 100644
--- a/python/lean_pool/exposition/source_text.py
+++ b/python/lean_pool/exposition/source_text.py
@@ -15,6 +15,7 @@
 
 from __future__ import annotations
 
+import bisect
 import re
 from collections.abc import Sequence
 from dataclasses import dataclass
@@ -63,13 +64,15 @@
 _IN_RE = re.compile(r"(?<![\w.'])in(?![\w'])")
 
 
-def code_view(text: str) -> str:
-    """Return ``text`` with comments and string literals blanked to spaces.
+def code_view(text: str, blank_strings: bool = True) -> str:
+    """Return ``text`` with comments (and optionally strings) blanked.
 
     Copied from ``scripts/proof-profile/statements.py``. Length and newline
     positions are preserved so indices computed on the result line up with
     the original source. Block comments (``/- -/``) nest, which also covers
-    doc comments (``/-- -/``) and module docs (``/-! -/``).
+    doc comments (``/-- -/``) and module docs (``/-! -/``). With
+    ``blank_strings=False`` string literals keep their content (used when
+    trimming trailing comments off a command without eating a final string).
     """
     out: list[str] = []
     i, n = 0, len(text)
@@ -92,7 +95,7 @@ def code_view(text: str) -> str:
                 block_depth = 1
                 continue
             if c == '"':
-                out.append(" ")
+                out.append(" " if blank_strings else '"')
                 i += 1
                 state = string_literal
                 continue
@@ -122,15 +125,21 @@ def code_view(text: str) -> str:
             i += 1
         else:  # string literal
             if c == "\\":
-                out.append("  " if i + 1 < n else " ")
+                if blank_strings:
+                    out.append("  " if i + 1 < n else " ")
+                else:
+                    out.append(text[i : i + 2])
                 i += 2
                 continue
             if c == '"':
-                out.append(" ")
+                out.append('"' if not blank_strings else " ")
                 state = normal
                 i += 1
                 continue
-            out.append("\n" if c == "\n" else " ")
+            if blank_strings:
+                out.append("\n" if c == "\n" else " ")
+            else:
+                out.append(c)
             i += 1
     return "".join(out)
 
@@ -187,6 +196,11 @@ def _line_prefix(code: str, pos: int) -> str:
     return code[start:pos]
 
 
+def _ident_char(character: str) -> bool:
+    """Is this character part of a Lean identifier token (statements.py)?"""
+    return character.isalnum() or character in "_.'" or ord(character) > 127
+
+
 def _find_boundary(
     code: str, start: int, end: int, bar_always_ends: bool = False
 ) -> int:
@@ -203,12 +217,24 @@ def _find_boundary(
     b_assign = b_where = b_bar = None
     seen_bars: list[int] = []
     depth = 0
+    pending_binders = 0  # top-level `let`/`have` in the type own the next `:=`
     i = start
     while i < end:
         c = code[i]
         if depth == 0:
+            if code[i : i + 4] in ("let ", "let\n", "let\t") and not _ident_char(
+                code[i - 1] if i > start else " "
+            ):
+                pending_binders += 1
+            elif code[i : i + 5] in ("have ", "have\n", "have\t") and not _ident_char(
+                code[i - 1] if i > start else " "
+            ):
+                pending_binders += 1
             if b_assign is None and code[i : i + 2] == ":=":
-                b_assign = i
+                if pending_binders > 0:
+                    pending_binders -= 1
+                else:
+                    b_assign = i
             elif (
                 code[i : i + 2] == "=>"
                 and seen_bars
@@ -260,6 +286,12 @@ def offset(self, line: int, column: int) -> int:
             return len(self.text)
         return min(self.line_offsets[line - 1] + max(column, 0), len(self.text))
 
+    def position(self, offset: int) -> tuple[int, int]:
+        """Return the (1-based line, 0-based column) of a character offset."""
+        clamped = min(max(offset, 0), len(self.text))
+        line = bisect.bisect_right(self.line_offsets, clamped)
+        return line, clamped - self.line_offsets[line - 1]
+
 
 def _next_token(code: str, pos: int, end: int) -> str:
     """Return the next token at or after ``pos``, skipping whitespace."""
@@ -291,13 +323,220 @@ def _boundary_scan_start(
     return name_end
 
 
+# Top-level commands replayed verbatim as scoping/notation context by the
+# minimal-file builder. Anything else at top level is either a declaration
+# (sliced through its own range) or intentionally dropped (`example`,
+# `#eval`, module docstrings, ...).
+CONTEXT_KEYWORDS = frozenset(
+    {
+        "namespace",
+        "section",
+        "end",
+        "open",
+        "variable",
+        "universe",
+        "set_option",
+        "attribute",
+        "export",
+        "deriving",
+        "notation",
+        "notation3",
+        "macro",
+        "macro_rules",
+        "syntax",
+        "elab",
+        "elab_rules",
+        "declare_syntax_cat",
+        "binder_predicate",
+        "infix",
+        "infixl",
+        "infixr",
+        "prefix",
+        "postfix",
+    }
+)
+
+_IMPORT_RE = re.compile(r"^import\s+([\w.«»]+)", re.MULTILINE)
+
+
+@dataclass
+class ModuleSkeleton:
+    """Per-module facts the minimal-file builder needs.
+
+    ``external_imports`` — the module's non-pool imports (Mathlib etc.).
+    ``local_imports`` — the module's pool-internal imports (full names).
+    ``contexts`` — ``(line, text)`` of top-level context commands, in order.
+    ``mutual_spans`` — ``(start_line, end_line)`` of top-level ``mutual``
+    blocks; members must be emitted as one verbatim block.
+    ``prefix_blocks`` — ``(line, next_line, text)`` of bare
+    ``open/set_option … in`` blocks whose declaration starts at
+    ``next_line`` (Lean's declaration range excludes such prefixes).
+    """
+
+    external_imports: list[str]
+    local_imports: list[str]
+    contexts: list[tuple[int, str]]
+    mutual_spans: list[tuple[int, int]]
+    prefix_blocks: list[tuple[int, int, str]]
+
+
+def _block_starts(code: str) -> list[int]:
+    """Offsets of top-level command starts (column-0 non-blank characters)."""
+    starts = [0] if code and not code[0].isspace() else []
+    for i in range(1, len(code)):
+        if code[i - 1] == "\n" and not code[i].isspace() and code[i] != "\n":
+            starts.append(i)
+    return starts
+
+
+def _is_context_block(code: str, start: int, end: int) -> bool:
+    """Classify a top-level block as a replayable context command.
+
+    ``open``/``set_option`` (and modifier-prefixed forms) can also prefix a
+    declaration via ``... in``; those blocks belong to the declaration and
+    are excluded by checking where :func:`_strip_prefixes` lands.
+    """
+    token = _read_token(code, start, end)
+    if token in ("scoped", "local", "noncomputable"):
+        # `noncomputable section` opens a scope; `scoped notation` etc.
+        after = start + len(token)
+        while after < end and code[after] in " \t":
+            after += 1
+        token = _read_token(code, after, end)
+    if token == "deriving":
+        # `deriving instance Foo for Bar` is a standalone command, but a
+        # column-0 `deriving Foo` continuation of an inductive belongs to
+        # that declaration's range.
+        after = start + len(token)
+        while after < end and code[after] in " \t":
+            after += 1
+        return _read_token(code, after, end) == "instance"
+    if token in ("attribute", "variable") and _ends_with_in(code, start, end):
+        # `attribute [...] X in` / `variable … in` prefix the next declaration.
+        return False
+    if token not in CONTEXT_KEYWORDS:
+        return False
+    if token in ("open", "set_option"):
+        after_prefixes = _strip_prefixes(code, start, end)
+        keyword = _read_token(code, after_prefixes, end)
+        if keyword in DECLARATION_KEYWORDS:
+            return False
+        if after_prefixes >= end or not keyword:
+            # A bare `open … in` / `set_option … in` block is the prefix of a
+            # declaration starting at column 0 on the next line; the
+            # declaration's own range covers it.
+            return False
+    return True
+
+
+def _ends_with_in(code: str, start: int, end: int) -> bool:
+    """Does this block's code end with a top-level ``in`` token?"""
+    j = end
+    while j > start and code[j - 1] in " \t\r\n":
+        j -= 1
+    return (
+        j - start >= 2
+        and code[j - 2 : j] == "in"
+        and (j - 2 == start or not _ident_char(code[j - 3]))
+    )
+
+
+def _is_prefix_only_block(code: str, start: int, end: int) -> bool:
+    """Is this a bare ``open/set_option/attribute/variable … in`` prefix?"""
+    token = _read_token(code, start, end)
+    if token in ("attribute", "variable"):
+        return _ends_with_in(code, start, end)
+    if token not in ("open", "set_option"):
+        return False
+    after_prefixes = _strip_prefixes(code, start, end)
+    keyword = _read_token(code, after_prefixes, end)
+    return (after_prefixes >= end or not keyword) and _IN_RE.search(
+        code, start, end
+    ) is not None
+
+
+def module_skeleton(source: SourceFile) -> ModuleSkeleton:
+    """Scan a module for imports, context commands, and mutual blocks."""
+    code = source.code
+    # Comments blanked but strings kept: used to trim trailing comments off a
+    # command without eating a final string literal (e.g. an `elab` command
+    # ending in an error message).
+    comment_view = code_view(source.text, blank_strings=False)
+    starts = _block_starts(code)
+    all_imports = _IMPORT_RE.findall(code)
+    external_imports = [
+        module
+        for module in all_imports
+        if not (module == "LeanPool" or module.startswith("LeanPool."))
+    ]
+    local_imports = [module for module in all_imports if module.startswith("LeanPool.")]
+    contexts: list[tuple[int, str]] = []
+    mutual_spans: list[tuple[int, int]] = []
+    prefix_blocks: list[tuple[int, int, str]] = []
+    skip_until = -1
+    for index, start in enumerate(starts):
+        end = starts[index + 1] if index + 1 < len(starts) else len(code)
+        if start < skip_until:
+            continue
+        first = _read_token(code, start, end)
+        if first == "import":
+            continue
+        if _is_prefix_only_block(code, start, end):
+            line, _ = source.position(start)
+            next_line = (
+                source.position(starts[index + 1])[0]
+                if index + 1 < len(starts)
+                else line + 1
+            )
+            code_end = end
+            while code_end > start and comment_view[code_end - 1] in " \t\r\n":
+                code_end -= 1
+            prefix_blocks.append(
+                (line, next_line, source.text[start:code_end].rstrip())
+            )
+            continue
+        if first == "mutual":
+            # The block ends at the next column-0 command, which is the
+            # matching bare `end`; fold it into the span and skip it.
+            close_end = end
+            if index + 1 < len(starts):
+                next_start = starts[index + 1]
+                next_end = starts[index + 2] if index + 2 < len(starts) else len(code)
+                if _read_token(code, next_start, next_end) == "end":
+                    close_end = next_end
+                    skip_until = next_end
+            start_line, _ = source.position(start)
+            last = close_end
+            while last > start and comment_view[last - 1] in " \t\r\n":
+                last -= 1
+            end_line, _ = source.position(max(last - 1, start))
+            mutual_spans.append((start_line, end_line))
+            continue
+        if _is_context_block(code, start, end):
+            line, _ = source.position(start)
+            # Cut at the last code character: the raw block otherwise runs to
+            # the next command and swallows a following declaration's doc
+            # comment (blanked in the comment view, so invisible to the scan).
+            code_end = end
+            while code_end > start and comment_view[code_end - 1] in " \t\r\n":
+                code_end -= 1
+            contexts.append((line, source.text[start:code_end].rstrip()))
+    return ModuleSkeleton(
+        external_imports=external_imports,
+        local_imports=local_imports,
+        contexts=contexts,
+        mutual_spans=mutual_spans,
+        prefix_blocks=prefix_blocks,
+    )
+
+
 def statement_slice(
     source: SourceFile,
     declaration_range: Sequence[int],
     selection: Sequence[int],
     fallback_kind: str,
-) -> tuple[str, str]:
-    """Return ``(kind, statement)`` for one declaration.
+) -> tuple[str, str, tuple[int, int] | None]:
+    """Return ``(kind, statement, statement_end)`` for one declaration.
 
     ``declaration_range`` is ``[startLine, startCol, endLine, endCol]`` with
     1-based lines; ``selection`` is the ``[line, col]`` of the name token.
@@ -305,11 +544,15 @@ def statement_slice(
     (``class inductive`` reports ``class``), else ``fallback_kind``. The
     statement is original source from the keyword to the body boundary,
     trimmed only at the edges and capped at 1200 characters.
+    ``statement_end`` is the boundary's ``(line, column)`` in the file —
+    where the body (``:=`` / ``where`` / ``|`` arms) begins — or ``None``
+    when the range points at a mid-line generated token; the minimal-file
+    builder cuts theorem statements there before appending ``:= sorry``.
     """
     start = source.offset(declaration_range[0], declaration_range[1])
     end = source.offset(declaration_range[2], declaration_range[3])
     if end <= start:
-        return fallback_kind, ""
+        return fallback_kind, "", None
     code = source.code
     keyword_position = _strip_prefixes(code, start, end)
     keyword = _read_token(code, keyword_position, end)
@@ -320,7 +563,7 @@ def statement_slice(
         # token; slicing from there yields a meaningless fragment.
         line_start = source.line_offsets[declaration_range[0] - 1]
         if source.text[line_start:start].strip():
-            return fallback_kind, ""
+            return fallback_kind, "", None
     inductive_like = keyword == "inductive" or (
         keyword == "class"
         and _next_token(code, keyword_position + len(keyword), end) == "inductive"
@@ -332,4 +575,4 @@ def statement_slice(
     statement = source.text[keyword_position:boundary].strip()
     if len(statement) > STATEMENT_CHARACTER_LIMIT:
         statement = statement[: STATEMENT_CHARACTER_LIMIT - 1].rstrip() + "…"
-    return kind, statement
+    return kind, statement, source.position(boundary)
diff --git a/python/lean_pool/exposition/static/assets/graph.js b/python/lean_pool/exposition/static/assets/graph.js
index 9d3e636f19..81debd56d5 100644
--- a/python/lean_pool/exposition/static/assets/graph.js
+++ b/python/lean_pool/exposition/static/assets/graph.js
@@ -123,6 +123,8 @@
   let searchQuery = '';
   let mainIds = []; // node ids flagged as main results (card metadata)
   let mainInformal = {}; // node id -> informal statement from the card
+  let rawShard = null; // full shard JSON (minimal-file builder input)
+  const moduleSources = {}; // module index -> fetched raw source text
 
   let fullView = null;
   let coneView = null;
@@ -685,6 +687,12 @@
       setHash('cone=' + id);
     });
     actions.appendChild(coneBtn);
+    const minimalBtn = elWith('button', 'btn', 'Minimal Lean file');
+    minimalBtn.type = 'button';
+    minimalBtn.addEventListener('click', () => {
+      openMinimalFile(id, minimalBtn);
+    });
+    actions.appendChild(minimalBtn);
     panelBodyEl.appendChild(actions);
 
     if (d.doc) {
@@ -1318,6 +1326,7 @@
   }
 
   function initData(json) {
+    rawShard = json;
     decls = Array.isArray(json.decls) ? json.decls : [];
     modules = Array.isArray(json.modules) ? json.modules : [];
     N = decls.length;
@@ -1413,6 +1422,239 @@
       });
   }
 
+  // ----- minimal Lean file --------------------------------------------------------
+
+  const RAW_BASE = 'https://raw.githubusercontent.com/Vilin97/lean-pool/';
+  const PLAYGROUND_URL_LIMIT = 128000; // characters; beyond this, download only
+
+  function fetchModuleSource(moduleIndex) {
+    if (moduleSources[moduleIndex] !== undefined) {
+      return Promise.resolve(moduleSources[moduleIndex]);
+    }
+    const path = modules[moduleIndex].split('.').join('/') + '.lean';
+    const commit = (rawShard && rawShard.commit) || 'main';
+    return fetch(RAW_BASE + encodeURIComponent(commit) + '/' + path)
+      .then((response) => {
+        if (!response.ok) throw new Error('HTTP ' + response.status);
+        return response.text();
+      })
+      .then((text) => {
+        moduleSources[moduleIndex] = text;
+        return text;
+      });
+  }
+
+  // LZ-string `compressToBase64` (with `=` padding stripped) — exactly what
+  // the Lean playground's #codez= fragment expects (see lean4web
+  // client/src/editor/code-atoms.ts). Algorithm by Pieroxy, MIT.
+  function lzCompress(input) {
+    const keyStrBase64 =
+      'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/';
+    if (input == null || input === '') return '';
+    const bitsPerChar = 6;
+    const dictionary = {};
+    const dictionaryToCreate = {};
+    let wc = '';
+    let w = '';
+    let enlargeIn = 2;
+    let dictSize = 3;
+    let numBits = 2;
+    const data = [];
+    let dataVal = 0;
+    let dataPosition = 0;
+
+    const writeBit = (bit) => {
+      dataVal = (dataVal << 1) | bit;
+      if (dataPosition === bitsPerChar - 1) {
+        dataPosition = 0;
+        data.push(keyStrBase64.charAt(dataVal));
+        dataVal = 0;
+      } else {
+        dataPosition++;
+      }
+    };
+    const writeBits = (numberOfBits, value) => {
+      for (let i = 0; i < numberOfBits; i++) {
+        writeBit(value & 1);
+        value >>= 1;
+      }
+    };
+    const decrementEnlarge = () => {
+      enlargeIn--;
+      if (enlargeIn === 0) {
+        enlargeIn = Math.pow(2, numBits);
+        numBits++;
+      }
+    };
+    const produceW = () => {
+      if (Object.prototype.hasOwnProperty.call(dictionaryToCreate, w)) {
+        const first = w.charCodeAt(0);
+        if (first < 256) {
+          writeBits(numBits, 0);
+          writeBits(8, first);
+        } else {
+          writeBits(numBits, 1);
+          writeBits(16, first);
+        }
+        decrementEnlarge();
+        delete dictionaryToCreate[w];
+      } else {
+        writeBits(numBits, dictionary[w]);
+      }
+      decrementEnlarge();
+    };
+
+    for (let ii = 0; ii < input.length; ii++) {
+      const c = input.charAt(ii);
+      if (!Object.prototype.hasOwnProperty.call(dictionary, c)) {
+        dictionary[c] = dictSize++;
+        dictionaryToCreate[c] = true;
+      }
+      wc = w + c;
+      if (Object.prototype.hasOwnProperty.call(dictionary, wc)) {
+        w = wc;
+      } else {
+        produceW();
+        dictionary[wc] = dictSize++;
+        w = String(c);
+      }
+    }
+    if (w !== '') produceW();
+    writeBits(numBits, 2); // end-of-stream token
+    // Flush the last partial character.
+    for (;;) {
+      dataVal <<= 1;
+      if (dataPosition === bitsPerChar - 1) {
+        data.push(keyStrBase64.charAt(dataVal));
+        break;
+      }
+      dataPosition++;
+    }
+    return data.join('');
+  }
+
+  function minimalModal() {
+    let modal = byId('minimal-modal');
+    if (modal) return modal;
+    modal = elWith('div', 'minimal-modal', null);
+    modal.id = 'minimal-modal';
+    modal.addEventListener('click', (event) => {
+      if (event.target === modal) modal.hidden = true;
+    });
+    const box = elWith('div', 'minimal-box', null);
+    const bar = elWith('div', 'minimal-bar', null);
+    bar.appendChild(elWith('span', 'minimal-title', null)).id = 'minimal-title';
+    const close = elWith('button', 'panel-close', '×');
+    close.type = 'button';
+    close.addEventListener('click', () => { modal.hidden = true; });
+    bar.appendChild(close);
+    box.appendChild(bar);
+    const meta = elWith('div', 'minimal-meta', null);
+    meta.id = 'minimal-meta';
+    box.appendChild(meta);
+    const actions = elWith('div', 'minimal-actions', null);
+    actions.id = 'minimal-actions';
+    box.appendChild(actions);
+    const pre = elWith('pre', 'minimal-code', null);
+    pre.id = 'minimal-code';
+    box.appendChild(pre);
+    modal.appendChild(box);
+    document.body.appendChild(modal);
+    return modal;
+  }
+
+  function showMinimalResult(node, result) {
+    const modal = minimalModal();
+    byId('minimal-title').textContent = 'Minimal Lean file · ' + node.name;
+    const meta = byId('minimal-meta');
+    const kb = (result.text.length / 1024).toFixed(1);
+    let summary = result.declarationCount + ' declarations from '
+      + result.moduleCount + ' module' + (result.moduleCount === 1 ? '' : 's')
+      + ' · ' + kb + ' KB';
+    if (result.missingHost.length > 0) {
+      summary += ' · ' + result.missingHost.length
+        + ' generated dependenc' + (result.missingHost.length === 1 ? 'y' : 'ies')
+        + ' could not be inlined';
+    }
+    meta.textContent = summary;
+    const actions = byId('minimal-actions');
+    actions.textContent = '';
+
+    const compressed = lzCompress(result.text);
+    const playgroundUrl = 'https://live.lean-lang.org/#codez=' + compressed;
+    if (playgroundUrl.length <= PLAYGROUND_URL_LIMIT) {
+      const open = elWith('a', 'btn btn-accent', 'Open in Lean playground');
+      open.href = playgroundUrl;
+      open.target = '_blank';
+      open.rel = 'noopener';
+      actions.appendChild(open);
+    } else {
+      const note = elWith('span', 'minimal-note',
+        'Too large for a playground link — download instead.');
+      actions.appendChild(note);
+    }
+
+    const download = elWith('a', 'btn', 'Download .lean');
+    const blob = new Blob([result.text], { type: 'text/plain;charset=utf-8' });
+    download.href = URL.createObjectURL(blob);
+    download.download = node.name.replace(/[^\w.']/g, '_') + '.lean';
+    actions.appendChild(download);
+
+    const copy = elWith('button', 'btn', 'Copy');
+    copy.type = 'button';
+    copy.addEventListener('click', () => {
+      navigator.clipboard.writeText(result.text).then(() => {
+        copy.textContent = 'Copied';
+        setTimeout(() => { copy.textContent = 'Copy'; }, 1200);
+      });
+    });
+    actions.appendChild(copy);
+
+    byId('minimal-code').textContent = result.text;
+    modal.hidden = false;
+  }
+
+  function openMinimalFile(id, button) {
+    if (!rawShard || !window.ExpoMinimal) return;
+    const previous = button.textContent;
+    button.disabled = true;
+    button.textContent = 'Building…';
+    const cone = window.ExpoMinimal.coneIds(rawShard, id);
+    const needed = new Set();
+    for (const nodeId of cone.ids) needed.add(decls[nodeId].module);
+    const buildOnceFetched = (attempt) =>
+      Promise.all(Array.from(needed).map(fetchModuleSource)).then(() => {
+        const result = window.ExpoMinimal.build(rawShard, moduleSources, id);
+        if (result.pending && attempt < 4) {
+          // The tactic-reference closure pulled in declarations from
+          // modules we have not fetched yet.
+          for (const moduleIndex of result.pending) needed.add(moduleIndex);
+          return buildOnceFetched(attempt + 1);
+        }
+        return result;
+      });
+    buildOnceFetched(0)
+      .then((result) => {
+        if (result.pending) {
+          throw new Error('could not resolve all module sources');
+        }
+        showMinimalResult(decls[id], result);
+      })
+      .catch((error) => {
+        const modal = minimalModal();
+        byId('minimal-title').textContent = 'Minimal Lean file';
+        byId('minimal-meta').textContent =
+          'Could not fetch project sources (' + error.message + ').';
+        byId('minimal-actions').textContent = '';
+        byId('minimal-code').textContent = '';
+        modal.hidden = false;
+      })
+      .finally(() => {
+        button.disabled = false;
+        button.textContent = previous;
+      });
+  }
+
   // ----- boot ---------------------------------------------------------------------
 
   readTheme();
diff --git a/python/lean_pool/exposition/static/assets/minimal.js b/python/lean_pool/exposition/static/assets/minimal.js
new file mode 100644
index 0000000000..63b00c293d
--- /dev/null
+++ b/python/lean_pool/exposition/static/assets/minimal.js
@@ -0,0 +1,540 @@
+/* Minimal Lean file builder for the Lean Pool exposition.
+ *
+ * Pure logic, no DOM: exposed as window.ExpoMinimal so graph.js (browser)
+ * and the validation harness (node) share the exact same code paths.
+ *
+ * Given a project shard, the raw text of the involved modules, and a target
+ * declaration id, `build` assembles a standalone .lean file: the union of
+ * the involved modules' external imports, then each module replayed in
+ * original order — top-level context commands (namespace/section/open/
+ * variable/notation/...) kept verbatim, needed definitions copied verbatim,
+ * needed theorems cut at their statement boundary with `:= sorry` — the
+ * whole module wrapped in a `section` so its `variable`s stay local.
+ *
+ * The dependency cone follows statement-only deps (`tdeps`) through
+ * theorems (their proofs become `sorry`) and full deps through everything
+ * else (bodies are kept). Generated declarations (deriving/@[simps]/...)
+ * are represented by their host declaration's source.
+ */
+(function (root) {
+  "use strict";
+
+  var PROOF_KINDS = { theorem: true, lemma: true };
+
+  function isProofKind(kind) {
+    return PROOF_KINDS[kind] === true;
+  }
+
+  /* Walk the dependency closure from `seeds`, accumulating into
+   * `state = {seen, included, missingHost}`; generated declarations are
+   * replaced by their hosts. */
+  function walkCone(shard, seeds, state) {
+    var decls = shard.decls;
+    var stack = seeds.slice();
+    while (stack.length > 0) {
+      var id = stack.pop();
+      var node = decls[id];
+      if (!node) continue;
+      if (typeof node.host === "number") {
+        id = node.host;
+        node = decls[id];
+        if (!node) continue;
+      } else if (node.statement === "" && node.stmtEnd === undefined) {
+        // Generated declaration without a source host: cannot be emitted.
+        if (!state.seen["m" + id]) {
+          state.seen["m" + id] = true;
+          state.missingHost.push(id);
+        }
+        continue;
+      }
+      if (state.seen[id]) continue;
+      state.seen[id] = true;
+      state.included.push(id);
+      var deps = declDeps(node);
+      for (var i = 0; i < deps.length; i++) stack.push(deps[i]);
+    }
+  }
+
+  /* Dependency cone for the minimal file. Returns shard-local ids, with
+   * generated declarations replaced by their hosts. */
+  function coneIds(shard, targetId) {
+    var state = { seen: {}, included: [], missingHost: [] };
+    walkCone(shard, [targetId], state);
+    state.included.sort(function (a, b) { return a - b; });
+    return { ids: state.included, missingHost: state.missingHost };
+  }
+
+  /* Dependencies to follow for a node. Theorems contribute statement-only
+   * deps (their proofs become `sorry`) — EXCEPT mutual-block members
+   * (span): the whole block is emitted verbatim, proofs included, so their
+   * full dependencies are needed. */
+  function declDeps(node) {
+    if (node.span) return node.deps;
+    return isProofKind(node.kind) && node.tdeps ? node.tdeps : node.deps;
+  }
+
+  /* Involved modules in emission order: the cone's modules closed under
+   * same-project imports (`moduleData.uses` — pulls in notation-only files
+   * whose context commands the cone's statements may rely on), ordered
+   * dependencies-first along the import DAG; ties keep module index order. */
+  function moduleOrder(shard, ids) {
+    var decls = shard.decls;
+    var moduleData = shard.moduleData || [];
+    var involved = {};
+    var queue = [];
+    var i;
+    for (i = 0; i < ids.length; i++) {
+      var moduleIndex = decls[ids[i]].module;
+      if (!involved[moduleIndex]) {
+        involved[moduleIndex] = true;
+        queue.push(moduleIndex);
+      }
+    }
+    while (queue.length > 0) {
+      var current = queue.pop();
+      var uses = (moduleData[current] || {}).uses || [];
+      for (var j = 0; j < uses.length; j++) {
+        if (!involved[uses[j]]) {
+          involved[uses[j]] = true;
+          queue.push(uses[j]);
+        }
+      }
+    }
+    var moduleList = Object.keys(involved).map(Number).sort(function (a, b) {
+      return a - b;
+    });
+    var placed = {};
+    var order = [];
+    function place(moduleIndex, depth) {
+      if (placed[moduleIndex] || depth > moduleList.length) return;
+      placed[moduleIndex] = true; // pre-mark: cycles fall back to index order
+      var needs = ((moduleData[moduleIndex] || {}).uses || [])
+        .filter(function (m) { return involved[m]; });
+      for (var k = 0; k < needs.length; k++) place(needs[k], depth + 1);
+      order.push(moduleIndex);
+    }
+    for (i = 0; i < moduleList.length; i++) place(moduleList[i], 0);
+    return order;
+  }
+
+  /* Slice a UTF-16 string prefix of `codepoints` Unicode code points. */
+  function codePointPrefix(line, codepoints) {
+    var index = 0;
+    var count = 0;
+    while (index < line.length && count < codepoints) {
+      var code = line.codePointAt(index);
+      index += code > 0xffff ? 2 : 1;
+      count += 1;
+    }
+    return line.slice(0, index);
+  }
+
+  function declText(node, lines) {
+    var startLine = node.line;
+    var endLine = node.endLine;
+    var prefix = "";
+    if (node.prefix) {
+      // Drop `attribute [custom] X in` prefix lines whose attribute cannot
+      // be replayed; keep open/set_option/variable prefixes.
+      var prefixLines = node.prefix.split("\n").filter(function (line) {
+        var attr = line.match(/^\s*attribute\s*\[([^\]]*)\]/);
+        return !(attr && hasUnknownAttribute(attr[1]));
+      });
+      if (prefixLines.length > 0) prefix = prefixLines.join("\n") + "\n";
+    }
+    if (node.span) {
+      startLine = node.span[0];
+      endLine = node.span[1];
+      prefix = "";
+    } else if (isProofKind(node.kind) && node.stmtEnd) {
+      var upto = lines.slice(startLine - 1, node.stmtEnd[0] - 1);
+      var boundaryLine = lines[node.stmtEnd[0] - 1] || "";
+      upto.push(codePointPrefix(boundaryLine, node.stmtEnd[1]));
+      var statement = upto.join("\n").replace(/\s+$/, "");
+      return sanitizeAttributes(prefix + statement) + " := sorry";
+    }
+    return sanitizeAttributes(
+      prefix + lines.slice(startLine - 1, endLine).join("\n").replace(/\s+$/, ""));
+  }
+
+  /* Identifier-ish tokens of a command text (used for context pruning). */
+  function identTokens(text) {
+    return text.match(/[A-Za-z_À-￿][\w.'À-￿]*/g) || [];
+  }
+
+  /* Attributes whose registrations ship with Lean/Mathlib. An `attribute`
+   * context using anything else (a project-registered attribute) cannot be
+   * replayed, since the registering command is not a context. */
+  var KNOWN_ATTRIBUTES = {
+    simp: 1, instance: 1, ext: 1, norm_cast: 1, push_cast: 1, coe: 1,
+    reducible: 1, semireducible: 1, irreducible: 1, inline: 1, specialize: 1,
+    simps: 1, mono: 1, positivity: 1, gcongr: 1, fun_prop: 1,
+    measurability: 1, continuity: 1, aesop: 1, refl: 1, symm: 1, trans: 1,
+    congr: 1, to_additive: 1, default_instance: 1, match_pattern: 1,
+    class: 1, induction_eliminator: 1, cases_eliminator: 1, elab_as_elim: 1,
+    pp_nodot: 1, grind: 1, norm_num: 1, local: 1, scoped: 1, nolint: 1,
+    deprecated: 1, simp_nf: 1, higher_order: 1,
+  };
+
+  /* Index the project's declaration names for token matching.
+   * `strict` — full names plus dotted suffixes at component boundaries
+   * (`DeMorgan.verum` ~ `LO.DeMorgan.verum`); bare single-component tokens
+   * only match single-component names, since matching them against last
+   * components would misfire on Mathlib homonyms. Used for pruning.
+   * `loose` — additionally last components (`coprodTree_node` ~
+   * `CK.coprodTree_node`). Used for tactic-reference closure, where the
+   * bracket list is known to name lemmas. */
+  function makeNameMatcher(shard) {
+    var strict = {}; // token -> [decl ids]
+    var loose = {};
+    function record(map, key, id) {
+      (map[key] = map[key] || []).push(id);
+    }
+    for (var d = 0; d < shard.decls.length; d++) {
+      var parts = shard.decls[d].name.split(".");
+      for (var p = 0; p < parts.length; p++) {
+        var suffix = parts.slice(p).join(".");
+        if (p === 0 || p < parts.length - 1) record(strict, suffix, d);
+        record(loose, suffix, d);
+      }
+    }
+    return { strict: strict, loose: loose };
+  }
+
+  /* Decide whether a context command survives into the minimal file.
+   * - `variable`/`attribute` commands mentioning project declarations
+   *   outside the cone are dropped (safe: a section variable actually used
+   *   by an emitted declaration only mentions cone declarations — they
+   *   appear in its statement's dependencies).
+   * - `attribute` commands using non-builtin attribute names are dropped
+   *   (their registration command cannot be replayed).
+   * - `export NS (a b …)` is dropped when `NS.a` … resolve outside the
+   *   cone. */
+  /* Does an `@[...]` entry list contain a non-builtin attribute name? */
+  function hasUnknownAttribute(inner) {
+    var entries = inner.split(",");
+    for (var e = 0; e < entries.length; e++) {
+      var words = identTokens(entries[e].replace(/^[\s\-↓↑]+/, ""));
+      var attrName = words[0] === "local" || words[0] === "scoped"
+        ? words[1] : words[0];
+      if (attrName && !KNOWN_ATTRIBUTES[attrName]) return true;
+    }
+    return false;
+  }
+
+  /* Drop non-builtin attributes from emitted declaration text: their
+   * registering command cannot be replayed, so `@[simp_isPosition]` would
+   * fail with "unknown attribute". */
+  function sanitizeAttributes(text) {
+    return text.replace(/@\[([^[\]]*)\]\s*/g, function (whole, inner) {
+      var kept = inner.split(",").filter(function (entry) {
+        return !hasUnknownAttribute(entry);
+      });
+      if (kept.length === 0) return "";
+      if (kept.length === inner.split(",").length) return whole;
+      return "@[" + kept.join(",").trim() + "] ";
+    });
+  }
+
+  function makeContextPruner(matcher, seen) {
+    function outOnlyIds(ids) {
+      if (!ids) return false;
+      for (var k = 0; k < ids.length; k++) {
+        if (seen[ids[k]]) return false;
+      }
+      return true;
+    }
+    /* nsPrefixes: enclosing namespace joins, innermost last. parentFallback:
+     * for reference lists (attribute/export args) a dotted token whose full
+     * name is unknown may be a structure/class projection — resolve its
+     * parent instead. */
+    function mentionsOutOnly(tokens, nsPrefixes, parentFallback) {
+      for (var t = 0; t < tokens.length; t++) {
+        var token = tokens[t];
+        var ids = matcher.strict[token];
+        if (!ids && nsPrefixes) {
+          for (var p = nsPrefixes.length - 1; p >= 0 && !ids; p--) {
+            ids = matcher.strict[nsPrefixes[p] + "." + token];
+          }
+        }
+        if (!ids && parentFallback && token.indexOf(".") >= 0) {
+          var parent = token.slice(0, token.lastIndexOf("."));
+          ids = matcher.loose[parent];
+        }
+        if (ids && outOnlyIds(ids)) return true;
+      }
+      return false;
+    }
+    return function keepContext(text, nsPrefixes) {
+      var exportMatch = text.match(
+        /^\s*export\s+([\w.'À-￿]+)\s*\(([^)]*)\)/);
+      if (exportMatch) {
+        var namespacePath = exportMatch[1];
+        var members = identTokens(exportMatch[2]);
+        var qualified = members.map(function (member) {
+          return namespacePath + "." + member;
+        });
+        // The namespace itself resolving out-of-cone also prunes (it may
+        // not even exist in the file without its declarations).
+        qualified.push(namespacePath);
+        return !mentionsOutOnly(qualified, nsPrefixes, true);
+      }
+      var attributeMatch = text.match(
+        /^\s*(?:scoped\s+|local\s+)?attribute\s*\[([^\]]*)\]/);
+      if (attributeMatch) {
+        if (hasUnknownAttribute(attributeMatch[1])) return false;
+        return !mentionsOutOnly(identTokens(text), nsPrefixes, true);
+      }
+      if (/^\s*(?:scoped\s+|local\s+)?variable\b/.test(text)) {
+        return !mentionsOutOnly(identTokens(text), nsPrefixes, false);
+      }
+      return true;
+    };
+  }
+
+  /* Track `namespace`/`section`/`end` context commands to know the
+   * enclosing namespace path at each point of a module replay. */
+  function updateNamespaceStack(stack, text) {
+    var ns = text.match(/^\s*namespace\s+([\w.'À-￿]+)/);
+    if (ns) {
+      stack.push(ns[1]);
+      return;
+    }
+    if (/^\s*(?:noncomputable\s+)?section\b/.test(text)) {
+      stack.push(null); // section: no namespace component
+      return;
+    }
+    if (/^\s*end\b/.test(text)) stack.pop();
+  }
+
+  function namespacePrefixes(stack) {
+    var prefixes = [];
+    var current = "";
+    for (var i = 0; i < stack.length; i++) {
+      if (stack[i] === null) continue;
+      current = current ? current + "." + stack[i] : stack[i];
+      prefixes.push(current);
+    }
+    return prefixes;
+  }
+
+  /* Namespaces mentioned by kept `open` commands; stubbed up front so the
+   * opens resolve even when nothing from that namespace is emitted. */
+  function openedNamespaces(contextTexts) {
+    var found = [];
+    var seen = {};
+    for (var i = 0; i < contextTexts.length; i++) {
+      var text = contextTexts[i];
+      if (!/^\s*(?:scoped\s+|local\s+)?open\b/.test(text)) continue;
+      var body = text.replace(/^\s*(?:scoped\s+|local\s+)?open\b/, "")
+        .replace(/\([^)]*\)/g, " ");
+      var tokens = body.split(/\s+/);
+      for (var j = 0; j < tokens.length; j++) {
+        var token = tokens[j];
+        if (!token || token === "scoped" || token === "hiding"
+            || token === "renaming" || token === "in") continue;
+        // Namespaces open with a capitalized or dotted path; anything else
+        // (prose, keywords, operators) must not become a stub.
+        if (!/^[A-Z\u00c0-\uffff][\w.'\u00c0-\uffff]*$/.test(token)
+            && token.indexOf(".") === -1) continue;
+        if (!/^[A-Za-z_\u00c0-\uffff][\w.'\u00c0-\uffff]*$/.test(token)) continue;
+        if (!seen[token]) {
+          seen[token] = true;
+          found.push(token);
+        }
+      }
+    }
+    return found;
+  }
+
+  /* Lemma references named in tactic bracket lists of an emitted body.
+   * `simp only [foo]` applies rfl-lemmas definitionally, leaving no
+   * constant in the proof term, so the recorded dependencies miss them;
+   * the bracket list is the only trace. */
+  function tacticReferences(text) {
+    var refs = [];
+    var pattern =
+      /\b(?:simp_all|simp_rw|simp|rw|rewrite|unfold|dsimp)\s+(?:only\s+)?\[([^\]]*)\]/g;
+    var match;
+    while ((match = pattern.exec(text)) !== null) {
+      var tokens = identTokens(match[1]);
+      for (var i = 0; i < tokens.length; i++) refs.push(tokens[i]);
+    }
+    return refs;
+  }
+
+  var TACTIC_MATCH_CAP = 5; // ambiguous tokens (many homonyms) are skipped
+
+  /* Grow the cone with declarations named in emitted bodies' tactic lists.
+   * Mutates `state`; returns module indices whose sources are still needed
+   * (the caller fetches them and calls build again). */
+  function expandTacticReferences(shard, sources, state, matcher, linesFor) {
+    var decls = shard.decls;
+    var pending = {};
+    for (var round = 0; round < 4; round++) {
+      var changed = false;
+      var idsNow = state.included.slice();
+      for (var i = 0; i < idsNow.length; i++) {
+        var node = decls[idsNow[i]];
+        if (isProofKind(node.kind) && !node.span) continue; // body sorried
+        if (sources[node.module] === undefined) {
+          pending[node.module] = true;
+          continue;
+        }
+        var refs = tacticReferences(declText(node, linesFor(node.module)));
+        for (var r = 0; r < refs.length; r++) {
+          var candidates = matcher.loose[refs[r]];
+          if (!candidates || candidates.length > TACTIC_MATCH_CAP) continue;
+          var anyCone = false;
+          var c;
+          for (c = 0; c < candidates.length; c++) {
+            if (state.seen[candidates[c]]) { anyCone = true; break; }
+          }
+          if (anyCone) continue;
+          for (c = 0; c < candidates.length; c++) {
+            walkCone(shard, [candidates[c]], state);
+            changed = true;
+          }
+        }
+      }
+      if (!changed) break;
+    }
+    for (var j = 0; j < state.included.length; j++) {
+      var moduleIndex = decls[state.included[j]].module;
+      if (sources[moduleIndex] === undefined) pending[moduleIndex] = true;
+    }
+    return Object.keys(pending).map(Number);
+  }
+
+  /* Assemble the minimal file.
+   * shard: the project shard JSON.
+   * sources: object mapping module index -> raw module text.
+   * targetId: shard-local declaration id.
+   * Returns {pending: [moduleIndex…]} when more sources are required.
+   */
+  function build(shard, sources, targetId) {
+    var decls = shard.decls;
+    var linesCache = {};
+    function linesFor(moduleIndex) {
+      if (!linesCache[moduleIndex]) {
+        linesCache[moduleIndex] = (sources[moduleIndex] || "").split("\n");
+      }
+      return linesCache[moduleIndex];
+    }
+    var state = { seen: {}, included: [], missingHost: [] };
+    walkCone(shard, [targetId], state);
+    var matcher = makeNameMatcher(shard);
+    var stillNeeded = expandTacticReferences(
+      shard, sources, state, matcher, linesFor);
+    if (stillNeeded.length > 0) return { pending: stillNeeded };
+    var ids = state.included.slice().sort(function (a, b) { return a - b; });
+    var cone = { ids: ids, missingHost: state.missingHost };
+    var target = decls[targetId];
+    var byModule = {};
+    var i;
+    for (i = 0; i < ids.length; i++) {
+      var node = decls[ids[i]];
+      (byModule[node.module] = byModule[node.module] || []).push(ids[i]);
+    }
+    var order = moduleOrder(shard, ids);
+
+    var keepContext = makeContextPruner(matcher, state.seen);
+    var imports = {};
+    var allContexts = [];
+    var keptContextsByModule = {};
+    for (i = 0; i < order.length; i++) {
+      var moduleData = (shard.moduleData || [])[order[i]] || {};
+      (moduleData.imports || []).forEach(function (name) {
+        imports[name] = true;
+      });
+      var nsStack = [];
+      var kept = [];
+      (moduleData.contexts || []).forEach(function (entry) {
+        if (keepContext(entry[1], namespacePrefixes(nsStack))) {
+          kept.push(entry);
+          allContexts.push(entry[1]);
+        }
+        updateNamespaceStack(nsStack, entry[1]);
+      });
+      keptContextsByModule[order[i]] = kept;
+    }
+    var importList = Object.keys(imports).sort();
+    if (importList.length === 0) importList = ["Mathlib"];
+
+    var out = [];
+    out.push("/- Minimal Lean file for `" + target.name + "`.");
+    out.push("Extracted from the Lean Pool project `" + shard.project
+      + "` (commit " + String(shard.commit || "main").slice(0, 12) + ").");
+    out.push("Definitions keep their bodies; theorem proofs are replaced by"
+      + " `sorry`.");
+    out.push("Auto-generated by the Lean Pool exposition — may need minor"
+      + " adjustments. -/");
+    out.push("");
+    for (i = 0; i < importList.length; i++) out.push("import " + importList[i]);
+    out.push("");
+    out.push("set_option quotPrecheck false");
+    out.push("set_option linter.all false");
+    out.push("");
+
+    var stubs = openedNamespaces(allContexts);
+    if (stubs.length > 0) {
+      out.push("-- Namespace stubs so later `open`s resolve.");
+      for (i = 0; i < stubs.length; i++) {
+        out.push("namespace " + stubs[i]);
+        out.push("end " + stubs[i]);
+      }
+      out.push("");
+    }
+
+    for (i = 0; i < order.length; i++) {
+      var moduleIndex = order[i];
+      var moduleName = shard.modules[moduleIndex];
+      var needed = (byModule[moduleIndex] || []).slice();
+      var keptContexts = keptContextsByModule[moduleIndex] || [];
+      // Context-only modules (no cone declarations) are replayed for their
+      // notation/attribute commands; skip them when nothing survives.
+      if (needed.length === 0 && keptContexts.length === 0) continue;
+      var source = sources[moduleIndex];
+      if (needed.length > 0 && source === undefined) continue;
+      var lines = source === undefined ? [] : source.split("\n");
+      var events = [];
+      var k;
+      for (k = 0; k < keptContexts.length; k++) {
+        events.push({ line: keptContexts[k][0], text: keptContexts[k][1] });
+      }
+      var emittedSpans = {};
+      for (k = 0; k < needed.length; k++) {
+        var entry = decls[needed[k]];
+        var spanKey = entry.span ? entry.span.join(":") : "d" + needed[k];
+        if (emittedSpans[spanKey]) continue;
+        emittedSpans[spanKey] = true;
+        events.push({
+          line: entry.span ? entry.span[0] : entry.line,
+          text: declText(entry, lines),
+        });
+      }
+      events.sort(function (a, b) { return a.line - b.line; });
+      out.push("-- ═══ " + moduleName + " ═══");
+      out.push("section");
+      for (k = 0; k < events.length; k++) {
+        out.push(events[k].text);
+        out.push("");
+      }
+      out.push("end");
+      out.push("");
+    }
+
+    return {
+      text: out.join("\n"),
+      declarationCount: ids.length,
+      moduleCount: order.length,
+      missingHost: cone.missingHost.map(function (id) {
+        return decls[id] ? decls[id].name : String(id);
+      }),
+    };
+  }
+
+  var api = { build: build, coneIds: coneIds, moduleOrder: moduleOrder };
+  if (typeof module !== "undefined" && module.exports) module.exports = api;
+  if (root) root.ExpoMinimal = api;
+})(typeof window !== "undefined" ? window : null);
diff --git a/python/lean_pool/exposition/static/assets/style.css b/python/lean_pool/exposition/static/assets/style.css
index 8087a7b44f..6b98528f96 100644
--- a/python/lean_pool/exposition/static/assets/style.css
+++ b/python/lean_pool/exposition/static/assets/style.css
@@ -382,6 +382,83 @@ a.main-result-name:hover {
   color: var(--muted);
 }
 
+/* minimal Lean file modal */
+
+.minimal-modal {
+  position: fixed;
+  inset: 0;
+  background: rgb(0 0 0 / 0.45);
+  display: flex;
+  align-items: center;
+  justify-content: center;
+  z-index: 40;
+  padding: 24px;
+}
+
+.minimal-box {
+  background: var(--card);
+  border: 1px solid var(--border);
+  border-radius: 8px;
+  box-shadow: 0 8px 32px rgb(0 0 0 / 0.25);
+  width: min(960px, 100%);
+  max-height: 86vh;
+  display: flex;
+  flex-direction: column;
+  padding: 14px 16px;
+  gap: 8px;
+}
+
+.minimal-bar {
+  display: flex;
+  align-items: center;
+  justify-content: space-between;
+  gap: 12px;
+}
+
+.minimal-title {
+  font-weight: 650;
+  font-family: var(--font-mono);
+  font-size: 14px;
+  overflow: hidden;
+  text-overflow: ellipsis;
+  white-space: nowrap;
+}
+
+.minimal-meta {
+  color: var(--muted);
+  font-size: 13px;
+}
+
+.minimal-actions {
+  display: flex;
+  align-items: center;
+  gap: 8px;
+  flex-wrap: wrap;
+}
+
+.minimal-actions a.btn {
+  text-decoration: none;
+}
+
+.minimal-note {
+  color: var(--muted);
+  font-size: 13px;
+}
+
+.minimal-code {
+  flex: 1;
+  overflow: auto;
+  margin: 0;
+  border: 1px solid var(--border);
+  border-radius: 6px;
+  padding: 10px 12px;
+  font-family: var(--font-mono);
+  font-size: 12.5px;
+  line-height: 1.5;
+  background: var(--bg);
+  white-space: pre;
+}
+
 .info-stats {
   color: var(--muted);
   font-size: 13px;
diff --git a/python/lean_pool/exposition/static/assets/viewer.js b/python/lean_pool/exposition/static/assets/viewer.js
index cffa2725f8..3a663576ed 100644
--- a/python/lean_pool/exposition/static/assets/viewer.js
+++ b/python/lean_pool/exposition/static/assets/viewer.js
@@ -42,6 +42,8 @@
   const sortedOrders = new Map(); // column name -> ascending Uint32Array
   let filtered = null;            // Uint32Array scratch; first filteredCount valid
   let filteredCount = 0;
+  let kindFacetCounts = null;     // Uint32Array: per-kind counts under project+search
+  let chipCountEls = [];          // kind index -> chip count element
 
   const state = {
     column: "name",
@@ -98,13 +100,17 @@
     const project = state.project;
     const kindActive = state.kindActive;
     const allKindsActive = kindActive.every(Boolean);
+    // Facet counts: per-kind totals under the project + search filters only,
+    // so the chips always show how many rows each kind toggle governs.
+    kindFacetCounts.fill(0);
     let n = 0;
     for (let j = 0; j < total; j++) {
       // Descending = walk the ascending order backwards (no array reversal).
       const i = order[descending ? total - 1 - j : j];
       if (project !== -1 && projectOf[i] !== project) continue;
-      if (!allKindsActive && !kindActive[kindOf[i]]) continue;
       if (hasQuery && lowerNames[i].indexOf(query) === -1) continue;
+      kindFacetCounts[kindOf[i]]++;
+      if (!allKindsActive && !kindActive[kindOf[i]]) continue;
       filtered[n++] = i;
     }
     filteredCount = n;
@@ -116,6 +122,7 @@
     emptyEl.hidden = filteredCount !== 0;
     countEl.textContent =
       `${formatCount(filteredCount)} of ${formatCount(total)} declarations`;
+    updateKindChipCounts();
     if (resetScroll) scroller.scrollTop = 0;
     renderWindow();
   }
@@ -212,6 +219,7 @@
       const count = document.createElement("span");
       count.className = "chip-count";
       count.textContent = formatCount(kindCounts[k]);
+      chipCountEls[k] = count;
       chip.append(label, count);
       chip.addEventListener("click", () => {
         state.kindActive[k] = !state.kindActive[k];
@@ -223,6 +231,14 @@
     }
   }
 
+  function updateKindChipCounts() {
+    for (let k = 0; k < chipCountEls.length; k++) {
+      if (chipCountEls[k]) {
+        chipCountEls[k].textContent = formatCount(kindFacetCounts[k]);
+      }
+    }
+  }
+
   function updateSortIndicators() {
     for (const button of headEl.querySelectorAll(".vsort")) {
       if (button.dataset.col === state.column) {
@@ -311,6 +327,8 @@
     }
     state.kindActive = new Array(kinds.length).fill(true);
     filtered = new Uint32Array(total);
+    kindFacetCounts = new Uint32Array(kinds.length);
+    chipCountEls = new Array(kinds.length).fill(null);
 
     buildProjectSelect();
     buildKindChips(kindCounts);
diff --git a/python/lean_pool/exposition/templates/project.html b/python/lean_pool/exposition/templates/project.html
index b1d31070d8..ddb3bc5b93 100644
--- a/python/lean_pool/exposition/templates/project.html
+++ b/python/lean_pool/exposition/templates/project.html
@@ -44,6 +44,7 @@ <h1 class="project-title" id="project-title">${TITLE}</h1>
       <div class="panel-body" id="panel-body"></div>
     </aside>
   </div>
+  <script src="../../assets/minimal.js"></script>
   <script src="../../assets/graph.js"></script>
 </body>
 </html>
diff --git a/python/tests/test_exposition_generate.py b/python/tests/test_exposition_generate.py
index bab704987e..7281a91f84 100644
--- a/python/tests/test_exposition_generate.py
+++ b/python/tests/test_exposition_generate.py
@@ -95,6 +95,7 @@ def a3 : Nat :=
         "r": [1, 0, 1, 26],
         "s": [1, 6],
         "deps": [],
+        "tdeps": [],
         "ext": 1,
     },
     {
@@ -198,15 +199,19 @@ def test_project_shard_schema_and_stats(site: tuple[Path, SiteSummary]) -> None:
     assert list(shard) == [
         "schema",
         "project",
+        "commit",
         "title",
         "provenance",
         "card",
         "mainResults",
         "stats",
         "modules",
+        "moduleData",
         "layers",
         "decls",
     ]
+    assert shard["commit"] == "deadbeef"
+    assert len(shard["moduleData"]) == len(shard["modules"])
     assert shard["schema"] == 1
     assert shard["project"] == "Alpha"
     assert shard["title"] == "Alpha & Co"
@@ -287,6 +292,10 @@ def test_declaration_nodes(site: tuple[Path, SiteSummary]) -> None:
         "order",
         "main",  # a3 is one of the card's main declarations
     ]
+    # a1 is a lemma: it carries the statement boundary and type-only deps.
+    assert alpha[0]["stmtEnd"] == [1, 16]  # the `:=` in `lemma a1 : True := …`
+    assert alpha[0]["tdeps"] == []
+    assert "stmtEnd" not in alpha[2]  # defs keep their bodies — no boundary field
     beta = _load(out, "data/projects/Beta.json")["decls"]
     b3 = beta[2]
     assert b3["full"] == "_private.LeanPool.Beta.0.b3"
@@ -300,6 +309,7 @@ def test_declaration_nodes(site: tuple[Path, SiteSummary]) -> None:
         "line",
         "endLine",
         "statement",
+        "stmtEnd",
         "private",
         "deps",
         "ext",
diff --git a/python/tests/test_exposition_source_text.py b/python/tests/test_exposition_source_text.py
index db0a753fef..19b48a2f99 100644
--- a/python/tests/test_exposition_source_text.py
+++ b/python/tests/test_exposition_source_text.py
@@ -2,7 +2,11 @@
 
 from __future__ import annotations
 
-from lean_pool.exposition.source_text import SourceFile, statement_slice
+from lean_pool.exposition.source_text import (
+    SourceFile,
+    module_skeleton,
+    statement_slice,
+)
 
 THEOREM_BLOCK = """\
 /-- Doc for foo. -/
@@ -19,16 +23,77 @@ def _slice(
     selection: list[int],
     fallback: str = "theorem",
 ) -> tuple[str, str]:
-    """Run statement_slice over freshly parsed source text."""
+    """Run statement_slice over freshly parsed source text (kind, statement)."""
+    kind, statement, _ = _slice_full(text, declaration_range, selection, fallback)
+    return kind, statement
+
+
+def _slice_full(
+    text: str,
+    declaration_range: list[int],
+    selection: list[int],
+    fallback: str = "theorem",
+) -> tuple[str, str, tuple[int, int] | None]:
+    """Run statement_slice over freshly parsed source text (full result)."""
     source = SourceFile.from_text(text)
     return statement_slice(source, declaration_range, selection, fallback)
 
 
 def test_theorem_with_assignment_boundary() -> None:
     """Doc comment, attribute, and modifier are skipped; body is cut at :=."""
-    kind, statement = _slice(THEOREM_BLOCK, [1, 0, 5, 6], [3, 16])
+    kind, statement, statement_end = _slice_full(THEOREM_BLOCK, [1, 0, 5, 6], [3, 16])
     assert kind == "theorem"
     assert statement == "theorem foo (n : Nat) :\n    n + 0 = n"
+    # The boundary sits at the `:=` on line 4, column 14 (0-based codepoints).
+    assert statement_end == (4, 14)
+
+
+def test_module_skeleton_contexts_imports_and_mutual() -> None:
+    """module_skeleton collects imports, context commands, and mutual spans."""
+    text = (
+        "import Mathlib.Order.Basic\n"
+        "import LeanPool.Other.Module\n"
+        "\n"
+        "/-! Module doc: skipped. -/\n"
+        "\n"
+        "namespace Demo\n"
+        "\n"
+        "open Finset in\n"
+        "theorem uses_prefix : True := trivial\n"
+        "\n"
+        "variable {n : Nat}\n"
+        "open Nat\n"
+        'notation "⟪" x "⟫" => id x\n'
+        "\n"
+        "mutual\n"
+        "  def even : Nat → Bool | 0 => true | n + 1 => odd n\n"
+        "  def odd : Nat → Bool | 0 => false | n + 1 => even n\n"
+        "end\n"
+        "\n"
+        "end Demo\n"
+    )
+    skeleton = module_skeleton(SourceFile.from_text(text))
+    assert skeleton.external_imports == ["Mathlib.Order.Basic"]
+    assert all("skipped" not in t for _, t in skeleton.contexts)
+    context_texts = [entry[1] for entry in skeleton.contexts]
+    assert context_texts == [
+        "namespace Demo",
+        "variable {n : Nat}",
+        "open Nat",
+        'notation "⟪" x "⟫" => id x',
+        "end Demo",
+    ]
+    assert skeleton.contexts[0][0] == 6  # namespace Demo sits on line 6
+    assert skeleton.mutual_spans == [(15, 18)]
+
+
+def test_context_block_does_not_swallow_following_doc_comment() -> None:
+    """A doc comment after a context command belongs to the next declaration."""
+    text = (
+        "namespace Demo\n\n/-- Doc of the next declaration. -/\ndef next : Nat := 1\n"
+    )
+    skeleton = module_skeleton(SourceFile.from_text(text))
+    assert skeleton.contexts == [(1, "namespace Demo")]
 
 
 def test_lemma_keyword_refines_theorem_kind() -> None:
diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean
index 9151917ff2..62dda4e582 100644
--- a/scripts/exposition/Extract.lean
+++ b/scripts/exposition/Extract.lean
@@ -87,15 +87,15 @@ def directUses (env : Environment) (info : ConstantInfo) : Array Name :=
       |>.toArray
   | _ => info.getUsedConstantsAsSet.toArray
 
-/-- Expand the used-constant set of `info`, tunnelling through generated pool
+/-- Expand a seed set of used constants, tunnelling through generated pool
 auxiliaries, until exposed pool declarations (edges) or non-pool constants
 (externals) are reached. -/
-def resolveDeps (env : Environment) (self : Name) (info : ConstantInfo)
+def resolveSeeds (env : Environment) (self : Name) (seeds : Array Name)
     (exposed : NameSet) : NameSet × Nat := Id.run do
   let mut edges : NameSet := {}
   let mut externals : NameSet := {}
   let mut visited : NameSet := {}
-  let mut stack : Array Name := directUses env info
+  let mut stack : Array Name := seeds
   while h : stack.size > 0 do
     let c := stack[stack.size - 1]
     stack := stack.pop
@@ -124,7 +124,13 @@ def declJson (env : Environment) (name : Name) (info : ConstantInfo)
   let module := env.header.moduleNames[moduleIdx.toNat]!
   let display := privateToUserName name
   let doc ← findDocString? env name
-  let (edges, extCount) := resolveDeps env name info exposed
+  let (edges, extCount) := resolveSeeds env name (directUses env info) exposed
+  -- Statement-only dependencies for proof-carrying declarations: the minimal
+  -- Lean file replaces their proofs by `sorry`, so only the type's
+  -- dependencies must be present for it to elaborate.
+  let typeEdges : Option NameSet := match info with
+    | .thmInfo v => some (resolveSeeds env name v.type.getUsedConstants exposed).1
+    | _ => none
   let r := ranges.range
   let s := ranges.selectionRange
   return some <| Json.mkObj <| [
@@ -136,7 +142,10 @@ def declJson (env : Environment) (name : Name) (info : ConstantInfo)
     ("s", toJson [s.pos.line, s.pos.column]),
     ("deps", Json.arr (edges.toArray.map (Json.str ∘ escapeName))),
     ("ext", Json.num extCount)
-  ] ++ (if isPrivateName name then [("p", Json.bool true)] else [])
+  ] ++ (match typeEdges with
+    | some t => [("tdeps", Json.arr (t.toArray.map (Json.str ∘ escapeName)))]
+    | none => [])
+    ++ (if isPrivateName name then [("p", Json.bool true)] else [])
     ++ (match doc with | some d => [("d", Json.str d)] | none => [])
 
 def extract (outPath : System.FilePath) : CoreM Unit := do