diff --git a/.github/scripts/busy_beaver_ci_shards.py b/.github/scripts/busy_beaver_ci_shards.py
new file mode 100755
index 00000000..be358d6b
--- /dev/null
+++ b/.github/scripts/busy_beaver_ci_shards.py
@@ -0,0 +1,362 @@
+#!/usr/bin/env python3
+# Copyright (c) 2026 Google LLC. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+"""Dependency-aware sharding and artifact helper for BusyBeaver CI and Docs CI.
+
+Commands:
+  plan        Partition BusyBeaver's module graph into:
+                - `foundation`: `BusyBeaverChallenge` plus every local module
+                  imported by at least one non-root module in `BusyBeaver`
+                  (e.g. `Cryptids.Machines`, `Defs`, `Basic`, `Calculi.*`,
+                  `A6.*`, `Pomme.*`, and shared donor `M_*` modules).
+                - `shards[0..N-1]`: all remaining pure leaf modules
+                  (in-degree 0 outside `BusyBeaver.lean`), deterministically
+                  assigned via `crc32(module) % N` so adding/removing proofs in
+                  PRs preserves per-shard cache locality.
+  pack        Pack `.lake/build/{lib/lean,ir}` artifacts for `foundation` or a
+              given `--shard` into a zstd tarball.
+  docs-args   Emit the minimal `lake build` target list required by
+              `literate.toml` so `docs.yml` never compiles excluded `M_*` blobs.
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import os
+import pathlib
+import re
+import shlex
+import subprocess
+import tempfile
+import tomllib
+import zlib
+
+IMPORT_LINE_RE = re.compile(
+    r"^(?:public\s+)?(?:meta\s+)?import(?:\s+all)?\s+(.+)$"
+)
+
+
+def strip_lean_comments(src: str) -> str:
+  """Strip `--` line comments and nested `/- ... -/` block comments."""
+  out: list[str] = []
+  i = 0
+  n = len(src)
+  depth = 0
+  in_str = False
+  while i < n:
+    ch = src[i]
+    nxt = src[i + 1] if i + 1 < n else ""
+    if depth > 0:
+      if ch == "/" and nxt == "-":
+        depth += 1
+        i += 2
+      elif ch == "-" and nxt == "/":
+        depth -= 1
+        i += 2
+      else:
+        if ch == "\n":
+          out.append("\n")
+        i += 1
+    elif in_str:
+      out.append(ch)
+      if ch == "\\" and i + 1 < n:
+        out.append(nxt)
+        i += 2
+      else:
+        if ch == '"':
+          in_str = False
+        i += 1
+    else:
+      if ch == "/" and nxt == "-":
+        depth = 1
+        out.append(" ")
+        i += 2
+      elif ch == "-" and nxt == "-":
+        while i < n and src[i] != "\n":
+          i += 1
+      else:
+        if ch == '"':
+          in_str = True
+        out.append(ch)
+        i += 1
+  return "".join(out)
+
+
+def mod_to_source(root: pathlib.Path, mod: str) -> pathlib.Path:
+  parts = [p.strip("«»") for p in mod.split(".")]
+  return root.joinpath(*parts).with_suffix(".lean")
+
+
+def parse_local_imports(root: pathlib.Path, path: pathlib.Path) -> list[str]:
+  # In Lean 4, module headers consist solely of optional `module`, optional
+  # `prelude`, and `import` statements before the first command/declaration.
+  clean = strip_lean_comments(path.read_text(encoding="utf-8"))
+  found: list[str] = []
+  for raw_line in clean.splitlines():
+    line = raw_line.strip()
+    if not line or line in ("prelude", "module"):
+      continue
+    match = IMPORT_LINE_RE.match(line)
+    if not match:
+      break
+    for tok in match.group(1).split():
+      if mod_to_source(root, tok).is_file():
+        found.append(tok)
+  return found
+
+
+def compute_partition(
+    root: pathlib.Path, num_shards: int
+) -> tuple[list[str], list[list[str]]]:
+  bb_root = root / "BusyBeaver.lean"
+  if not bb_root.is_file():
+    raise SystemExit(f"Missing {bb_root}")
+
+  seed_imports = parse_local_imports(root, bb_root)
+  reachable: dict[str, list[str]] = {}
+  stack = list(seed_imports)
+  while stack:
+    mod = stack.pop()
+    if mod in reachable or mod == "BusyBeaver":
+      continue
+    src = mod_to_source(root, mod)
+    if not src.is_file():
+      continue
+    imps = parse_local_imports(root, src)
+    reachable[mod] = imps
+    stack.extend(imps)
+
+  # Include BusyBeaverChallenge and its local imports (if any) in foundation.
+  challenge_mods = {"BusyBeaverChallenge"}
+  c_stack = ["BusyBeaverChallenge"]
+  while c_stack:
+    mod = c_stack.pop()
+    src = mod_to_source(root, mod)
+    if not src.is_file():
+      continue
+    for imp in parse_local_imports(root, src):
+      if imp not in challenge_mods:
+        challenge_mods.add(imp)
+        c_stack.append(imp)
+
+  imported_by_nonroot: set[str] = set()
+  for imps in reachable.values():
+    imported_by_nonroot.update(imps)
+
+  foundation = sorted((imported_by_nonroot | challenge_mods) - {"BusyBeaver"})
+  foundation_set = set(foundation)
+  leaves = sorted(m for m in reachable if m not in foundation_set)
+
+  # Invariant check: no leaf may import a module outside foundation.
+  for leaf in leaves:
+    bad = [imp for imp in reachable[leaf] if imp not in foundation_set]
+    if bad:
+      raise SystemExit(f"Partition invariant violated: {leaf} imports {bad}")
+
+  shards: list[list[str]] = [[] for _ in range(num_shards)]
+  for mod in leaves:
+    idx = zlib.crc32(mod.encode("utf-8")) % num_shards
+    shards[idx].append(mod)
+
+  return foundation, shards
+
+
+def hash_files(root: pathlib.Path, rel_paths: list[str]) -> str:
+  h = hashlib.sha256()
+  for rel in sorted(rel_paths):
+    p = root / rel
+    h.update(rel.encode("utf-8"))
+    h.update(b"\0")
+    h.update(hashlib.sha256(p.read_bytes()).digest())
+    h.update(b"\0")
+  return h.hexdigest()[:24]
+
+
+def emit_output(key: str, value: str) -> None:
+  gh_out = os.environ.get("GITHUB_OUTPUT")
+  if gh_out:
+    with open(gh_out, "a", encoding="utf-8") as f:
+      f.write(f"{key}={value}\n")
+  print(f"{key}={value}")
+
+
+def module_artifact_paths(root: pathlib.Path, mod: str) -> list[str]:
+  rel_no_ext = pathlib.Path(*mod.split("."))
+  parent_part = rel_no_ext.parent
+  stem = rel_no_ext.name
+  results: list[str] = []
+  for sub in ("lib/lean", "ir"):
+    base_dir = root / ".lake" / "build" / sub / parent_part
+    if not base_dir.is_dir():
+      continue
+    for entry in sorted(base_dir.iterdir()):
+      if entry.is_file() and (
+          entry.name == stem or entry.name.startswith(stem + ".")
+      ):
+        results.append(entry.relative_to(root).as_posix())
+  return results
+
+
+def cmd_plan(args: argparse.Namespace) -> None:
+  root = pathlib.Path(args.root).resolve()
+  foundation, shards = compute_partition(root, args.num_shards)
+
+  base_cfg = ["lean-toolchain", "lake-manifest.json", "lakefile.toml"]
+  f_rels = base_cfg + [
+      mod_to_source(root, m).relative_to(root).as_posix() for m in foundation
+  ]
+  f_hash = hash_files(root, f_rels)
+  emit_output("foundation_count", str(len(foundation)))
+  emit_output("foundation_hash", f_hash)
+
+  if args.targets_out:
+    targets = foundation if args.shard is None else shards[args.shard]
+    out_path = pathlib.Path(args.targets_out)
+    out_path.parent.mkdir(parents=True, exist_ok=True)
+    out_path.write_text("\n".join(targets) + ("\n" if targets else ""), encoding="utf-8")
+
+  if args.shard is not None:
+    shard_mods = shards[args.shard]
+    s_rels = [
+        mod_to_source(root, m).relative_to(root).as_posix() for m in shard_mods
+    ]
+    s_hash = hash_files(root, s_rels) if s_rels else "empty"
+    emit_output("shard_count", str(len(shard_mods)))
+    emit_output("shard_hash", s_hash)
+
+
+def cmd_pack(args: argparse.Namespace) -> None:
+  root = pathlib.Path(args.root).resolve()
+  foundation, shards = compute_partition(root, args.num_shards)
+  if args.group == "foundation":
+    mods = foundation
+  else:
+    shard_idx = int(args.group)
+    mods = shards[shard_idx]
+
+  collected: list[str] = []
+  missing: list[str] = []
+  for mod in mods:
+    olean = (
+        root
+        / ".lake"
+        / "build"
+        / "lib"
+        / "lean"
+        / (mod.replace(".", "/") + ".olean")
+    )
+    trace = (
+        root
+        / ".lake"
+        / "build"
+        / "lib"
+        / "lean"
+        / (mod.replace(".", "/") + ".trace")
+    )
+    ir_c = (
+        root / ".lake" / "build" / "ir" / (mod.replace(".", "/") + ".c")
+    )
+    if not (olean.is_file() and trace.is_file() and ir_c.is_file()):
+      missing.append(mod)
+      continue
+    collected.extend(module_artifact_paths(root, mod))
+
+  if missing and not args.allow_partial:
+    raise SystemExit(
+        f"Missing compiled artifacts for {len(missing)} module(s), e.g. "
+        f"{missing[:5]}"
+    )
+
+  out_file = pathlib.Path(args.out).resolve()
+  unique_files = sorted(set(collected))
+  if not unique_files:
+    out_file.unlink(missing_ok=True)
+    if args.allow_partial:
+      print("No completed module artifacts found; skipping partial archive.")
+      return
+    raise SystemExit("No compiled module artifacts found to pack.")
+
+  out_file.parent.mkdir(parents=True, exist_ok=True)
+  with tempfile.NamedTemporaryFile("w", encoding="utf-8", delete=False) as tf:
+    for rel in unique_files:
+      tf.write(rel + "\n")
+    list_path = tf.name
+  try:
+    subprocess.run(
+        ["tar", "--zstd", "-cf", str(out_file), "-C", str(root), "-T", list_path],
+        check=True,
+    )
+  finally:
+    pathlib.Path(list_path).unlink(missing_ok=True)
+  size_mb = out_file.stat().st_size / (1024 * 1024)
+  print(
+      f"Packed {len(unique_files)} files ({len(mods) - len(missing)}/{len(mods)}"
+      f" modules) into {out_file} ({size_mb:.2f} MiB)"
+  )
+
+
+def cmd_docs_args(args: argparse.Namespace) -> None:
+  root = pathlib.Path(args.root).resolve()
+  cfg = tomllib.loads((root / "literate.toml").read_text(encoding="utf-8"))
+  excludes = [e.strip() for e in cfg.get("exclude", [])]
+
+  def is_excluded(mod: str) -> bool:
+    return any(mod == ex or mod.startswith(ex + ".") for ex in excludes)
+
+  targets: list[str] = []
+  seen: set[str] = set()
+  for entry in cfg.get("targets", []):
+    mod = entry.get("module")
+    lib = entry.get("library")
+    if mod:
+      src = mod_to_source(root, mod)
+      mod_dir = root / mod.replace(".", "/")
+      candidates: list[str] = []
+      if src.is_file():
+        candidates.append(mod)
+      if mod_dir.is_dir():
+        for f in sorted(mod_dir.rglob("*.lean")):
+          candidates.append(".".join(f.relative_to(root).with_suffix("").parts))
+      if not candidates:
+        raise SystemExit(f"literate.toml target module {mod!r} matches no .lean files")
+      for c in candidates:
+        if not is_excluded(c) and c not in seen:
+          seen.add(c)
+          targets.append(c)
+    elif lib:
+      if not is_excluded(lib) and lib not in seen:
+        seen.add(lib)
+        targets.append(lib)
+  emit_output("build_args", " ".join(shlex.quote(t) for t in targets))
+
+
+def main() -> None:
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("--root", default=".", help="Repository root directory")
+  sub = parser.add_subparsers(dest="cmd", required=True)
+
+  p_plan = sub.add_parser("plan")
+  p_plan.add_argument("--num-shards", type=int, default=8)
+  p_plan.add_argument("--shard", type=int, default=None)
+  p_plan.add_argument("--targets-out", default=None)
+  p_plan.set_defaults(func=cmd_plan)
+
+  p_pack = sub.add_parser("pack")
+  p_pack.add_argument("--num-shards", type=int, default=8)
+  p_pack.add_argument(
+      "--group", required=True, help="'foundation' or shard index 0..N-1"
+  )
+  p_pack.add_argument("--out", required=True)
+  p_pack.add_argument("--allow-partial", action="store_true")
+  p_pack.set_defaults(func=cmd_pack)
+
+  p_docs = sub.add_parser("docs-args")
+  p_docs.set_defaults(func=cmd_docs_args)
+
+  parsed = parser.parse_args()
+  parsed.func(parsed)
+
+
+if __name__ == "__main__":
+  main()
diff --git a/.github/workflows/busy_beaver_ci.yml b/.github/workflows/busy_beaver_ci.yml
index 88a7a8ef..e9cac5de 100644
--- a/.github/workflows/busy_beaver_ci.yml
+++ b/.github/workflows/busy_beaver_ci.yml
@@ -14,6 +14,7 @@ on:
       - 'lake-manifest.json'
       - 'lean-toolchain'
       - '.github/workflows/busy_beaver_ci.yml'
+      - '.github/scripts/busy_beaver_ci_shards.py'
   pull_request:
     paths:
       - 'BusyBeaver/**'
@@ -27,14 +28,207 @@ on:
       - 'lake-manifest.json'
       - 'lean-toolchain'
       - '.github/workflows/busy_beaver_ci.yml'
+      - '.github/scripts/busy_beaver_ci_shards.py'
   workflow_dispatch:
 
 permissions:
   contents: read
 
+concurrency:
+  group: busy-beaver-ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
+
+env:
+  NUM_SHARDS: "8"
+  LEAN_NUM_THREADS: "1"
+
 jobs:
+  foundation:
+    name: Build shared foundation
+    runs-on: ubuntu-latest
+    timeout-minutes: 180
+
+    steps:
+      - name: Free runner disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /usr/local/share/boost
+
+      - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
+
+      - name: Plan foundation module graph
+        id: plan
+        run: |
+          python3 .github/scripts/busy_beaver_ci_shards.py plan \
+            --num-shards "$NUM_SHARDS" \
+            --targets-out "${RUNNER_TEMP}/foundation_targets.txt"
+
+      - uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
+        with:
+          build: false
+          test: false
+          lint: false
+          use-github-cache: "false"
+
+      - name: Restore foundation cache
+        id: cache-restore
+        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: .lake/shard-cache/foundation.tar.zst
+          key: bb-foundation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.plan.outputs.foundation_hash }}
+          restore-keys: |
+            bb-foundation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
+
+      - name: Unpack restored foundation cache
+        if: steps.cache-restore.outputs.cache-matched-key != ''
+        run: tar --zstd -xf .lake/shard-cache/foundation.tar.zst
+
+      - name: Compile foundation & shared donor modules
+        id: compile
+        timeout-minutes: 150
+        run: |
+          mapfile -t targets < "${RUNNER_TEMP}/foundation_targets.txt"
+          echo "Compiling ${#targets[@]} foundation module(s)..."
+          lake build "${targets[@]}"
+
+      - name: Pack foundation artifacts
+        if: ${{ !cancelled() && (success() || steps.compile.outcome == 'failure') }}
+        run: |
+          python3 .github/scripts/busy_beaver_ci_shards.py pack \
+            --num-shards "$NUM_SHARDS" \
+            --group foundation \
+            --out .lake/shard-cache/foundation.tar.zst \
+            ${{ steps.compile.outcome == 'failure' && '--allow-partial' || '' }}
+
+      - name: Save foundation cache
+        if: >-
+          ${{ !cancelled() &&
+              steps.cache-restore.outputs.cache-hit != 'true' &&
+              hashFiles('.lake/shard-cache/foundation.tar.zst') != '' &&
+              (success() || steps.compile.outcome == 'failure') }}
+        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: .lake/shard-cache/foundation.tar.zst
+          key: >-
+            bb-foundation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.compile.outcome == 'success' && steps.plan.outputs.foundation_hash || format('partial-{0}', github.run_id) }}
+
+      - name: Upload foundation artifact for shards
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: bb-foundation
+          path: .lake/shard-cache/foundation.tar.zst
+          compression-level: 0
+          retention-days: 1
+          if-no-files-found: error
+
+  shards:
+    name: Build leaf shard ${{ matrix.shard }}
+    needs: foundation
+    runs-on: ubuntu-latest
+    timeout-minutes: 180
+    strategy:
+      fail-fast: false
+      matrix:
+        shard: [0, 1, 2, 3, 4, 5, 6, 7]
+
+    steps:
+      - name: Free runner disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /usr/local/share/boost
+
+      - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
+
+      - name: Plan shard ${{ matrix.shard }} targets
+        id: plan
+        run: |
+          python3 .github/scripts/busy_beaver_ci_shards.py plan \
+            --num-shards "$NUM_SHARDS" \
+            --shard "${{ matrix.shard }}" \
+            --targets-out "${RUNNER_TEMP}/shard_targets.txt"
+
+      - uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
+        if: steps.plan.outputs.shard_count != '0'
+        with:
+          build: false
+          test: false
+          lint: false
+          use-github-cache: "false"
+
+      - name: Download & unpack foundation artifacts
+        if: steps.plan.outputs.shard_count != '0'
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: bb-foundation
+          path: .lake/foundation-in
+
+      - name: Unpack foundation tarball
+        if: steps.plan.outputs.shard_count != '0'
+        run: |
+          tar --zstd -xf .lake/foundation-in/foundation.tar.zst
+          rm -rf .lake/foundation-in
+
+      - name: Restore shard ${{ matrix.shard }} cache
+        id: cache-restore
+        if: steps.plan.outputs.shard_count != '0'
+        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: .lake/shard-cache/shard.tar.zst
+          key: bb-shard-v1-${{ matrix.shard }}-of-8-${{ runner.os }}-${{ steps.plan.outputs.foundation_hash }}-${{ steps.plan.outputs.shard_hash }}
+          restore-keys: |
+            bb-shard-v1-${{ matrix.shard }}-of-8-${{ runner.os }}-${{ steps.plan.outputs.foundation_hash }}-
+            bb-shard-v1-${{ matrix.shard }}-of-8-${{ runner.os }}-
+
+      - name: Unpack restored shard cache
+        if: steps.plan.outputs.shard_count != '0' && steps.cache-restore.outputs.cache-matched-key != ''
+        run: tar --zstd -xf .lake/shard-cache/shard.tar.zst
+
+      - name: Compile leaf shard ${{ matrix.shard }}
+        id: compile
+        if: steps.plan.outputs.shard_count != '0'
+        timeout-minutes: 150
+        run: |
+          mapfile -t targets < "${RUNNER_TEMP}/shard_targets.txt"
+          echo "Compiling ${#targets[@]} leaf module(s) in shard ${{ matrix.shard }}..."
+          lake build "${targets[@]}"
+
+      - name: Pack shard ${{ matrix.shard }} artifacts
+        if: >-
+          ${{ steps.plan.outputs.shard_count != '0' &&
+              !cancelled() &&
+              (success() || steps.compile.outcome == 'failure') }}
+        run: |
+          python3 .github/scripts/busy_beaver_ci_shards.py pack \
+            --num-shards "$NUM_SHARDS" \
+            --group "${{ matrix.shard }}" \
+            --out .lake/shard-cache/shard.tar.zst \
+            ${{ steps.compile.outcome == 'failure' && '--allow-partial' || '' }}
+
+      - name: Save shard ${{ matrix.shard }} cache
+        if: >-
+          ${{ steps.plan.outputs.shard_count != '0' &&
+              !cancelled() &&
+              steps.cache-restore.outputs.cache-hit != 'true' &&
+              hashFiles('.lake/shard-cache/shard.tar.zst') != '' &&
+              (success() || steps.compile.outcome == 'failure') }}
+        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: .lake/shard-cache/shard.tar.zst
+          key: >-
+            bb-shard-v1-${{ matrix.shard }}-of-8-${{ runner.os }}-${{ steps.plan.outputs.foundation_hash }}-${{ steps.compile.outcome == 'success' && steps.plan.outputs.shard_hash || format('partial-{0}', github.run_id) }}
+
+      - name: Upload shard ${{ matrix.shard }} artifact
+        if: steps.plan.outputs.shard_count != '0'
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: bb-shard-${{ matrix.shard }}
+          path: .lake/shard-cache/shard.tar.zst
+          compression-level: 0
+          retention-days: 1
+          if-no-files-found: error
+
   build:
+    needs: [foundation, shards]
     runs-on: ubuntu-latest
+    timeout-minutes: 120
 
     steps:
       - name: Free runner disk space and install bubblewrap
@@ -45,11 +239,28 @@ jobs:
           sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
 
       - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
+
       - uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
         with:
-          build-args: "BusyBeaver BusyBeaverChallenge"
-        env:
-          LEAN_NUM_THREADS: "1"
+          build: false
+          test: false
+          lint: false
+          use-github-cache: "false"
+
+      - name: Download foundation & leaf shard artifacts
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          pattern: bb-*
+          path: .lake/artifacts-in
+
+      - name: Assemble `.lake/build` and compile `BusyBeaver` root
+        run: |
+          for archive in .lake/artifacts-in/*/*.tar.zst; do
+            echo "Unpacking $archive..."
+            tar --zstd -xf "$archive"
+          done
+          rm -rf .lake/artifacts-in
+          lake build BusyBeaver BusyBeaverChallenge
 
       - name: Verify BusyBeaver against BusyBeaverChallenge with comparator
         run: lake comparator --config comparator/busy_beaver.json
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 7ae6412f..9ce6c247 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -4,6 +4,19 @@ on:
   push:
     branches:
       - main
+    paths-ignore:
+      - '**/*.md'
+      - '.github/workflows/busy_beaver_ci.yml'
+      - '.github/workflows/lean_action_ci.yml'
+      - '.github/workflows/create-release.yml'
+      - '.github/workflows/update.yml'
+      - 'BusyBeaver/BB6/Halt/**'
+      - 'BusyBeaver/BB6/NonHalt/**'
+      - 'BusyBeaver/BB6/Cryptids/**'
+      - 'BusyBeaver/Calculi/**'
+      - 'BusyBeaver.lean'
+      - 'comparator/**'
+      - 'verify.py'
   workflow_dispatch:
 
 permissions:
@@ -14,21 +27,33 @@ permissions:
 jobs:
   build:
     runs-on: ubuntu-latest
+    timeout-minutes: 240
+    concurrency:
+      group: docs-build
+      cancel-in-progress: true
 
     steps:
       - name: Free runner disk space
         run: |
           sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /usr/local/share/boost
 
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
+      - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
+
+      - name: Compute documented Lean targets from literate.toml
+        id: docs-targets
+        run: python3 .github/scripts/busy_beaver_ci_shards.py docs-args
+
+      - uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
         with:
-          build-args: "Cryptids BusyBeaver"
+          build-args: ${{ steps.docs-targets.outputs.build_args }}
+          test: false
+          lint: false
         env:
           LEAN_NUM_THREADS: "1"
 
-      - name: Cache Verso literate build
-        uses: actions/cache@v4
+      - name: Restore Verso literate build cache
+        id: verso-cache
+        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
         with:
           path: |
             .lake/packages/verso/.lake/build
@@ -36,12 +61,14 @@ jobs:
             .lake/packages/MD4Lean/.lake/build
             .lake/packages/illuminate/.lake/build
             .lake/build/literate
-          key: verso-literate-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
+          key: verso-literate-v2-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'literate.toml') }}-${{ github.sha }}
           restore-keys: |
-            verso-literate-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-
+            verso-literate-v2-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'literate.toml') }}-
+            verso-literate-v2-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-
 
       - name: Build Verso literate HTML
         id: verso
+        timeout-minutes: 150
         env:
           LEAN_NUM_THREADS: "1"
         run: |
@@ -53,20 +80,42 @@ jobs:
           sed -i 's/| \.latexMath _x => \.empty -- TODO/| .latexMath x => {{<code class="math inline">{{String.join x.toList}}<\/code>}}/; s/| \.latexMathDisplay _x => \.empty -- TODO/| .latexMathDisplay x => {{<code class="math display">{{String.join x.toList}}<\/code>}}/' .lake/packages/verso/src/verso-literate-code/VersoLiterateCode.lean
           path=$(lake query :literateHtml)
           echo "path=$path" >> "$GITHUB_OUTPUT"
-          rm -rf .lake/packages/mathlib .lake/build/lib .lake/build/ir
+
+      - name: Save Verso literate build cache
+        # Persist partial `.lake/build/literate/*.json` progress even if `verso` hits its step
+        # timeout, avoiding a cold-cache timeout loop.
+        if: >-
+          ${{ !cancelled() &&
+              steps.verso-cache.outputs.cache-hit != 'true' &&
+              (success() || steps.verso.outcome == 'failure') }}
+        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: |
+            .lake/packages/verso/.lake/build
+            .lake/packages/subverso/.lake/build
+            .lake/packages/MD4Lean/.lake/build
+            .lake/packages/illuminate/.lake/build
+            .lake/build/literate
+          key: verso-literate-v2-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'literate.toml') }}-${{ github.sha }}
+
+      - name: Reclaim build disk space before Pages upload
+        run: rm -rf .lake/packages/mathlib .lake/build/lib .lake/build/ir
 
       - name: Upload Pages artifact
-        uses: actions/upload-pages-artifact@v4
+        uses: actions/upload-pages-artifact@7b1f4a764d45c48632c6b24a0339c27f5614fb0b # v4.0.0
         with:
           path: ${{ steps.verso.outputs.path }}
 
   deploy:
     needs: build
     runs-on: ubuntu-latest
+    concurrency:
+      group: github-pages
+      cancel-in-progress: false
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v4
+        uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5
diff --git a/literate.toml b/literate.toml
index d7f130a4..dae9e5af 100644
--- a/literate.toml
+++ b/literate.toml
@@ -1,7 +1,58 @@
 landing_page = "Cryptids"
 extra_css = ["literate-overrides.css"]
 
-order = ["Cryptids", "BusyBeaver"]
+# Verso applies `order` at every directory level (`parent == prefix_`), including
+# dotted subsection prefixes where `[order_children]` TOML keys wouldn't split.
+order = [
+  "Cryptids",
+  "BusyBeaver",
+  "BusyBeaverChallenge",
+  # BusyBeaver.BB6
+  "BusyBeaver.BB6.Equivalences",
+  "BusyBeaver.BB6.Hardness",
+  "BusyBeaver.BB6.HardnessEvidence",
+  "BusyBeaver.BB6.Accelerations",
+  "BusyBeaver.BB6.A6",
+  "BusyBeaver.BB6.Pomme",
+  # Cryptids.Semantics
+  "Cryptids.Semantics.Goldbach",
+  "Cryptids.Semantics.Zf",
+  "Cryptids.Semantics.Zf393",
+  "Cryptids.Semantics.PA",
+  "Cryptids.Semantics.Riemann",
+  "Cryptids.Semantics.Riemann120",
+  "Cryptids.Semantics.Riemann95",
+  "Cryptids.Semantics.ErdosTernary15",
+  "Cryptids.Semantics.ErdosTernary14",
+  "Cryptids.Semantics.Brocard28",
+  # Cryptids.Semantics.Zf
+  "Cryptids.Semantics.Zf.Boot",
+  "Cryptids.Semantics.Zf.Gadgets",
+  "Cryptids.Semantics.Zf.Dispatcher",
+  "Cryptids.Semantics.Zf.Subroutines",
+  "Cryptids.Semantics.Zf.RegisterMachine",
+  "Cryptids.Semantics.Zf.Soundness",
+  # Cryptids.Semantics.Zf393
+  "Cryptids.Semantics.Zf393.Backend",
+  "Cryptids.Semantics.Zf393.Program",
+  # Cryptids.Semantics.Riemann
+  "Cryptids.Semantics.Riemann.Gadgets",
+  "Cryptids.Semantics.Riemann.Dispatcher",
+  "Cryptids.Semantics.Riemann.RegisterMachine",
+  "Cryptids.Semantics.Riemann.Analytic",
+  "Cryptids.Semantics.Riemann.Schmidt",
+  "Cryptids.Semantics.Riemann.DigammaBinet",
+  "Cryptids.Semantics.Riemann.HorizontalBounds",
+  "Cryptids.Semantics.Riemann.VonMangoldtCount",
+  "Cryptids.Semantics.Riemann.WeightedStieltjes",
+  "Cryptids.Semantics.Riemann.ExplicitLarge",
+  # Cryptids.Semantics.Riemann120
+  "Cryptids.Semantics.Riemann120.Backend",
+  "Cryptids.Semantics.Riemann120.Program",
+  "Cryptids.Semantics.Riemann120.Analytic",
+  "Cryptids.Semantics.Riemann120.VonMangoldt",
+  "Cryptids.Semantics.Riemann120.Bridge",
+]
 
 [metadata]
 title = "Cryptids & Busy Beaver"
@@ -10,8 +61,68 @@ description = "Formally verified conjecture-checking and Busy Beaver Turing mach
 [[targets]]
 library = "Cryptids"
 
+[[targets]]
+library = "BusyBeaverChallenge"
+
+# Render human-authored BusyBeaver definitions, certificate frameworks,
+# equivalence/hardness analyses, and named case studies (`A6`, `Pomme`,
+# `WilyCoyote`) without running full SubVerso hover elaboration on hundreds of
+# generated `M_*` holdout proof scripts and `Calculi` data tables.
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.Defs"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.Basic"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.Bridge"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.Cert"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.WordRLE"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.AffRLE"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.ElabRLE"
+
 [[targets]]
 library = "BusyBeaver"
+module = "BusyBeaver.BB6.Equivalences"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.BB6.Hardness"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.BB6.HardnessEvidence"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.BB6.Accelerations.Stack"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.BB6.A6"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.BB6.Pomme"
+
+[[targets]]
+library = "BusyBeaver"
+module = "BusyBeaver.BB33.WilyCoyote"
 
 [order_children]
 "BusyBeaver" = [
@@ -19,6 +130,9 @@ library = "BusyBeaver"
   "BusyBeaver.Basic",
   "BusyBeaver.Bridge",
   "BusyBeaver.Cert",
+  "BusyBeaver.WordRLE",
+  "BusyBeaver.AffRLE",
+  "BusyBeaver.ElabRLE",
   "BusyBeaver.BB6",
   "BusyBeaver.BB33",
 ]
@@ -30,48 +144,14 @@ library = "BusyBeaver"
   "Cryptids.Zf380",
   "Cryptids.Riemann120",
   "Cryptids.Riemann104",
+  "Cryptids.Riemann95",
+  "Cryptids.ErdosTernary15",
+  "Cryptids.ErdosTernary14",
+  "Cryptids.Brocard28",
   "Cryptids.Semantics",
-]
-"Cryptids.Semantics" = [
-  "Cryptids.Semantics.Goldbach",
-  "Cryptids.Semantics.Zf",
-  "Cryptids.Semantics.Zf393",
-  "Cryptids.Semantics.Riemann",
-  "Cryptids.Semantics.Riemann120",
-]
-"Cryptids.Semantics.Zf" = [
-  "Cryptids.Semantics.Zf.Boot",
-  "Cryptids.Semantics.Zf.Gadgets",
-  "Cryptids.Semantics.Zf.Dispatcher",
-  "Cryptids.Semantics.Zf.Subroutines",
-  "Cryptids.Semantics.Zf.RegisterMachine",
-  "Cryptids.Semantics.Zf.Soundness",
-]
-"Cryptids.Semantics.Zf393" = [
-  "Cryptids.Semantics.Zf393.Backend",
-  "Cryptids.Semantics.Zf393.Program",
-]
-"Cryptids.Semantics.Riemann" = [
-  "Cryptids.Semantics.Riemann.Gadgets",
-  "Cryptids.Semantics.Riemann.Dispatcher",
-  "Cryptids.Semantics.Riemann.RegisterMachine",
-  "Cryptids.Semantics.Riemann.Analytic",
-  "Cryptids.Semantics.Riemann.Schmidt",
-  "Cryptids.Semantics.Riemann.DigammaBinet",
-  "Cryptids.Semantics.Riemann.HorizontalBounds",
-  "Cryptids.Semantics.Riemann.VonMangoldtCount",
-  "Cryptids.Semantics.Riemann.WeightedStieltjes",
-  "Cryptids.Semantics.Riemann.ExplicitLarge",
-]
-"Cryptids.Semantics.Riemann120" = [
-  "Cryptids.Semantics.Riemann120.Backend",
-  "Cryptids.Semantics.Riemann120.Program",
-  "Cryptids.Semantics.Riemann120.Analytic",
-  "Cryptids.Semantics.Riemann120.VonMangoldt",
-  "Cryptids.Semantics.Riemann120.Bridge",
+  "Cryptids.ReductionSupport",
 ]
 
 # Verso's dark mode leaves code tokens black on a dark background.
 [theme.dark]
 code_color = "var(--verso-text-color)"
-