diff --git a/.gitignore b/.gitignore
index 3c886f148965e4..077c05742ada71 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,3 +8,5 @@
 **/__pycache__/
 # Progress file from scripts/rm_set_option.py
 scripts/.rm_set_option_progress.jsonl
+# Output directory for `lake exe no_expose`
+scripts/.no_expose/
diff --git a/lakefile.lean b/lakefile.lean
index c6ef52a6ff89f8..ce92f0359e49bb 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -127,6 +127,25 @@ lean_exe «check_title_labels» where
 lean_exe «nightly-testing-checklist» where
   srcDir := "scripts"
 
+/-- Implementation modules for the `no_expose` exe (see below). Kept as a
+lib so multiple files under `scripts/NoExpose/` can `import` each other.
+The lib deliberately does NOT pull in Mathlib. -/
+lean_lib NoExpose where
+  srcDir := "scripts"
+  globs := #[`NoExpose.+]
+
+/-- `lake exe no_expose` is the user-facing tool for analysing and
+removing unnecessary `@[expose]` attributes in Mathlib (and downstream
+Mathlib-using projects). Subcommands:
+  * `collect` — build with diagnostics, scan env, produce report data
+  * `report`  — render per-file recommendations (no build)
+  * `edit`    — apply removals (with safety checks + audit trail)
+The exe deliberately does NOT `import Mathlib` so that it builds in
+seconds; it loads Mathlib at runtime via `Lean.withImportModules`. -/
+lean_exe no_expose where
+  srcDir := "scripts"
+  supportInterpreter := true
+
 lean_exe mathlib_test_executable where
   root := `MathlibTest.MathlibTestExecutable
 
diff --git a/scripts/NoExpose/Cli.lean b/scripts/NoExpose/Cli.lean
new file mode 100644
index 00000000000000..51acf0788687fd
--- /dev/null
+++ b/scripts/NoExpose/Cli.lean
@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+/-!
+# `NoExpose.Cli` — argument parsing for `lake exe no_expose`
+
+Subcommands: `collect`, `report`, `edit`, plus `clean` for removing the
+data directory.
+-/
+
+namespace NoExpose
+
+/-- Format option for `report` output. -/
+inductive ReportFormat where
+  | text
+  | json
+  deriving Repr, BEq
+
+structure CollectArgs where
+  skipBuild : Bool := false
+  /-- Extra files to insert `set_option diagnostics false` into. -/
+  patchFiles : Array String := #[]
+
+structure ReportArgs where
+  paths : Array String := #[]
+  format : ReportFormat := .text
+
+structure EditArgs where
+  paths : Array String := #[]
+  dryRun : Bool := false
+  verify : Bool := false
+  forceDirty : Bool := false
+  forceStale : Bool := false
+
+inductive Subcommand where
+  | help
+  | collect (args : CollectArgs)
+  | report  (args : ReportArgs)
+  | edit    (args : EditArgs)
+  | clean
+
+/-- Top-level help text. -/
+def helpText : String := "\
+USAGE:
+  lake exe no_expose <subcommand> [args...]
+
+SUBCOMMANDS:
+  collect [--skip-build] [--patch-file FILE]...
+      Build Mathlib with `set_option diagnostics true`, walk the env,
+      and write report data to scripts/.no_expose/.
+
+  report [PATH...] [--format text|json]
+      Render per-file recommendations from existing report data.
+      With no PATH, renders every file in the report. Default
+      `--format text` lists `safe-to-unexpose` and
+      `needed-downstream` decls in each file.
+
+  edit [PATH...] [--dry-run] [--verify] [--force-dirty] [--force-stale]
+      Apply (default) or preview (--dry-run) the un-expose edits to
+      each PATH. Refuses on dirty git tree or stale report unless the
+      corresponding --force-* flag is given. With --verify, runs
+      `lake build` on the touched lib after applying.
+
+  clean
+      Remove scripts/.no_expose/ entirely.
+
+  help, --help, -h
+      Show this message.
+"
+
+private def parseFormat : String → Except String ReportFormat
+  | "text" => .ok .text
+  | "json" => .ok .json
+  | s      => .error s!"unknown --format value: {s} (expected text|json)"
+
+/-- Parse a `collect` argument list. -/
+private partial def parseCollect (rest : List String) : Except String CollectArgs := loop rest {} where
+  loop : List String → CollectArgs → Except String CollectArgs
+    | [], acc => .ok acc
+    | "--skip-build" :: rest, acc => loop rest { acc with skipBuild := true }
+    | "--patch-file" :: f :: rest, acc =>
+      loop rest { acc with patchFiles := acc.patchFiles.push f }
+    | flag :: _, _ => .error s!"collect: unknown argument {flag}"
+
+/-- Parse a `report` argument list. -/
+private partial def parseReport (rest : List String) : Except String ReportArgs := loop rest {} where
+  loop : List String → ReportArgs → Except String ReportArgs
+    | [], acc => .ok acc
+    | "--format" :: v :: rest, acc => do
+      let f ← parseFormat v
+      loop rest { acc with format := f }
+    | arg :: rest, acc =>
+      if arg.startsWith "--" then .error s!"report: unknown flag {arg}"
+      else loop rest { acc with paths := acc.paths.push arg }
+
+/-- Parse an `edit` argument list. -/
+private partial def parseEdit (rest : List String) : Except String EditArgs := loop rest {} where
+  loop : List String → EditArgs → Except String EditArgs
+    | [], acc => .ok acc
+    | "--dry-run" :: rest, acc => loop rest { acc with dryRun := true }
+    | "--verify" :: rest, acc => loop rest { acc with verify := true }
+    | "--force-dirty" :: rest, acc => loop rest { acc with forceDirty := true }
+    | "--force-stale" :: rest, acc => loop rest { acc with forceStale := true }
+    | arg :: rest, acc =>
+      if arg.startsWith "--" then .error s!"edit: unknown flag {arg}"
+      else loop rest { acc with paths := acc.paths.push arg }
+
+/-- Top-level dispatch. -/
+def parseArgs : List String → Except String Subcommand
+  | []                       => .ok .help
+  | "help" :: _              => .ok .help
+  | "--help" :: _            => .ok .help
+  | "-h" :: _                => .ok .help
+  | "collect" :: rest        => .collect <$> parseCollect rest
+  | "report"  :: rest        => .report  <$> parseReport rest
+  | "edit"    :: rest        => .edit    <$> parseEdit rest
+  | "clean" :: []            => .ok .clean
+  | "clean" :: rest          => .error s!"clean: unexpected arguments: {String.intercalate " " rest}"
+  | sub :: _                 => .error s!"unknown subcommand: {sub} (try `--help`)"
+
+end NoExpose
diff --git a/scripts/NoExpose/Collect.lean b/scripts/NoExpose/Collect.lean
new file mode 100644
index 00000000000000..4fde35b13c5cb9
--- /dev/null
+++ b/scripts/NoExpose/Collect.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import NoExpose.Cli
+import NoExpose.Diagnostics
+import NoExpose.Env
+import NoExpose.Paths
+import NoExpose.Report
+import NoExpose.Restore
+
+/-!
+# `NoExpose.Collect` — orchestrator for the `collect` subcommand
+
+Owns the high-level sequence:
+1. `NoExpose.Diagnostics`: patch lakefile, run `lake build`, parse log
+   into `diagnostics.jsonl`. Skipped under `--skip-build`.
+2. `NoExpose.Env`: open env via `withImportModules`; emit
+   `exposed.jsonl`, `static_refs.jsonl`, `decl_refs.jsonl`.
+3. `NoExpose.Report.build`: join everything into `report.jsonl`.
+-/
+
+open Lean
+
+namespace NoExpose
+
+/-- Run the env-scan portion of `collect`: opens the env once via
+`withImportModules`, gathers static/decl refs, returns enumerated
+candidates; then post-scans source files and writes `exposed.jsonl`. -/
+unsafe def runEnvScan (_project : ProjectInfo) (modules : Array Name)
+    (scopePrefix : Array Name) : IO Unit := do
+  IO.FS.createDirAll dataDir
+  let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot))
+  -- All env-dependent work happens inside `withImportModules`. The
+  -- `DeclRecord` fields are stringified (and `Name` references dropped)
+  -- before any iteration of the records, so the data is safe to write
+  -- without lifetime worries.
+  withImportModules modules
+      (searchPath := searchPath) (trustLevel := 1024) do
+    let env ← getEnv
+    -- Static refs → static_refs.jsonl
+    let refs ← collectStaticRefs
+    IO.FS.withFile staticRefsPath .write fun h => writeStaticRefs env refs h
+    IO.eprintln s!"[no_expose collect] wrote {refs.size} static-refs pairs to {staticRefsPath}"
+    -- Per-decl refs → decl_refs.jsonl
+    IO.FS.withFile declRefsPath .write fun h => writeDeclRefs env h
+    IO.eprintln s!"[no_expose collect] wrote per-decl refs to {declRefsPath}"
+    -- Source-driven enumeration: walk source for `@[expose]`,
+    -- intersect with env decl ranges.
+    let recs ← enumerate scopePrefix
+    IO.FS.withFile exposedPath .write fun h => do
+      for r in recs do h.putStrLn r.toJsonLine
+    IO.eprintln s!"[no_expose collect] wrote {recs.size} exposed records to {exposedPath}"
+
+/-- Run the `collect` subcommand. -/
+unsafe def runCollect (args : CollectArgs) : IO UInt32 := do
+  -- On every startup, restore any orphaned backups left by an
+  -- interrupted previous run. (No-op if state.json is absent.)
+  detectOrphan
+  let project ← detectProjectInfo
+  IO.eprintln s!"[no_expose collect] project: {project.name} \
+    (libs: {project.libRoots})"
+  -- Step 1: full build with diagnostics, unless skipped.
+  unless args.skipBuild do
+    if project.name.toString != "mathlib" then
+      IO.eprintln s!"no_expose collect: full-build mode is Mathlib-only \
+        (detected project: {project.name}); pass --skip-build."
+      return 1
+    let extraOff : Array System.FilePath := args.patchFiles.map .mk
+    let rc ← runDiagnostics project.lakefilePath extraOff
+    if rc != 0 then
+      IO.eprintln s!"[no_expose collect] lake build returned {rc}; \
+        diagnostics.jsonl reflects the partial log. Continuing with env scan."
+  -- Step 2: env scan.
+  -- For Mathlib, the canonical target is just `Mathlib` (the union module).
+  -- For downstream projects, pick the first lib root.
+  let modules : Array Name :=
+    if project.libRoots.contains `Mathlib then #[`Mathlib]
+    else project.libRoots.take 1
+  let scopePrefix : Array Name :=
+    if project.libRoots.contains `Mathlib then #[`Mathlib]
+    else project.libRoots
+  runEnvScan project modules scopePrefix
+  -- Step 3: join.
+  build exposedPath diagnosticsPath staticRefsPath declRefsPath reportPath
+  return 0
+
+end NoExpose
diff --git a/scripts/NoExpose/Diagnostics.lean b/scripts/NoExpose/Diagnostics.lean
new file mode 100644
index 00000000000000..5f78a3bd8ac74f
--- /dev/null
+++ b/scripts/NoExpose/Diagnostics.lean
@@ -0,0 +1,276 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import NoExpose.Paths
+import NoExpose.Restore
+
+/-!
+# `NoExpose.Diagnostics` — lakefile patch + lake build + log parser
+
+Three pieces:
+
+* **patchLakefile**: insert two `mathlibLeanOptions` entries
+  (`diagnostics=true`, `diagnostics.threshold=0`). Recognises Mathlib's
+  `mathlibLeanOptions` `abbrev`; errors out on any other lakefile shape.
+* **patchDiagnosticsOffFiles**: 5-file hardcoded list of source files
+  that fail to elaborate under global `diagnostics=true`; we splice in
+  `set_option diagnostics false` after the last import.
+* **parseLog**: scan `build.log` line-by-line, emit one JSONL record
+  per (file, decl, count, category) tuple.
+
+The build itself is `lake build Mathlib`, run as a child process.
+Hours of CPU; pass `--skip-build` to `collect` to reuse an existing
+`build.log` and skip this step.
+-/
+
+open System
+
+namespace NoExpose
+
+/-! ## Lakefile patching -/
+
+private def patchMarkerBegin : String :=
+  "    -- BEGIN no_expose diagnostics patch"
+private def patchMarkerEnd : String :=
+  "    -- END no_expose diagnostics patch"
+
+private def patchAnchor : String := "    ⟨`autoImplicit, false⟩,\n"
+
+private def patchBlock : String :=
+  patchMarkerBegin ++ "\n" ++
+  "    ⟨`diagnostics, true⟩,\n" ++
+  "    ⟨`diagnostics.threshold, (0 : Nat)⟩,\n" ++
+  patchMarkerEnd ++ "\n"
+
+/-- Insert the diagnostics options into Mathlib's `mathlibLeanOptions`.
+Aborts (with a clear error) for any non-Mathlib lakefile shape. -/
+def patchLakefile (lakefilePath : FilePath) : IO Unit := do
+  let original ← IO.FS.readFile lakefilePath
+  let markerHits := (original.splitOn patchMarkerBegin).length
+  if markerHits > 1 then
+    throw <| IO.userError s!"{lakefilePath} already contains no_expose patch markers; \
+      restore it manually before re-running."
+  let anchorHits := (original.splitOn patchAnchor).length
+  unless anchorHits > 1 do
+    throw <| IO.userError s!"could not find insertion anchor in {lakefilePath}; \
+      only Mathlib-shaped lakefiles are supported. \
+      Pass --skip-build and enable diagnostics yourself, or run on Mathlib."
+  -- Replace first occurrence only.
+  let parts := original.splitOn patchAnchor
+  let patched := parts[0]! ++ patchAnchor ++ patchBlock ++
+                 String.intercalate patchAnchor (parts.drop 1)
+  -- Back up before writing.
+  backup lakefilePath
+  IO.FS.writeFile lakefilePath patched
+
+/-! ## Per-file diagnostics-off patches
+
+Five Mathlib files fail under global `diagnostics=true`. Splice
+`set_option diagnostics false` after the last `import` line. -/
+
+/-- Mathlib's hardcoded fragile-files list. Override via
+`patchDiagnosticsOffFiles extra` to add downstream files. -/
+def diagnosticsOffFiles : Array FilePath := #[
+  "Mathlib/Tactic/Linter/ValidatePRTitle.lean",
+  "Mathlib/Order/Interval/Lex.lean",
+  "Mathlib/Tactic/NormNum/Ordinal.lean",
+  "Mathlib/Probability/ConditionalProbability.lean",
+  "Mathlib/CategoryTheory/Discrete/Basic.lean"]
+
+private def filePatchLine : String :=
+  "-- no_expose: locally disable diagnostics so this file builds " ++
+  "under global `diagnostics=true`\nset_option diagnostics false\n"
+
+/-- Insert `set_option diagnostics false` after the last
+`import` / `public import` line. Idempotent: re-applying is a no-op. -/
+def patchOneFile (path : FilePath) : IO Unit := do
+  unless ← System.FilePath.pathExists path do
+    IO.eprintln s!"[no_expose diagnostics] skipping non-existent {path}"
+    return
+  let text ← IO.FS.readFile path
+  let alreadyPatched := (text.splitOn filePatchLine).length > 1
+  if alreadyPatched then return
+  let lines : List String := text.splitOn "\n"
+  let mut lastImport : Int := -1
+  for h : i in [:lines.length] do
+    let line : String := lines[i]
+    let stripped : String := line.trimAscii.toString
+    if stripped.startsWith "import " || stripped.startsWith "public import " then
+      lastImport := i
+  if lastImport < 0 then
+    throw <| IO.userError s!"no import line in {path}; can't insert set_option"
+  let i := lastImport.toNat + 1
+  let prefixLines := lines.take i
+  let suffixLines := lines.drop i
+  let patched := String.intercalate "\n"
+    (prefixLines ++ ["", filePatchLine.trimAsciiEnd.toString] ++ suffixLines)
+  backup path
+  IO.FS.writeFile path patched
+
+/-- Patch all `diagnosticsOffFiles ++ extra`. -/
+def patchDiagnosticsOffFiles (extra : Array FilePath := #[]) : IO Unit := do
+  for p in diagnosticsOffFiles ++ extra do patchOneFile p
+
+/-! ## Build-log parser -/
+
+structure DiagRecord where
+  file     : String
+  decl     : String
+  count    : Nat
+  category : String
+  deriving Inhabited
+
+private def diagToJsonLine (r : DiagRecord) : String :=
+  "{\"file\":\"" ++ r.file ++ "\",\"decl\":\"" ++ r.decl ++
+  "\",\"count\":" ++ toString r.count ++
+  ",\"category\":\"" ++ r.category ++ "\"}"
+
+private def categoryShort (tag label : String) : Option String :=
+  match tag, label with
+  | "reduction", "unfolded declarations"           => some "reduction/unfolded"
+  | "reduction", "unfolded instances"              => some "reduction/instances"
+  | "reduction", "unfolded reducible declarations" => some "reduction/reducible"
+  | "kernel",    "unfolded declarations"           => some "kernel/unfolded"
+  | "type_class","used instances"                  => some "type_class/used"
+  | _, _ => none
+
+private def targetToFile (target : String) : Option String :=
+  if target.contains ':' then none
+  else some (target.replace "." "/" ++ ".lean")
+
+/-- Match `✔ [N/M] Built Mathlib.Foo.Bar` and friends; return the target. -/
+private def parseBuiltLine (line : String) : Option String := Id.run do
+  -- Accept any of ✔ ℹ ⚠ ✖ as the leading bullet. Cheap precheck.
+  unless line.startsWith "✔" || line.startsWith "ℹ" ||
+         line.startsWith "⚠" || line.startsWith "✖" do return none
+  let parts : List String := line.splitOn "Built "
+  unless parts.length ≥ 2 do return none
+  let after : String := parts[1]!
+  -- `Mathlib.Foo` then optional whitespace; take up to first space.
+  let target : String :=
+    (after.takeWhile (fun c => c != ' ' && c != '\t' && c != '\n')).toString
+  return some target
+
+/-- Strip a literal `[tag] ` prefix; on success return `(tag, rest)`. -/
+private def stripTagPrefix (s : String) : Option (String × String) := Id.run do
+  unless s.startsWith "[" do return none
+  for tag in ["reduction", "kernel", "type_class"] do
+    let p := "[" ++ tag ++ "] "
+    if s.startsWith p then
+      let rest : String := s.drop p.length |>.toString
+      return some (tag, rest)
+  return none
+
+/-- `[reduction] unfolded declarations (max: N, num: M):` -/
+private def parseCategoryHeader (line : String) : Option (String × String) := Id.run do
+  let trimmed : String := line.trimAscii.toString
+  let some (tag, rest) := stripTagPrefix trimmed | none
+  unless line.endsWith ":" do return none
+  -- `rest` is `<label> (max: ..., num: ...):`
+  let parenParts : List String := rest.splitOn " ("
+  unless parenParts.length ≥ 2 do return none
+  let label : String := parenParts[0]!
+  return some (tag, label)
+
+/-- `    [reduction] Foo.bar ↦ 3` -/
+private def parseEntry (line : String) : Option (String × String × Nat) := Id.run do
+  let trimmed : String := line.trimAscii.toString
+  let some (tag, rest) := stripTagPrefix trimmed | none
+  let arrowParts : List String := rest.splitOn " ↦ "
+  unless arrowParts.length == 2 do return none
+  let decl : String := arrowParts[0]!
+  let countRaw : String := arrowParts[1]!
+  let countStr : String := countRaw.trimAscii.toString
+  let some count := String.toNat? countStr | none
+  return some (tag, decl, count)
+
+/-- Scan log into `(file, decl, count, category)` records in memory. -/
+def parseLogToRecords (logPath : FilePath) : IO (Array DiagRecord) := do
+  let raw ← IO.FS.readFile logPath
+  let lines := raw.splitOn "\n"
+  let mut currentFile : Option String := none
+  let mut currentCategory : Option String := none
+  let mut out : Array DiagRecord := #[]
+  for line in lines do
+    if let some target := parseBuiltLine line then
+      currentFile := targetToFile target
+      currentCategory := none
+      continue
+    if let some (tag, label) := parseCategoryHeader line then
+      currentCategory := categoryShort tag label
+      continue
+    if let some (tag, decl, count) := parseEntry line then
+      if let some cat := currentCategory then
+        if cat.startsWith tag then
+          if let some f := currentFile then
+            out := out.push { file := f, decl := decl, count := count, category := cat }
+          continue
+        else
+          currentCategory := none
+          continue
+    if !line.isEmpty && !line.startsWith " " then
+      currentCategory := none
+  return out
+
+/-- Parse `logPath` and write `outPath` with one JSONL record per
+(file, decl, count, category). -/
+def parseLog (logPath outPath : FilePath) : IO Nat := do
+  let records ← parseLogToRecords logPath
+  IO.FS.withFile outPath .write fun h => do
+    for r in records do h.putStrLn (diagToJsonLine r)
+  return records.size
+
+/-! ## Build runner -/
+
+/-- Run `lake build Mathlib`, streaming output to `logPath` (and stdout).
+Returns the lake exit code. -/
+def runBuild (logPath : FilePath) : IO UInt32 := do
+  IO.FS.createDirAll logPath.parent.get!
+  let proc ← IO.Process.spawn {
+    cmd := "lake"
+    args := #["build", "Mathlib"]
+    stdout := .piped
+    stderr := .piped
+  }
+  -- Tee stdout+stderr to logPath.
+  IO.FS.withFile logPath .write fun h => do
+    let outTask ← IO.asTask <| do
+      let mut acc : String := ""
+      while true do
+        let line ← proc.stdout.getLine
+        if line.isEmpty then break
+        IO.print line
+        h.putStr line
+        acc := acc ++ line
+      return acc
+    let errTask ← IO.asTask <| do
+      while true do
+        let line ← proc.stderr.getLine
+        if line.isEmpty then break
+        IO.eprint line
+        h.putStr line
+      return ()
+    let _ ← IO.wait outTask
+    let _ ← IO.wait errTask
+    pure ()
+  let rc ← proc.wait
+  return rc
+
+/-- Top-level diagnostics collection: patch, build, parse. Restores via
+`Restore.withBackups`-like discipline (callers should use
+`withBackups`). -/
+def runDiagnostics (lakefilePath : FilePath) (extraOffFiles : Array FilePath := #[]) :
+    IO UInt32 := do
+  IO.FS.createDirAll dataDir
+  patchLakefile lakefilePath
+  patchDiagnosticsOffFiles extraOffFiles
+  let rc ← runBuild buildLogPath
+  -- Parse regardless (partial logs are still useful).
+  let n ← parseLog buildLogPath diagnosticsPath
+  IO.eprintln s!"[no_expose diagnostics] wrote {n} records to {diagnosticsPath}"
+  restoreAll
+  return rc
+
+end NoExpose
diff --git a/scripts/NoExpose/Edit.lean b/scripts/NoExpose/Edit.lean
new file mode 100644
index 00000000000000..d969714345775a
--- /dev/null
+++ b/scripts/NoExpose/Edit.lean
@@ -0,0 +1,629 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lean.Parser.Module
+import NoExpose.Cli
+import NoExpose.Paths
+import NoExpose.Report
+
+/-!
+# `NoExpose.Edit` — apply `@[expose]` removals to source files
+
+The user-facing core. For each target file:
+
+1. **Read** the report to find this file's safe-to-unexpose and
+   needed-downstream decls.
+2. **Detect strategy**: pick `section` if the file has
+   `@[expose] public section`; otherwise `individual`.
+3. **Compute edits** (text-level, deliberately not full Lean parse):
+   * `section`: drop `@[expose] ` from the section line, then prepend
+     `@[expose]` to each needed-downstream decl line.
+   * `individual`: for each safe-to-unexpose decl, drop `@[expose]`
+     from its attribute list. Only single-attribute lines are handled;
+     multi-attribute lines are skipped with a logged diagnostic.
+4. **Safety checks**:
+   * stale-data check: report.jsonl mtime ≥ source mtime
+   * clean-tree check: `git status --porcelain PATH` is empty
+5. **Apply** unless `--dry-run`.
+6. **Audit trail** (apply-only): append a `git apply`-compatible unified
+   diff to `scripts/.no_expose/edits.patch`. `--dry-run` prints the same
+   diff to stdout but does not touch the audit file.
+7. **Verify** (apply-only, `--verify`): re-run `lake build` on the
+   touched module and roll back the edit on non-zero exit.
+-/
+
+open System
+
+namespace NoExpose
+
+/-! ## Source-file location helpers -/
+
+/-- Strategy used for a particular file. -/
+inductive Strategy where
+  | section_   : Strategy
+  | individual : Strategy
+  deriving Repr, DecidableEq
+
+/-- Section strategy if any record carries a `sectionLine`, otherwise
+individual. -/
+private def chooseStrategy (records : Array ReportRecord) : Strategy :=
+  if records.any (·.sectionLine.isSome) then .section_
+  else .individual
+
+/-! ## Section-strategy edit
+
+Algorithm:
+1. Find the line `@[expose] public section`. Replace with `public section`.
+2. For each needed-downstream decl in the file (sorted by line desc, so
+   line numbers stay valid), insert a new line `@[expose]` *above* it.
+   "Above" means: insert before the first preceding line that is the
+   start of the decl's declaration block (skipping `@[...]` attribute
+   lines and `/-- ... -/` doccomments).
+-/
+
+/-- Starting at `idx` (0-based, pointing into the "decl block" — doc
+comments, attribute lines, or the decl keyword itself), advance past
+blank lines, doc comments and attribute blocks (single or multi-line)
+until we reach the line containing the decl keyword (`def`,
+`theorem`, `instance`, `abbrev`, …). Returns that line's index. -/
+private partial def declKeywordLineFrom
+    (lines : Array String) (idx : Nat) : Nat := Id.run do
+  let mut i := idx
+  while i < lines.size do
+    let line : String := lines[i]!
+    let trimmed : String := line.trimAscii.toString
+    if trimmed.isEmpty then
+      i := i + 1
+    else if trimmed.startsWith "/--" then
+      if trimmed.endsWith "-/" && trimmed.length > "/----/".length then
+        i := i + 1
+      else
+        i := i + 1
+        while i < lines.size do
+          let l2 := (lines[i]!).trimAscii.toString
+          i := i + 1
+          if l2.endsWith "-/" then break
+    else if trimmed.startsWith "@[" then
+      -- Multi-line `@[...]` blocks (e.g. `@[to_dual (attr := simps)
+      -- /-- doc -/]` spanning two lines) close with a line ending in
+      -- `]`. Without this branch the walker would misread the embedded
+      -- `/--` on the close-line as a standalone doc-comment and
+      -- overshoot the decl.
+      if trimmed.endsWith "]" then
+        i := i + 1
+      else
+        i := i + 1
+        while i < lines.size do
+          let l2 := (lines[i]!).trimAscii.toString
+          i := i + 1
+          if l2.endsWith "]" then break
+    else
+      break
+  return i
+
+/-- Find the contiguous `@[...]` attribute block immediately before
+the decl-keyword line at `declIdx`. Returns `(blockStart, blockEnd)`
+as 0-based line indices (inclusive on both ends), or `none` if no
+attribute block precedes the decl. Lean's `declModifiers` grammar
+requires doc-comment → attribute → decl in that order, so the
+attribute (if present) must sit on the line immediately before the
+decl-keyword line. We bound the upward walk for the `@[` opener to a
+fixed window so we can never match a `]` in an unrelated earlier
+line's content. -/
+private partial def attrBlockBefore (lines : Array String) (declIdx : Nat) :
+    Option (Nat × Nat) := Id.run do
+  if declIdx == 0 then return none
+  let endLine := declIdx - 1
+  let endTrim := (lines[endLine]!).trimAscii.toString
+  -- The line immediately before the decl must end with `]`, otherwise
+  -- there is no attribute block here.
+  if endTrim.isEmpty || !endTrim.endsWith "]" then return none
+  -- Single-line attribute: opener and closer are the same line.
+  if endTrim.startsWith "@[" then return some (endLine, endLine)
+  -- Multi-line attribute: walk upward (bounded) for the line that
+  -- *opens* this block with `@[`. The intermediate lines are part of
+  -- the attribute body and can contain anything (including embedded
+  -- `/-- doc -/`), so we don't filter on content — but we do bound
+  -- the walk and require that no intermediate line itself ends with
+  -- `]` (which would belong to a different, prior block).
+  let lowerBound := if endLine ≥ 10 then endLine - 10 else 0
+  let mut k := endLine
+  while k > lowerBound do
+    k := k - 1
+    let t := (lines[k]!).trimAscii.toString
+    if t.startsWith "@[" then return some (k, endLine)
+    if t.endsWith "]" then return none
+  return none
+
+/-- Inside `body` (an `@[...]` block body), locate the
+`(attr := …)` clause and return `(before, attrsList, after)` where
+`before ++ "(attr := " ++ attrsList ++ ")" ++ after == body`. Returns
+`none` if there is no `(attr := …)` clause. -/
+private def splitAttrClause (body : String) : Option (String × String × String) := Id.run do
+  let needle := "(attr := "
+  let parts := body.splitOn needle
+  if parts.length < 2 then return none
+  let before := parts[0]!
+  let after := String.intercalate needle (parts.drop 1)
+  -- Find the matching `)` for the opening paren.
+  let bytes := after.toUTF8
+  let n := bytes.size
+  let mut depth : Nat := 1
+  let mut i : Nat := 0
+  while i < n do
+    let b := bytes[i]!
+    if b == 0x28 then depth := depth + 1            -- '('
+    else if b == 0x29 then                          -- ')'
+      depth := depth - 1
+      if depth == 0 then break
+    i := i + 1
+  if depth != 0 then return none
+  let attrsList := String.fromUTF8! (bytes.extract 0 i)
+  let rest      := String.fromUTF8! (bytes.extract (i + 1) n)
+  return some (before, attrsList, rest)
+
+/-- True iff a comma-separated attribute list `s` already contains
+`expose` as one of its tokens. -/
+private def attrListHasExpose (s : String) : Bool := Id.run do
+  for tok in s.splitOn "," do
+    if tok.trimAscii.toString == "expose" then return true
+  return false
+
+/-- Apply the section strategy. Returns the new file contents (or
+`none` to indicate "no changes needed"). -/
+def applySectionStrategy (text : String) (neededDownstream : Array Nat) :
+    Option String := Id.run do
+  let lines := (text.splitOn "\n").toArray
+  -- Step 1: rewrite the section line.
+  let mut sectionRewritten := false
+  let mut newLines : Array String := #[]
+  for line in lines do
+    let trimmed := line.trimAscii.toString
+    if !sectionRewritten && trimmed.startsWith "@[expose] public section" then
+      sectionRewritten := true
+      let leading : String := (line.takeWhile Char.isWhitespace).toString
+      let rest : String :=
+        (line.drop (leading.length + "@[expose] public section".length)).toString
+      newLines := newLines.push (leading ++ "public section" ++ rest)
+    else
+      newLines := newLines.push line
+  unless sectionRewritten do return none
+  -- Step 2: re-apply `@[expose]` to each needed-downstream decl.
+  -- Process highest line first so earlier indices stay valid. Three
+  -- placement strategies depending on what attribute block already
+  -- exists on the decl:
+  --   1. None             → insert `@[expose]` on its own new line.
+  --   2. Plain attributes → merge into the block: `@[X]` → `@[X, expose]`.
+  --   3. Propagator macro (`to_dual`/`to_additive`) → modify the
+  --      macro's `(attr := …)` clause so the macro applies `@[expose]`
+  --      to both source and twin.
+  -- Stacked attribute blocks (`@[expose]\n@[X]`) are a Lean syntax
+  -- error — `declModifiers` only accepts one `@[…]` block per decl.
+  let sortedDesc := neededDownstream.qsort (· > ·)
+  -- Multiple records can resolve to the same decl-keyword line (e.g.
+  -- the `to_dual` twin and the source decl both report a position
+  -- inside the same source decl block). Track which declIdx values
+  -- we've already touched so we don't inject twice.
+  let mut seen : Std.HashSet Nat := {}
+  for declLine in sortedDesc do
+    if declLine == 0 then continue
+    let blockStart := declLine - 1
+    if blockStart ≥ newLines.size then continue
+    let declIdx := declKeywordLineFrom newLines blockStart
+    if declIdx == 0 || declIdx ≥ newLines.size then continue
+    if seen.contains declIdx then continue
+    seen := seen.insert declIdx
+    match attrBlockBefore newLines declIdx with
+    | none =>
+      -- Case 1: no existing attribute block. Insert on a new line.
+      let declLineStr := newLines[declIdx]!
+      let leading := (declLineStr.takeWhile Char.isWhitespace).toString
+      newLines := newLines.insertIdx! declIdx (leading ++ "@[expose]")
+    | some (openIdx, closeIdx) =>
+      -- Concatenate the block body (between `@[` and `]`) across lines.
+      let mut body : String := ""
+      for k in [openIdx:closeIdx + 1] do
+        let t := (newLines[k]!).trimAscii.toString
+        let chunk := if k == openIdx then t.drop 2 |>.toString else t
+        let chunk := if k == closeIdx then chunk.dropEnd 1 |>.toString else chunk
+        body := if body.isEmpty then chunk else body ++ " " ++ chunk
+      -- Already-exposed: skip. We check both the outer attribute
+      -- list (for top-level `expose`) and the inner `(attr := ...)`
+      -- clause (for macros like `to_dual`/`to_additive` that
+      -- propagate exposure to their twin).
+      let outerHasExpose :=
+        body == "expose" || body.startsWith "expose " || body.startsWith "expose," ||
+        (body.splitOn ", expose").length > 1 || (body.splitOn ",expose").length > 1
+      let innerHasExpose := match splitAttrClause body with
+        | some (_, attrsList, _) => attrListHasExpose attrsList
+        | none                   => false
+      if outerHasExpose || innerHasExpose then continue
+      -- Append `, expose` to the outer attribute list. `@[expose]` is
+      -- consumed at decl elaboration, so it must sit in the decl's
+      -- modifier list (not in `(attr := …)`, which would try to apply
+      -- it post-hoc — Lean's expose attribute rejects that).
+      -- For propagator macros (`to_dual` / `to_additive`), the macro
+      -- already re-exposes the twin when the source is exposed (see
+      -- `Mathlib.Tactic.Translate.Core` ~line 784), so we don't need
+      -- to touch `(attr := …)`.
+      let newBody := body ++ ", expose"
+      -- Replace lines [openIdx..closeIdx] with a single rebuilt line.
+      let leading := ((newLines[openIdx]!).takeWhile Char.isWhitespace).toString
+      let rebuilt := leading ++ "@[" ++ newBody ++ "]"
+      newLines := newLines.set! openIdx rebuilt
+      for _ in [openIdx + 1:closeIdx + 1] do
+        newLines := newLines.eraseIdx! (openIdx + 1)
+  return some (String.intercalate "\n" newLines.toList)
+
+/-! ## Individual-strategy edit
+
+For each safe-to-unexpose decl on a recorded line, look for an
+`@[expose]` attribute on or above the decl line and remove it. Only
+two shapes are handled:
+
+* `@[expose]` on its own line → delete the entire line.
+* Decl line is `@[expose] def foo …` → strip the `@[expose] ` prefix
+  (only if it's the *only* attribute on the line).
+
+Anything else (multi-attribute `@[expose, simp]`, splits across lines
+in unusual ways) is skipped with a diagnostic. -/
+
+/-- Why an individual-strategy strip was skipped. -/
+inductive SkipReason where
+  /-- No `@[expose]` on or directly above the decl line — likely
+  exposed via an enclosing `public meta section` or similar. -/
+  | noAttribute
+  /-- `@[expose]` is present but bundled with other attributes
+  (e.g. `@[expose, simp]`); the tool doesn't unbundle. -/
+  | multiAttribute
+  deriving Repr, BEq
+
+def SkipReason.toString : SkipReason → String
+  | .noAttribute    => "no `@[expose]` attribute found (likely inside a `public meta section`)"
+  | .multiAttribute => "`@[expose]` bundled with other attributes; unbundling not implemented"
+
+/-- Strip `@[expose]` from a single-attribute occurrence around `line`
+(0-based index into `lines`). Returns `Except SkipReason (Array String)`:
+the updated lines on success, or the reason we couldn't edit. -/
+private def stripIndividualOne (lines : Array String) (lineIdx : Nat) :
+    Except SkipReason (Array String) := Id.run do
+  if lineIdx ≥ lines.size then return .error .noAttribute
+  let line := lines[lineIdx]!
+  let trimmed := line.trimAscii.toString
+  -- Case A: `@[expose] decl ...` on the same line, single attribute.
+  if trimmed.startsWith "@[expose] " then
+    let leading := line.takeWhile Char.isWhitespace |>.toString
+    let rest := (line.drop (leading.length + "@[expose] ".length)).toString
+    return .ok (lines.set! lineIdx (leading ++ rest))
+  -- Case B: previous line is exactly `@[expose]` (with optional whitespace).
+  if lineIdx > 0 then
+    let prev := lines[lineIdx - 1]!
+    if prev.trimAscii.toString == "@[expose]" then
+      return .ok (lines.eraseIdx! (lineIdx - 1))
+  -- Case C: `@[expose, ...]` or `@[..., expose, ...]` on the decl line
+  -- or directly above — present but bundled.
+  let containsExpose (s : String) : Bool :=
+    s.startsWith "@[expose," || s.startsWith "@[expose ," ||
+    (s.splitOn ", expose").length > 1 || (s.splitOn ",expose").length > 1
+  if containsExpose trimmed then return .error .multiAttribute
+  if lineIdx > 0 then
+    let prevTrim := (lines[lineIdx - 1]!).trimAscii.toString
+    if prevTrim.startsWith "@[" && containsExpose prevTrim then
+      return .error .multiAttribute
+  return .error .noAttribute
+
+/-- Apply the individual strategy. Returns the new contents and a list
+of `(line, reason)` pairs for decls we couldn't safely edit. -/
+def applyIndividualStrategy (text : String) (safe : Array Nat) :
+    String × Array (Nat × SkipReason) := Id.run do
+  let mut lines := (text.splitOn "\n").toArray
+  let mut skipped : Array (Nat × SkipReason) := #[]
+  -- Process highest line first so index shifts don't matter.
+  let sortedDesc := safe.qsort (· > ·)
+  for declLine in sortedDesc do
+    if declLine == 0 then continue
+    let idx := declLine - 1
+    match stripIndividualOne lines idx with
+    | .ok lines'  => lines := lines'
+    | .error r    => skipped := skipped.push (declLine, r)
+  return (String.intercalate "\n" lines.toList, skipped)
+
+/-! ## Safety checks -/
+
+/-- Compare modification times: ok if `report` is at least as new as `source`. -/
+private def checkStaleness (sourcePath reportPath : FilePath) : IO Bool := do
+  let srcTime := (← sourcePath.metadata).modified
+  let rptTime := (← reportPath.metadata).modified
+  return rptTime ≥ srcTime
+
+/-- True if the working tree for `path` has no uncommitted changes. -/
+private def isCleanInGit (path : FilePath) : IO Bool := do
+  let out ← IO.Process.output {
+    cmd := "git", args := #["status", "--porcelain", path.toString] }
+  return out.stdout.trimAscii.toString == ""
+
+/-! ## Parse validation + lake-build verify -/
+
+/-- Count parse errors in `text` at the syntax level only (no
+elaboration). Cheap — only `Init` is in scope, so Mathlib-defined
+notations produce false positives. Callers should use this
+*differentially* (compare before/after) rather than absolutely. -/
+unsafe def countParseErrors (file : System.FilePath) (text : String) :
+    IO Nat := do
+  Lean.initSearchPath (← Lean.findSysroot)
+  let env ← Lean.importModules #[{ module := `Init }] {}
+  let inputCtx := Lean.Parser.mkInputContext text file.toString
+  let (_, mps, msgs) ← Lean.Parser.parseHeader inputCtx
+  let pmctx : Lean.Parser.ParserModuleContext := { env, options := {} }
+  let mut state := mps
+  let mut messages := msgs
+  repeat
+    let (stx, state', msgs') := Lean.Parser.parseCommand inputCtx pmctx state messages
+    state := state'
+    messages := msgs'
+    if Lean.Parser.isTerminalCommand stx then break
+  return messages.toList.foldl (init := 0) fun n m =>
+    if m.severity == .error then n + 1 else n
+
+/-- Convert `Mathlib/Foo/Bar.lean` to the module name `Mathlib.Foo.Bar`. -/
+private def fileToModule (path : System.FilePath) : String :=
+  let s := path.toString
+  let stripped : String :=
+    if s.endsWith ".lean" then (s.dropEnd 5).toString else s
+  stripped.replace "/" "."
+
+/-- Run `lake build <module>` for the touched file. Returns the exit code. -/
+def verifyByLakeBuild (file : System.FilePath) : IO UInt32 := do
+  let mod := fileToModule file
+  IO.eprintln s!"[no_expose edit] verifying: lake build {mod}"
+  let proc ← IO.Process.spawn {
+    cmd := "lake", args := #["build", mod]
+    stdout := .inherit, stderr := .inherit }
+  proc.wait
+
+/-! ## Unified-diff rendering
+
+A standard LCS-based line diff with `git apply`-compatible hunk headers
+(`@@ -A,B +C,D @@`). Used for both the on-screen `--dry-run` preview and
+the persisted audit trail at `scripts/.no_expose/edits.patch`. -/
+
+private inductive DiffOp where
+  | keep (line : String)
+  | del  (line : String)
+  | ins  (line : String)
+  deriving Inhabited
+
+/-- Split on `"\n"` and drop the trailing empty element produced by a
+final newline, so that "a\nb\n" yields `#["a", "b"]` (two lines, not
+three). -/
+private def splitIntoLines (s : String) : Array String :=
+  let xs := (s.splitOn "\n").toArray
+  if xs.size > 0 && xs[xs.size - 1]! == "" then xs.pop else xs
+
+/-- Line-level LCS diff. O(m·n) time and memory; fine for the file
+sizes `no_expose` edits (mathlib files are at most a few thousand
+lines). -/
+private def diffOps (old new : Array String) : Array DiffOp := Id.run do
+  let m := old.size
+  let n := new.size
+  let w := n + 1
+  -- Flat (m+1) × (n+1) LCS-length table.
+  let mut t : Array Nat := Array.replicate ((m+1) * w) 0
+  for i in [:m] do
+    for j in [:n] do
+      let v :=
+        if old[i]! == new[j]! then
+          t[i*w + j]! + 1
+        else
+          Nat.max t[i*w + (j+1)]! t[(i+1)*w + j]!
+      t := t.set! ((i+1)*w + (j+1)) v
+  -- Backtrack from (m, n).
+  let mut ops : Array DiffOp := #[]
+  let mut i := m
+  let mut j := n
+  while i > 0 || j > 0 do
+    if i > 0 && j > 0 && old[i-1]! == new[j-1]! then
+      ops := ops.push (.keep old[i-1]!)
+      i := i - 1; j := j - 1
+    else if j > 0 && (i == 0 || t[i*w + (j-1)]! ≥ t[(i-1)*w + j]!) then
+      ops := ops.push (.ins new[j-1]!)
+      j := j - 1
+    else
+      ops := ops.push (.del old[i-1]!)
+      i := i - 1
+  return ops.reverse
+
+private structure Hunk where
+  oldStart : Nat
+  newStart : Nat
+  oldLen : Nat
+  newLen : Nat
+  lines : Array String  -- each prefixed by ' ', '-', or '+'
+
+/-- Group diff ops into hunks with `context` lines of unchanged context
+around each run of changes. Adjacent runs whose contexts touch are
+merged into a single hunk. -/
+private def buildHunks (ops : Array DiffOp) (context : Nat := 3) : Array Hunk := Id.run do
+  let n := ops.size
+  if n == 0 then return #[]
+  -- Mark each op that is within `context` positions of a non-keep op.
+  let mut inHunk : Array Bool := Array.replicate n false
+  for k in [:n] do
+    match ops[k]! with
+    | .keep _ => pure ()
+    | _ =>
+      let lo := if k ≥ context then k - context else 0
+      let hi := Nat.min n (k + context + 1)
+      for p in [lo:hi] do
+        inHunk := inHunk.set! p true
+  -- Walk, emitting one hunk per maximal run of inHunkd ops.
+  let mut hunks : Array Hunk := #[]
+  let mut oldLine : Nat := 1
+  let mut newLine : Nat := 1
+  let mut k : Nat := 0
+  while k < n do
+    if !inHunk[k]! then
+      match ops[k]! with
+      | .keep _ => oldLine := oldLine + 1; newLine := newLine + 1
+      | .del _ => oldLine := oldLine + 1
+      | .ins _ => newLine := newLine + 1
+      k := k + 1
+    else
+      let hOldStart := oldLine
+      let hNewStart := newLine
+      let mut hLines : Array String := #[]
+      let mut hOldLen := 0
+      let mut hNewLen := 0
+      while k < n && inHunk[k]! do
+        match ops[k]! with
+        | .keep s =>
+          hLines := hLines.push (" " ++ s)
+          oldLine := oldLine + 1; newLine := newLine + 1
+          hOldLen := hOldLen + 1; hNewLen := hNewLen + 1
+        | .del s =>
+          hLines := hLines.push ("-" ++ s)
+          oldLine := oldLine + 1
+          hOldLen := hOldLen + 1
+        | .ins s =>
+          hLines := hLines.push ("+" ++ s)
+          newLine := newLine + 1
+          hNewLen := hNewLen + 1
+        k := k + 1
+      hunks := hunks.push ⟨hOldStart, hNewStart, hOldLen, hNewLen, hLines⟩
+  return hunks
+
+private def formatHunkHeader (h : Hunk) : String :=
+  -- For pure insertions/deletions, the conventional start in unified
+  -- diff is the line *before* the change (or 0 at file start).
+  let oldStart := if h.oldLen == 0 && h.oldStart > 0 then h.oldStart - 1 else h.oldStart
+  let newStart := if h.newLen == 0 && h.newStart > 0 then h.newStart - 1 else h.newStart
+  s!"@@ -{oldStart},{h.oldLen} +{newStart},{h.newLen} @@"
+
+/-- Render a `git apply`-compatible unified diff for a single file. -/
+private def renderUnifiedDiff (filePath : String) (oldText newText : String) : String := Id.run do
+  let oldLines := splitIntoLines oldText
+  let newLines := splitIntoLines newText
+  let ops := diffOps oldLines newLines
+  let hunks := buildHunks ops
+  if hunks.isEmpty then return ""
+  let mut acc : String := s!"--- a/{filePath}\n+++ b/{filePath}\n"
+  for h in hunks do
+    acc := acc ++ formatHunkHeader h ++ "\n"
+    for line in h.lines do
+      acc := acc ++ line ++ "\n"
+  return acc
+
+/-! ## Top-level driver -/
+
+/-- Apply edits to a single file. Returns `true` if the file was
+modified (or would be, in dry-run mode). -/
+unsafe def editOneFile (file : FilePath) (records : Array ReportRecord)
+    (args : EditArgs) (auditAccum : IO.Ref String) : IO Bool := do
+  unless ← System.FilePath.pathExists file do
+    IO.eprintln s!"no_expose edit: {file} does not exist; skipping"
+    return false
+  -- Safety: clean tree.
+  unless args.forceDirty do
+    if !(← isCleanInGit file) then
+      IO.eprintln s!"no_expose edit: {file} has uncommitted changes; \
+        pass --force-dirty to override."
+      return false
+  -- Safety: stale data.
+  unless args.forceStale do
+    if !(← checkStaleness file reportPath) then
+      IO.eprintln s!"no_expose edit: {file} is newer than {reportPath}; \
+        re-run `collect` or pass --force-stale."
+      return false
+  let originalText ← IO.FS.readFile file
+  -- Dedupe by line: `to_additive` (and similar) macros produce multiple
+  -- report rows that all point at the same source line. Each line should
+  -- get at most one edit.
+  let dedupe (xs : Array Nat) : Array Nat :=
+    let init : Array Nat × Std.HashSet Nat := (#[], {})
+    (xs.foldl (init := init) fun (acc, seen) x =>
+      if seen.contains x then (acc, seen) else (acc.push x, seen.insert x)).1
+  let neededDownstreamLines : Array Nat := dedupe (records
+    |>.filter (Verdict.classify · == .neededDownstream) |>.map (·.line))
+  -- A source line is only safe to unexpose if EVERY record at that
+  -- line is safe — i.e. no twin (`to_additive`/`to_dual`) is needed
+  -- downstream.
+  let neededSet : Std.HashSet Nat := neededDownstreamLines.foldl (·.insert ·) {}
+  let safeLines : Array Nat := dedupe (records
+    |>.filter (Verdict.classify · == .safeToUnexpose) |>.map (·.line))
+    |>.filter (fun ln => !neededSet.contains ln)
+  let strategy := chooseStrategy records
+  let (newText, skipped) : String × Array (Nat × SkipReason) ← do
+    match strategy with
+    | .section_ => do
+      match applySectionStrategy originalText neededDownstreamLines with
+      | some t => pure (t, #[])
+      | none => do
+        IO.eprintln s!"no_expose edit: {file}: section strategy chosen but \
+          no `@[expose] public section` line found; skipping."
+        pure (originalText, #[])
+    | .individual => pure (applyIndividualStrategy originalText safeLines)
+  for (ln, reason) in skipped do
+    IO.eprintln s!"  {file}:{ln}: {reason.toString}"
+  if newText == originalText then
+    IO.println s!"{file}: no changes."
+    return false
+  let diff := renderUnifiedDiff file.toString originalText newText
+  -- Parse-validate (differential): the edited text must not introduce
+  -- new syntax errors over the original. False positives from
+  -- Mathlib-only notation cancel out.
+  let oldErrCount ← countParseErrors file originalText
+  let newErrCount ← countParseErrors file newText
+  if newErrCount > oldErrCount then
+    IO.eprintln s!"no_expose edit: {file}: edit introduced {newErrCount - oldErrCount} \
+      new parse error(s); refusing to write."
+    return false
+  if args.dryRun then
+    IO.println s!"{file}: would modify (dry-run; pass without --dry-run to apply)."
+    IO.print diff
+    return true
+  -- Persisted audit trail (apply-only).
+  auditAccum.modify (· ++ diff)
+  IO.FS.writeFile file newText
+  IO.println s!"{file}: applied edits."
+  if args.verify then
+    let rc ← verifyByLakeBuild file
+    if rc != 0 then
+      IO.eprintln s!"no_expose edit: {file}: lake build failed (exit {rc}); \
+        rolling back."
+      IO.FS.writeFile file originalText
+      return false
+    IO.println s!"{file}: verify ok."
+  return true
+
+/-- Top-level `edit` subcommand. -/
+unsafe def runEdit (args : EditArgs) : IO UInt32 := do
+  unless ← System.FilePath.pathExists reportPath do
+    IO.eprintln s!"no_expose edit: {reportPath} not found; \
+      run `lake exe no_expose collect` first."
+    return 2
+  let (records, errs) ← readReport reportPath
+  for e in errs do IO.eprintln s!"warning: {e}"
+  let groups := byFile records
+  if args.paths.isEmpty then
+    IO.eprintln "no_expose edit: pass at least one PATH"
+    return 2
+  let auditAccum ← IO.mkRef ""
+  let mut anyModified := false
+  for p in args.paths do
+    let recs := groups.getD p #[]
+    if recs.isEmpty then
+      IO.eprintln s!"{p}: no exposed decls in report"
+      continue
+    let modified ← editOneFile (FilePath.mk p) recs args auditAccum
+    if modified then anyModified := true
+  -- Append audit trail.
+  let auditBody ← auditAccum.get
+  if anyModified && !auditBody.isEmpty then
+    IO.FS.createDirAll dataDir
+    IO.FS.withFile editsPatchPath .append fun h => h.putStr auditBody
+    IO.eprintln s!"[no_expose edit] audit trail appended to {editsPatchPath}"
+  return 0
+
+end NoExpose
diff --git a/scripts/NoExpose/Env.lean b/scripts/NoExpose/Env.lean
new file mode 100644
index 00000000000000..3b66801e1a7647
--- /dev/null
+++ b/scripts/NoExpose/Env.lean
@@ -0,0 +1,274 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lean
+import NoExpose.Paths
+import NoExpose.SourceScan
+
+/-!
+# `NoExpose.Env` — env-walk pieces (enumeration + static refs)
+
+Three responsibilities, all running inside a `Lean.withImportModules`
+block opened by the `collect` orchestrator:
+
+* **enumerate**: emit one record per "candidate" decl in the project's
+  scope (a def whose body is in the exported view, isn't a compiler
+  helper, isn't an instance whose exposure is automatic).
+* **staticRefs**: per-(refModule, refName) cross-reference counts, with
+  a `theorem_count` split for same-module rfl detection.
+* **declRefs**: per-decl direct reference list, used downstream by
+  `Report` for one-hop transitive closure.
+
+This module does NOT `import Mathlib`; the exe links against just Lean
+core + Lake so it builds in seconds.
+-/
+
+open Lean Core
+
+namespace NoExpose
+
+/-- Run a `CoreM α` against a fresh `Environment` populated by
+importing `modules`. -/
+def withImportModules {α : Type} (modules : Array Name) (run : CoreM α)
+    (searchPath : Option SearchPath := none) (options : Options := {})
+    (trustLevel : UInt32 := 0) (fileName := "") :
+    IO α := unsafe do
+  if let some sp := searchPath then searchPathRef.set sp
+  Lean.withImportModules (modules.map ({ module := · })) options
+    (trustLevel := trustLevel) fun env => do
+      let ctx : Core.Context := { fileName, options, fileMap := default }
+      let state : Core.State := { env }
+      let (a, _) ← Core.CoreM.toIO run ctx state
+      pure a
+
+/-! ## Enumeration -/
+
+/-- One row of the eventual `exposed.jsonl`. Each record represents
+one source `@[expose]` occurrence intersected with one env decl whose
+range falls inside it. `name`/`module` come from the env (so we don't
+hand-parse identifiers); `line`/`col` are the decl's own start (used
+by `edit`). `attrLine` is the line of the `@[expose]` text that covers
+this decl; `sectionLine` is set iff the `@[expose]` came from a
+section attribute (and points at the `@[expose] section` line). -/
+structure DeclRecord where
+  name : String
+  kind : String
+  «module» : String
+  file : String
+  line : Nat
+  col : Nat
+  «effect» : String
+  attrLine : Nat
+  sectionLine : Option Nat := none
+  deriving Inhabited
+
+/-- Suffixes Lean uses for compiler-generated structure/inductive
+helpers; we exclude them since they aren't user-written `@[expose]`
+candidates. -/
+private def autoGenSuffixes : Array String := #[
+  "recOn", "casesOn", "brecOn", "binductionOn", "below", "ibelow", "ndrec",
+  "ndrecOn", "recAux", "rec", "noConfusion", "noConfusionType", "sizeOf",
+  "sizeOf_spec", "injEq"
+]
+
+/-- True if `name` is a compiler helper we should exclude from
+enumeration. -/
+def isAutoGen (env : Environment) (name : Name) : CoreM Bool := do
+  if Lean.isAuxRecursor env name then return true
+  if Lean.isNoConfusion env name then return true
+  if (env.getProjectionFnInfo? name).isSome then return true
+  if ← Lean.Meta.isMatcher name then return true
+  if let .str _ last := name then
+    if autoGenSuffixes.contains last then return true
+  return false
+
+/-- True if `name`'s body is in the *exported* view of `env`. -/
+def isBodyExported (env : Environment) (name : Name) : Bool :=
+  match (env.setExporting true).find? name with
+  | some info => info.hasValue
+  | none => false
+
+/-- Map `Mathlib.Foo.Bar` → `"Mathlib/Foo/Bar.lean"`. -/
+def moduleToPath (m : Name) : String :=
+  String.intercalate "/" (m.toString.splitOn ".") ++ ".lean"
+
+/-- Constant `name` lives in one of the project's modules — i.e. the
+declaring module's name has one of `scopePrefix` as a `Name`-prefix. -/
+private def isInScope (env : Environment) (scopePrefix : Array Name) (name : Name) :
+    Option Name := do
+  let idx ← env.getModuleIdxFor? name
+  let mod := env.header.moduleNames[idx]!
+  if scopePrefix.any fun p => p.isPrefixOf mod || p == mod then
+    some mod
+  else
+    none
+
+/-- Per-decl info we need to perform the source-occurrence × env-range
+intersection: the project file the decl came from, its name/kind/etc.,
+and the line range its declaration source spans. -/
+private structure EnvDecl where
+  name : Name
+  kind : String
+  «module» : Name
+  file : String
+  startLine : Nat
+  endLine : Nat
+  col : Nat
+  isAbbrev : Bool
+
+/-- Walk the env, returning every project-scope decl that could carry
+`@[expose]`. The source-occurrence scanner will pick out which of these
+are actually covered by an `@[expose]` attribute. -/
+private def collectEnvDecls (scopePrefix : Array Name) : CoreM (Array EnvDecl) := do
+  let env ← getEnv
+  let mut out : Array EnvDecl := #[]
+  for (name, info) in env.constants.toList do
+    let .defnInfo defnVal := info | continue
+    let some mod := isInScope env scopePrefix name | continue
+    if name.hasMacroScopes then continue
+    if name.isInternal then continue
+    if ← isAutoGen env name then continue
+    unless isBodyExported env name do continue
+    let some ranges ← Lean.findDeclarationRanges? name | continue
+    out := out.push {
+      name
+      kind := "def"
+      «module» := mod
+      file := moduleToPath mod
+      startLine := ranges.range.pos.line
+      endLine := ranges.range.endPos.line
+      col := ranges.range.pos.column
+      isAbbrev := defnVal.hints.isAbbrev
+    }
+  return out
+
+/-- Source-occurrence-driven enumeration: scan each project file for
+`@[expose]` text occurrences, intersect with env decl ranges, and emit
+one `DeclRecord` per (occurrence, covered env decl) pair.
+
+This replaces the previous "walk every body-exposed def, then classify
+how it got exposed" approach. The new approach is honest about what
+the tool can actually edit: by construction every record corresponds
+to a literal `@[expose]` in source. -/
+unsafe def enumerate (scopePrefix : Array Name) : CoreM (Array DeclRecord) := do
+  let envDecls ← collectEnvDecls scopePrefix
+  -- Group decls by their source file.
+  let mut byFile : Std.HashMap String (Array EnvDecl) := {}
+  for d in envDecls do
+    byFile := byFile.insert d.file ((byFile.getD d.file #[]).push d)
+  IO.eprintln s!"[no_expose enumerate] {envDecls.size} candidate env decls \
+    across {byFile.size} files"
+  -- For each file, scan source for `@[expose]` occurrences and
+  -- intersect with the env decls in that file.
+  let mut out : Array DeclRecord := #[]
+  let mut filesDone : Nat := 0
+  for (file, decls) in byFile do
+    let path : System.FilePath := file
+    unless ← System.FilePath.pathExists path do
+      filesDone := filesDone + 1
+      continue
+    let text ← IO.FS.readFile path
+    let occurrences := scanExposeOccurrences text
+    -- Sort decls once by startLine for cheap binary-search-style lookup.
+    let sortedDecls := decls.qsort fun a b => a.startLine < b.startLine
+    for occ in occurrences do
+      match occ.scope with
+      | .decl =>
+        -- The covered decl is the one whose range starts on the
+        -- next line after `occ.attrLine` (allowing for the decl's
+        -- modifiers spanning the attribute line itself).
+        for d in sortedDecls do
+          if d.startLine ≥ occ.attrLine && d.startLine ≤ occ.attrLine + 1 then
+            out := out.push (declRecordOf d occ.attrLine none)
+      | .section_ closeLine =>
+        for d in sortedDecls do
+          if d.startLine ≥ occ.attrLine && d.startLine ≤ closeLine then
+            out := out.push (declRecordOf d occ.attrLine (some occ.attrLine))
+    filesDone := filesDone + 1
+    if filesDone % 500 == 0 then
+      IO.eprintln s!"[no_expose enumerate] scanned {filesDone} files \
+        ({out.size} records so far)"
+  IO.eprintln s!"[no_expose enumerate] {out.size} records from {filesDone} files"
+  return out
+where
+  declRecordOf (d : EnvDecl) (attrLine : Nat) (sectionLine : Option Nat) :
+      DeclRecord := {
+    name := d.name.toString
+    kind := d.kind
+    «module» := d.module.toString
+    file := d.file
+    line := d.startLine
+    col := d.col
+    «effect» := if d.isAbbrev then "noop-always-exported" else "exposed"
+    attrLine
+    sectionLine
+  }
+
+/-! ## Static references -/
+
+/-- For each (referencing module, referenced name),
+`(total_count, theorem_count)`. -/
+abbrev RefMap := Std.HashMap (Nat × Name) (Nat × Nat)
+
+/-- Walk every constant in env; aggregate by (refModule, refName). -/
+def collectStaticRefs : CoreM RefMap := do
+  let env ← getEnv
+  let mut acc : RefMap := {}
+  for (name, info) in env.constants.toList do
+    let some refModIdx := env.getModuleIdxFor? name | continue
+    if name.hasMacroScopes then continue
+    if name.isInternal then continue
+    let isThm := info matches .thmInfo _
+    let refs := info.getUsedConstantsAsSet
+    acc := refs.foldl (init := acc) fun acc referenced =>
+      let key := (refModIdx, referenced)
+      let (cTot, cThm) := acc.getD key (0, 0)
+      acc.insert key (cTot + 1, if isThm then cThm + 1 else cThm)
+  return acc
+
+/-! ## JSON serialisation -/
+
+def DeclRecord.toJsonLine (d : DeclRecord) : String :=
+  let sectionField := match d.sectionLine with
+    | none   => ""
+    | some l => ",\"section_line\":" ++ toString l
+  "{\"name\":\"" ++ jsonEscape d.name ++
+  "\",\"kind\":\"" ++ d.kind ++
+  "\",\"module\":\"" ++ jsonEscape d.module ++
+  "\",\"file\":\"" ++ jsonEscape d.file ++
+  "\",\"line\":" ++ toString d.line ++
+  ",\"col\":" ++ toString d.col ++
+  ",\"effect\":\"" ++ d.effect ++
+  "\",\"attr_line\":" ++ toString d.attrLine ++
+  sectionField ++ "}"
+
+/-- Write a `RefMap` aggregation as one JSONL record per pair. -/
+def writeStaticRefs (env : Environment) (acc : RefMap)
+    (h : IO.FS.Handle) : IO Unit := do
+  for ((modIdx, decl), (count, thmCount)) in acc.toList do
+    let some mod := env.header.moduleNames[modIdx]? | continue
+    let file := moduleToPath mod
+    h.putStrLn <|
+      "{\"file\":\"" ++ jsonEscape file ++
+      "\",\"decl\":\"" ++ jsonEscape decl.toString ++
+      "\",\"count\":" ++ toString count ++
+      ",\"theorem_count\":" ++ toString thmCount ++
+      ",\"category\":\"static/ref\"}"
+
+/-- Write per-decl direct reference lists for transitive closure. -/
+def writeDeclRefs (env : Environment) (h : IO.FS.Handle) : IO Unit := do
+  for (name, info) in env.constants.toList do
+    if name.hasMacroScopes then continue
+    if name.isInternal then continue
+    if (env.getModuleIdxFor? name).isNone then continue
+    let refs := info.getUsedConstantsAsSet
+    if refs.isEmpty then continue
+    let body : String := String.intercalate "," <|
+      refs.foldl (init := []) (fun acc n => ("\"" ++ jsonEscape n.toString ++ "\"") :: acc)
+    h.putStrLn <|
+      "{\"decl\":\"" ++ jsonEscape name.toString ++
+      "\",\"refs\":[" ++ body ++ "]}"
+
+end NoExpose
diff --git a/scripts/NoExpose/Paths.lean b/scripts/NoExpose/Paths.lean
new file mode 100644
index 00000000000000..6ccd0660627568
--- /dev/null
+++ b/scripts/NoExpose/Paths.lean
@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lake.CLI.Main
+
+/-!
+# `NoExpose.Paths` — data-artifact paths and project autodetect
+
+Centralises every filesystem path the tool reads or writes, and the
+small piece of Lake-introspection that lets `no_expose` adapt to the
+current package (Mathlib, or a downstream Mathlib-using project).
+-/
+
+open Lake System
+
+namespace NoExpose
+
+/-- Root of the data directory the tool owns. Sibling of `lakefile.lean`. -/
+def dataDir : FilePath := "scripts" / ".no_expose"
+
+/-- Full Mathlib build log (raw `lake build` output). Several GB on a full
+collection; kept by default for debuggability. -/
+def buildLogPath : FilePath := dataDir / "build.log"
+
+/-- Per-file diagnostic-message records parsed from the build log. -/
+def diagnosticsPath : FilePath := dataDir / "diagnostics.jsonl"
+
+/-- One record per `@[expose]` def/instance the env walk found. -/
+def exposedPath : FilePath := dataDir / "exposed.jsonl"
+
+/-- Per-(refModule, refName) static reference counts (with theorem split). -/
+def staticRefsPath : FilePath := dataDir / "static_refs.jsonl"
+
+/-- Per-decl direct reference lists (used for one-hop transitive closure). -/
+def declRefsPath : FilePath := dataDir / "decl_refs.jsonl"
+
+/-- Joined report — the primary input to `report` and `edit`. -/
+def reportPath : FilePath := dataDir / "report.jsonl"
+
+/-- Audit trail for `edit` runs: unified diff of every change. -/
+def editsPatchPath : FilePath := dataDir / "edits.patch"
+
+/-- Where `Restore` writes original copies before patching the lakefile or
+fragile source files. Detected on every startup so an interrupted run
+can be recovered. -/
+def restoreDir : FilePath := dataDir / "restore"
+
+/-- Marker file: present iff a `collect` run is mid-flight (used by
+`Restore` to recognise crash recovery). -/
+def restoreStatePath : FilePath := restoreDir / "state.json"
+
+/-- Information about the current Lake package needed by the tool. -/
+structure ProjectInfo where
+  /-- The package name, e.g. `mathlib`. -/
+  name : Lean.Name
+  /-- The module names of the package's `lean_lib` targets that the tool
+  should treat as "owned by this project". For Mathlib this is
+  `[Mathlib, Archive, Counterexamples]` (we further filter to `Mathlib`
+  for normal use). For a downstream `MyProj`: `[MyProj]`. -/
+  libRoots : Array Lean.Name
+  /-- Source root directories the libs cover, used to map decl-source-files
+  back to "this project's files" vs imported deps. -/
+  srcDirs : Array System.FilePath
+  /-- The lakefile's path. May be `lakefile.lean` or `lakefile.toml`. -/
+  lakefilePath : System.FilePath
+
+/-- Inspect the current Lake workspace and produce a `ProjectInfo`. Mirrors
+`scripts/mk_all.lean:26` and `scripts/lint-style.lean:34`. -/
+def detectProjectInfo : IO ProjectInfo := do
+  let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
+  let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig
+    { elanInstall?, leanInstall?, lakeInstall? }
+  let some ws ← (Lake.loadWorkspace config).toBaseIO
+    | throw <| IO.userError "NoExpose: failed to load Lake workspace"
+  let pkg := ws.root
+  let libs := pkg.leanLibs.map fun lib => lib.config.name
+  let srcDirs := pkg.leanLibs.map fun lib => pkg.dir / lib.config.srcDir
+  let lakefilePath := pkg.dir / "lakefile.lean"
+  return {
+    name := pkg.baseName
+    libRoots := libs
+    srcDirs := srcDirs
+    lakefilePath
+  }
+
+/-- JSON-string-escape `s`. -/
+def jsonEscape (s : String) : String :=
+  s.foldl (init := "") fun acc c => acc ++
+    match c with
+    | '"'  => "\\\""
+    | '\\' => "\\\\"
+    | '\n' => "\\n"
+    | '\r' => "\\r"
+    | '\t' => "\\t"
+    | c    => c.toString
+
+end NoExpose
diff --git a/scripts/NoExpose/Report.lean b/scripts/NoExpose/Report.lean
new file mode 100644
index 00000000000000..fb36751e59515d
--- /dev/null
+++ b/scripts/NoExpose/Report.lean
@@ -0,0 +1,357 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lean.Data.Json
+import NoExpose.Cli
+import NoExpose.Paths
+
+/-!
+# `NoExpose.Report` — read and render the joined report
+
+A `report.jsonl` record (built by `collect`) carries everything `report`
+and `edit` need:
+
+```
+{"name": "Foo.bar", "kind": "def", "effect": "exposed",
+ "module": "Mathlib.Foo", "file": "Mathlib/Foo.lean",
+ "line": 42, "col": 0, "attr_line": 41,
+ "section_line": 25,                   -- present iff the `@[expose]`
+                                       --   is a section attribute
+ "downstream_usage": 17, "num_using_files": 5,
+ "top_using_files": [{"file": "...", "count": 4}, ...]}
+```
+
+Every record corresponds to a literal `@[expose]` occurrence in source,
+intersected with one env decl whose start falls inside its scope.
+There is no `unknown`/`meta`/`nonAttrExposed` taxonomy because, by
+construction, every record represents an actually-editable attribute.
+
+This module parses those records and renders per-file output in text or
+JSON. Building `report.jsonl` is the responsibility of
+`NoExpose.Diagnostics` and the `collect` orchestrator.
+-/
+
+open Lean (Json)
+
+namespace NoExpose
+
+/-- A single decl's report row. -/
+structure ReportRecord where
+  name : String
+  kind : String
+  effect : String
+  module : String
+  file : String
+  line : Nat
+  col : Nat
+  attrLine : Nat
+  sectionLine : Option Nat
+  downstreamUsage : Nat
+  numUsingFiles : Nat
+  topUsingFiles : Array (String × Nat)
+  deriving Inhabited
+
+/-- The ordered groups we render. -/
+inductive Verdict where
+  | safeToUnexpose
+  | neededDownstream
+  | noopAlwaysExported
+  deriving BEq
+
+def Verdict.classify (r : ReportRecord) : Verdict :=
+  if r.effect == "noop-always-exported" then .noopAlwaysExported
+  else if r.downstreamUsage == 0 then .safeToUnexpose
+  else .neededDownstream
+
+private def jsonGetStr (j : Json) (field : String) : Except String String :=
+  (j.getObjVal? field).bind (·.getStr?)
+
+private def jsonGetNat (j : Json) (field : String) : Except String Nat := do
+  let v ← j.getObjVal? field
+  match v with
+  | .num n =>
+    -- JSON numbers can be integer-valued; reject negatives.
+    if n.mantissa ≥ 0 then
+      pure (n.mantissa.toNat * 10 ^ n.exponent)
+    else
+      .error s!"non-integer or negative count in field {field}: {n}"
+  | _ => .error s!"expected number for field {field}, got {v.compress}"
+
+private def parseTopUsing (j : Json) : Except String (Array (String × Nat)) := do
+  let arr ← j.getArr?
+  arr.mapM fun entry => do
+    let file ← jsonGetStr entry "file"
+    let count ← jsonGetNat entry "count"
+    pure (file, count)
+
+/-- Parse a single line of `report.jsonl`. -/
+def parseRecord (line : String) : Except String ReportRecord := do
+  let j ← Json.parse line
+  let topJ := j.getObjVal? "top_using_files" |>.toOption |>.getD (.arr #[])
+  let sectionLine :=
+    (j.getObjVal? "section_line" |>.toOption.bind
+      (fun v => match v with | .num n => some n.mantissa.toNat | _ => none))
+  return {
+    name := ← jsonGetStr j "name"
+    kind := ← jsonGetStr j "kind"
+    effect := ← jsonGetStr j "effect"
+    module := ← jsonGetStr j "module"
+    file := ← jsonGetStr j "file"
+    line := ← jsonGetNat j "line"
+    col := ← jsonGetNat j "col"
+    attrLine := ← jsonGetNat j "attr_line"
+    sectionLine
+    downstreamUsage := ← jsonGetNat j "downstream_usage"
+    numUsingFiles := ← jsonGetNat j "num_using_files"
+    topUsingFiles := ← parseTopUsing topJ
+  }
+
+/-- Read all records from `report.jsonl`, accumulating any parse errors
+into a separate channel rather than aborting on the first one. -/
+def readReport (path : System.FilePath) :
+    IO (Array ReportRecord × Array String) := do
+  let mut ok : Array ReportRecord := #[]
+  let mut errs : Array String := #[]
+  let lines := (← IO.FS.readFile path).splitOn "\n"
+  for (line, i) in lines.zip (List.range lines.length) do
+    if line.trimAscii.isEmpty then continue
+    match parseRecord line with
+    | .ok r => ok := ok.push r
+    | .error msg => errs := errs.push s!"line {i+1}: {msg}"
+  return (ok, errs)
+
+/-- Group records by their `file`. -/
+def byFile (rs : Array ReportRecord) : Std.HashMap String (Array ReportRecord) :=
+  rs.foldl (init := {}) fun acc r =>
+    let existing := acc.getD r.file #[]
+    acc.insert r.file (existing.push r)
+
+/-- Pad a string to at least `n` characters with trailing spaces. -/
+private def padTo (n : Nat) (s : String) : String :=
+  if s.length ≥ n then s
+  else s ++ "".pushn ' ' (n - s.length)
+
+/-- Sort records within a file: by line first, then by name. -/
+private def sortByPosition (rs : Array ReportRecord) : Array ReportRecord :=
+  rs.qsort fun a b => if a.line ≠ b.line then a.line < b.line else a.name < b.name
+
+/-- Render one file's records in text format. -/
+def renderTextFile (file : String) (rs : Array ReportRecord) : String := Id.run do
+  let total := rs.size
+  let safe := rs.filter (Verdict.classify · == .safeToUnexpose)
+  let needed := rs.filter (Verdict.classify · == .neededDownstream)
+  let noop := rs.filter (Verdict.classify · == .noopAlwaysExported)
+  let mut out := s!"{file}: {safe.size} safe-to-unexpose, " ++
+    s!"{needed.size} needed-downstream, {noop.size} noop ({total} total)\n"
+  if !safe.isEmpty then
+    out := out ++ "\n  safe-to-unexpose:\n"
+    for r in sortByPosition safe do
+      out := out ++ s!"    {padTo 60 r.name}  (line {r.line})\n"
+  if !needed.isEmpty then
+    out := out ++ "\n  needed downstream (must keep @[expose]):\n"
+    for r in sortByPosition needed do
+      out := out ++ s!"    {padTo 60 r.name}  " ++
+        s!"(line {r.line}; {r.downstreamUsage} uses across " ++
+        s!"{r.numUsingFiles} files)\n"
+  return out
+
+/-- Render one file's records in JSON (one object per file, decls grouped). -/
+def renderJsonFile (file : String) (rs : Array ReportRecord) : Json := Id.run do
+  let mkDecl (r : ReportRecord) : Json := Json.mkObj [
+    ("name", r.name),
+    ("line", r.line),
+    ("downstream_usage", r.downstreamUsage),
+    ("num_using_files", r.numUsingFiles)]
+  let bucket (vs : Array ReportRecord) : Json :=
+    .arr (sortByPosition vs |>.map mkDecl)
+  let safe := rs.filter (Verdict.classify · == .safeToUnexpose)
+  let needed := rs.filter (Verdict.classify · == .neededDownstream)
+  let noop := rs.filter (Verdict.classify · == .noopAlwaysExported)
+  return Json.mkObj [
+    ("file", file),
+    ("safe_to_unexpose", bucket safe),
+    ("needed_downstream", bucket needed),
+    ("noop", bucket noop)]
+
+/-- Top-level `report` subcommand. -/
+def runReport (args : ReportArgs) : IO UInt32 := do
+  unless ← System.FilePath.pathExists reportPath do
+    IO.eprintln s!"no_expose: {reportPath} not found. \
+      Run `lake exe no_expose collect` first."
+    return 2
+  let (records, errs) ← readReport reportPath
+  for e in errs do IO.eprintln s!"warning: {e}"
+  let groups := byFile records
+  -- Default to every file in the report; with explicit PATHs, just those.
+  let selectedFiles : Array String :=
+    if args.paths.isEmpty then groups.toArray.map (·.1) |>.qsort (· < ·)
+    else args.paths
+  match args.format with
+  | .text => do
+    for f in selectedFiles do
+      let rs := groups.getD f #[]
+      if rs.isEmpty then
+        IO.println s!"{f}: no exposed decls in report"
+      else
+        IO.print (renderTextFile f rs)
+  | .json => do
+    let objs := selectedFiles.map fun f =>
+      renderJsonFile f (groups.getD f #[])
+    IO.println (Json.arr objs).pretty
+  return 0
+
+/-! ## Build side: join raw signals into `report.jsonl` -/
+
+/-- Decl key + originating file. `Std.HashMap` lacks structural keys
+of arbitrary nested type, so we use a `String × String` here. -/
+private abbrev UseKey := String × String
+
+/-- Parse one line of `diagnostics.jsonl` or `static_refs.jsonl`. Returns
+`(decl, file, count, theoremCount)`. `theoremCount = 0` when the field
+is absent (diagnostics records). -/
+private def parseSignalLine (line : String) :
+    Except String (String × String × Nat × Nat) := do
+  let j ← Json.parse line
+  let decl ← jsonGetStr j "decl"
+  let file ← jsonGetStr j "file"
+  let count ← jsonGetNat j "count"
+  let thm := j.getObjVal? "theorem_count" |>.toOption
+    |>.bind (·.getNat?.toOption) |>.getD 0
+  return (decl, file, count, thm)
+
+/-- Parse one line of `decl_refs.jsonl`: `{decl: ..., refs: [...]}`. -/
+private def parseDeclRefsLine (line : String) :
+    Except String (String × Array String) := do
+  let j ← Json.parse line
+  let decl ← jsonGetStr j "decl"
+  let refsJ ← j.getObjVal? "refs"
+  let refsArr ← refsJ.getArr?
+  let refs ← refsArr.mapM (·.getStr?)
+  return (decl, refs)
+
+/-- Read `exposed.jsonl` into a map keyed by decl name. -/
+private def readExposed (path : System.FilePath) : IO (Std.HashMap String Json) := do
+  let mut acc : Std.HashMap String Json := {}
+  for line in (← IO.FS.readFile path).splitOn "\n" do
+    if line.trimAscii.isEmpty then continue
+    match Json.parse line with
+    | .ok j =>
+      match jsonGetStr j "name" with
+      | .ok name => acc := acc.insert name j
+      | .error _ => pure ()
+    | .error _ => pure ()
+  return acc
+
+/-- Same-module-but-from-theorem references count; other same-module
+refs are skipped. -/
+private def shouldCount (sameModule : Bool) (count theoremCount : Nat) : Option Nat :=
+  if sameModule then
+    if theoremCount > 0 then some theoremCount else none
+  else
+    some count
+
+/-- Absorb one signal file into the running usage map. Returns the
+number of records actually counted (skipping any that don't match an
+exposed decl or are filtered out). -/
+private def absorbSignal (exposed : Std.HashMap String Json)
+    (path : System.FilePath)
+    (usage : Std.HashMap String Nat)
+    (usingMap : Std.HashMap UseKey Nat) :
+    IO (Std.HashMap String Nat × Std.HashMap UseKey Nat × Nat) := do
+  let mut usage := usage
+  let mut usingMap := usingMap
+  let mut absorbed := 0
+  for line in (← IO.FS.readFile path).splitOn "\n" do
+    if line.trimAscii.isEmpty then continue
+    match parseSignalLine line with
+    | .error _ => continue
+    | .ok (decl, file, count, thm) =>
+      let some rec := exposed[decl]? | continue
+      let recFile := (rec.getObjVal? "file" |>.bind (·.getStr?)).toOption.getD ""
+      let some delta := shouldCount (file == recFile) count thm | continue
+      usage := usage.insert decl ((usage.getD decl 0) + delta)
+      let key : UseKey := (decl, file)
+      usingMap := usingMap.insert key ((usingMap.getD key 0) + delta)
+      absorbed := absorbed + 1
+  return (usage, usingMap, absorbed)
+
+/-- One-hop transitive closure: a downstream use of decl `K` propagates
+to every decl in `K`'s body. -/
+private def applyTransitiveClosure (exposed : Std.HashMap String Json)
+    (declRefsPath : System.FilePath)
+    (usage : Std.HashMap String Nat)
+    (usingMap : Std.HashMap UseKey Nat) :
+    IO (Std.HashMap String Nat × Std.HashMap UseKey Nat × Nat) := do
+  -- Load decl_refs into a map.
+  let mut refsMap : Std.HashMap String (Array String) := {}
+  for line in (← IO.FS.readFile declRefsPath).splitOn "\n" do
+    if line.trimAscii.isEmpty then continue
+    if let .ok (decl, refs) := parseDeclRefsLine line then
+      refsMap := refsMap.insert decl refs
+  -- Snapshot usingMap to avoid iterating while mutating.
+  let snapshot := usingMap.toArray
+  let mut usage := usage
+  let mut usingMap := usingMap
+  let mut propagated := 0
+  for ((decl, file), count) in snapshot do
+    let some refs := refsMap[decl]? | continue
+    for ref in refs do
+      let some refRec := exposed[ref]? | continue
+      let recFile := (refRec.getObjVal? "file" |>.bind (·.getStr?)).toOption.getD ""
+      if file == recFile then continue  -- same-module
+      usage := usage.insert ref ((usage.getD ref 0) + count)
+      let key : UseKey := (ref, file)
+      usingMap := usingMap.insert key ((usingMap.getD key 0) + count)
+      propagated := propagated + 1
+  return (usage, usingMap, propagated)
+
+/-- Build `report.jsonl` by joining the four input files. -/
+def build (exposedPath diagnosticsPath staticRefsPath declRefsPath : System.FilePath)
+    (outPath : System.FilePath) : IO Unit := do
+  let exposed ← readExposed exposedPath
+  IO.eprintln s!"[no_expose report] loaded {exposed.size} exposed decls"
+
+  let mut usage : Std.HashMap String Nat := {}
+  let mut usingMap : Std.HashMap UseKey Nat := {}
+  if ← System.FilePath.pathExists diagnosticsPath then
+    let (u, uf, n) ← absorbSignal exposed diagnosticsPath usage usingMap
+    usage := u; usingMap := uf
+    IO.eprintln s!"[no_expose report] absorbed {n} diagnostics records"
+  if ← System.FilePath.pathExists staticRefsPath then
+    let (u, uf, n) ← absorbSignal exposed staticRefsPath usage usingMap
+    usage := u; usingMap := uf
+    IO.eprintln s!"[no_expose report] absorbed {n} static-reference records"
+  if ← System.FilePath.pathExists declRefsPath then
+    let (u, uf, n) ← applyTransitiveClosure exposed declRefsPath usage usingMap
+    usage := u; usingMap := uf
+    IO.eprintln s!"[no_expose report] one-hop transitive: propagated {n} extra (ref,file) edges"
+
+  -- Build per-decl `top_usingMap_files` from `usingMap`.
+  let mut perDecl : Std.HashMap String (Array (String × Nat)) := {}
+  for ((decl, file), count) in usingMap.toArray do
+    let cur := perDecl.getD decl #[]
+    perDecl := perDecl.insert decl (cur.push (file, count))
+
+  IO.FS.writeFile outPath ""
+  IO.FS.withFile outPath .append fun h => do
+    for (name, exposedRec) in exposed.toArray do
+      let u := usage.getD name 0
+      let top := perDecl.getD name #[]
+      let topSorted := top.qsort fun a b => a.2 > b.2
+      let topNFiles := top.size
+      let top5 := topSorted.take 5
+      let topJson := "[" ++ String.intercalate "," (top5.toList.map fun (f, c) =>
+        "{\"file\":\"" ++ jsonEscape f ++ "\",\"count\":" ++ toString c ++ "}") ++ "]"
+      -- Re-emit the original exposed record's fields plus our additions.
+      let baseStr := exposedRec.compress
+      -- Drop the trailing `}` and append our fields.
+      let baseStripped := baseStr.dropEnd 1
+      h.putStrLn (baseStripped.toString ++
+        ",\"downstream_usage\":" ++ toString u ++
+        ",\"num_using_files\":" ++ toString topNFiles ++
+        ",\"top_using_files\":" ++ topJson ++ "}")
+  IO.eprintln s!"[no_expose report] wrote {exposed.size} report rows to {outPath}"
+
+end NoExpose
diff --git a/scripts/NoExpose/Restore.lean b/scripts/NoExpose/Restore.lean
new file mode 100644
index 00000000000000..dfdd3b4697fa6a
--- /dev/null
+++ b/scripts/NoExpose/Restore.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lean.Data.Json
+import NoExpose.Paths
+
+/-!
+# `NoExpose.Restore` — backup, restore, orphan detection
+
+Tiny safety wrapper around "modify a file, run something, put it
+back." Used by `NoExpose.Diagnostics` (lakefile patch + per-file
+patches) and by `NoExpose.Edit` to keep an audit trail.
+
+* `backup path`: copy `path` into `restoreDir` under a sanitised name,
+  recording the mapping in `state.json`.
+* `restoreAll`: read `state.json`, copy every backup back to its
+  original location, then `rm -rf` `restoreDir`.
+* `detectOrphan`: at startup, if `state.json` exists, prompt/restore
+  before continuing — this means a previous `collect` was killed
+  mid-run and the source tree is still patched.
+* `withBackups [paths] body`: bracket pattern. Backs up every path,
+  runs `body`, restores in `finally` even on exception.
+-/
+
+open System Lean
+
+namespace NoExpose
+
+/-- Sanitise a path into a flat backup file name.
+`Mathlib/Foo/Bar.lean` → `Mathlib_Foo_Bar.lean`. -/
+private def sanitise (p : FilePath) : String :=
+  p.toString.replace "/" "_" |>.replace "\\" "_"
+
+/-- One entry in `state.json`: original path + backup path. -/
+structure RestoreEntry where
+  original : String
+  backup   : String
+  deriving Inhabited
+
+private def entryToJson (e : RestoreEntry) : Json :=
+  Json.mkObj [("original", e.original), ("backup", e.backup)]
+
+private def parseStateFile (s : String) : Array RestoreEntry :=
+  match Json.parse s with
+  | .error _ => #[]
+  | .ok j => Id.run do
+    let arr := j.getObjVal? "entries" |>.toOption |>.bind (·.getArr?.toOption)
+              |>.getD #[]
+    let mut out : Array RestoreEntry := #[]
+    for entry in arr do
+      let some original := entry.getObjValAs? String "original" |>.toOption | continue
+      let some backup := entry.getObjValAs? String "backup" |>.toOption | continue
+      out := out.push { original, backup }
+    return out
+
+private def writeStateFile (entries : Array RestoreEntry) : IO Unit := do
+  IO.FS.createDirAll restoreDir
+  let body := Json.mkObj [("entries", Json.arr (entries.map entryToJson))]
+  IO.FS.writeFile restoreStatePath body.compress
+
+private def readStateFile : IO (Array RestoreEntry) := do
+  if ← System.FilePath.pathExists restoreStatePath then
+    let s ← IO.FS.readFile restoreStatePath
+    return parseStateFile s
+  return #[]
+
+/-- Copy `path` into `restoreDir` and append it to the state file. Idempotent:
+calling twice with the same path is a no-op. -/
+def backup (path : FilePath) : IO Unit := do
+  IO.FS.createDirAll restoreDir
+  let entries ← readStateFile
+  let pathStr := path.toString
+  if entries.any (·.original == pathStr) then return
+  unless ← System.FilePath.pathExists path do
+    throw <| IO.userError s!"NoExpose.backup: {pathStr} does not exist"
+  let bkName := sanitise path
+  let bkPath := restoreDir / bkName
+  IO.FS.writeFile bkPath (← IO.FS.readFile path)
+  writeStateFile (entries.push { original := pathStr, backup := bkPath.toString })
+
+/-- Restore all backups recorded in `state.json`, then remove `restoreDir`. -/
+def restoreAll : IO Unit := do
+  let entries ← readStateFile
+  for e in entries do
+    if ← System.FilePath.pathExists e.backup then
+      let content ← IO.FS.readFile e.backup
+      IO.FS.writeFile e.original content
+  if ← System.FilePath.pathExists restoreDir then
+    IO.FS.removeDirAll restoreDir
+
+/-- Called at every startup. If `state.json` exists, a previous `collect`
+was interrupted; restore everything before continuing. -/
+def detectOrphan : IO Unit := do
+  unless ← System.FilePath.pathExists restoreStatePath do return
+  let entries ← readStateFile
+  if entries.isEmpty then
+    if ← System.FilePath.pathExists restoreDir then
+      IO.FS.removeDirAll restoreDir
+    return
+  IO.eprintln s!"[no_expose] detected {entries.size} orphan backup(s) from a previous run; restoring."
+  restoreAll
+
+/-- Bracket pattern: back up every path, run `body`, restore even on
+exception. Returns `body`'s result. -/
+def withBackups {α : Type} (paths : Array FilePath) (body : IO α) : IO α := do
+  for p in paths do backup p
+  try
+    let r ← body
+    restoreAll
+    return r
+  catch e =>
+    restoreAll
+    throw e
+
+end NoExpose
diff --git a/scripts/NoExpose/SourceScan.lean b/scripts/NoExpose/SourceScan.lean
new file mode 100644
index 00000000000000..7e49b279bc7452
--- /dev/null
+++ b/scripts/NoExpose/SourceScan.lean
@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+/-!
+# `NoExpose.SourceScan` — locate `@[expose]` occurrences in source
+
+The tool can only edit `@[expose]` attributes that actually exist in
+source text, so we drive candidate selection from those occurrences
+rather than from an env-walk of every body-exposed `def` (which over-
+collects by ~50x once macro-generated and `meta`-section decls are
+counted).
+
+For each `@[expose]` text occurrence in a `.lean` file we emit one
+`ExposeOccurrence` carrying:
+
+* `attrLine`/`attrCol` — position of the literal `@[expose]` text.
+* `scope` — either `.decl` (attaches to the next declaration) or
+  `.section_ closeLine` (attaches to every declaration whose own
+  start line falls in `[attrLine, closeLine]`).
+
+The companion mapping from source ranges to env constants happens in
+`NoExpose.Env`, using `Lean.findDeclarationRanges?` as the authority
+for names and ranges.
+-/
+
+namespace NoExpose
+
+/-- How a `@[expose]` attribute attaches to source. -/
+inductive ExposeScope where
+  /-- `@[expose]` (possibly bundled with other attributes) immediately
+  preceding a declaration. -/
+  | decl
+  /-- `@[expose] (public)? (meta)? section ...` covering everything
+  through the matching `end` on line `closeLine`. -/
+  | section_ (closeLine : Nat)
+  deriving Repr, Inhabited
+
+structure ExposeOccurrence where
+  /-- 1-based line of the literal `@[expose]` text. -/
+  attrLine : Nat
+  /-- 1-based column of the `@` of `@[expose]`. -/
+  attrCol : Nat
+  scope : ExposeScope
+  deriving Repr, Inhabited
+
+namespace SourceScan
+
+/-- Does `body` (content between `@[` and `]`) contain `expose` as a
+comma-separated token? Avoids matching `no_expose`, `exposes`, etc. -/
+private def bodyHasExposeToken (body : String) : Bool := Id.run do
+  for tok in body.splitOn "," do
+    if tok.trimAscii.toString == "expose" then return true
+  return false
+
+/-- If `s` starts with `@[`, return `(col, body, restOfLine)` where
+`col` is the 0-based offset of the `@`, `body` is the content between
+`@[` and the matching `]`, and `restOfLine` is what comes after `]`.
+Returns `none` if no `@[` opens at `s.firstNonWhitespace`. Tab/space
+prefixes are tolerated. -/
+private partial def consumeOneAttr (s : String) : Option (Nat × String × String) := Id.run do
+  let bytes := s.toUTF8
+  let n := bytes.size
+  let mut i : Nat := 0
+  -- skip leading whitespace
+  while i < n && (bytes[i]! == 0x20 || bytes[i]! == 0x09) do i := i + 1
+  if i + 1 >= n then return none
+  if bytes[i]! != 0x40 || bytes[i + 1]! != 0x5B then return none  -- not `@[`
+  let attCol := i
+  let bodyStart := i + 2
+  let mut p := bodyStart
+  while p < n && bytes[p]! != 0x5D do p := p + 1                   -- ']'
+  if p == n then return none
+  let body := String.fromUTF8! (bytes.extract bodyStart p)
+  let rest := String.fromUTF8! (bytes.extract (p + 1) n)
+  return some (attCol, body, rest)
+
+/-- Strip every leading `@[...]` block, returning `(rest, sawExpose)`.
+`sawExpose` is true if any of the stripped blocks contained the
+`expose` token. -/
+private partial def consumeAttrs (s : String) : String × Bool := Id.run do
+  let mut s := s
+  let mut sawExpose := false
+  while true do
+    match consumeOneAttr s with
+    | none => break
+    | some (_, body, rest) =>
+      if bodyHasExposeToken body then sawExpose := true
+      s := rest
+  return (s.trimAscii.toString, sawExpose)
+
+private def sectionModifiers : Array String :=
+  #["public ", "private ", "protected ", "meta ", "noncomputable ",
+    "partial ", "unsafe ", "scoped "]
+
+/-- Strip leading section/decl modifier words. -/
+private partial def stripMods (s : String) : String := Id.run do
+  let mut s := s
+  let mut changed := true
+  while changed do
+    changed := false
+    for m in sectionModifiers do
+      if s.startsWith m then
+        s := (s.drop m.length).toString
+        changed := true
+        break
+  return s
+
+/-- Does the line (after attribute and modifier prefixes) open a
+section or namespace? Both contribute frames to the open-scope stack
+so that `end` matches the right opener. -/
+private def opensScope (afterMods : String) : Bool :=
+  afterMods == "section" || afterMods.startsWith "section " ||
+  afterMods.startsWith "namespace "
+
+/-- Does the trimmed line start an `end ...` command? -/
+private def isEndLine (trimmed : String) : Bool :=
+  trimmed == "end" || trimmed.startsWith "end "
+
+end SourceScan
+
+open SourceScan in
+/-- Walk `text` line by line, tracking nested sections/namespaces and
+emitting one `ExposeOccurrence` per `@[expose]` occurrence we find.
+For section-style occurrences we record the line of the matching
+`end`; for decl-style ones the next declaration command line is the
+attachment point (resolved by the caller against env declaration
+ranges, not parsed from text).
+
+This scanner is deliberately text-level and small: it only needs to
+find `@[expose]` text, recognise `section`/`namespace`/`end` openers,
+and balance them. Mathlib's notation extensions don't affect any of
+those tokens, so we don't need the full Lean parser. -/
+partial def scanExposeOccurrences (text : String) : Array ExposeOccurrence := Id.run do
+  let lines := (text.splitOn "\n").toArray
+  -- Stack of open scopes, each with `Some attrLineCol` iff opened by
+  -- `@[expose] section`. Namespaces and non-expose sections push
+  -- `none` and contribute only to balance.
+  let mut stack : List (Option (Nat × Nat)) := []
+  let mut out : Array ExposeOccurrence := #[]
+  let mut inBlockComment : Bool := false
+  for h : i in [:lines.size] do
+    let line := lines[i]
+    let trimmed := line.trimAscii.toString
+    let lineNum := i + 1
+    -- Handle multi-line block / module-doc comments.
+    if inBlockComment then
+      if trimmed.endsWith "-/" then inBlockComment := false
+      continue
+    if trimmed.isEmpty || trimmed.startsWith "--" then continue
+    if trimmed.startsWith "/-" && !trimmed.startsWith "/--" then
+      if !trimmed.endsWith "-/" then inBlockComment := true
+      continue
+    if trimmed.startsWith "/--" then
+      let isOneLine := trimmed.length > "/----/".length && trimmed.endsWith "-/"
+      if !isOneLine then inBlockComment := true
+      continue
+    -- `end` balances the stack regardless of expose-ness.
+    if isEndLine trimmed then
+      match stack with
+      | some (openLine, openCol) :: rest =>
+        out := out.push
+          { attrLine := openLine, attrCol := openCol,
+            scope := .section_ lineNum }
+        stack := rest
+      | none :: rest => stack := rest
+      | []           => ()
+      continue
+    -- Consume any leading `@[...]` attribute blocks, recording whether
+    -- one of them carried `expose`.
+    let (afterAttrs, hasExpose) := consumeAttrs trimmed
+    let afterMods := stripMods afterAttrs
+    -- This line opens a section/namespace.
+    if opensScope afterMods then
+      if hasExpose && afterMods.startsWith "section" then
+        -- attrCol is approximated by the leading-whitespace count.
+        let col := (line.takeWhile Char.isWhitespace).length
+        stack := some (lineNum, col + 1) :: stack
+      else
+        stack := none :: stack
+      continue
+    -- Decl-level `@[expose]` on this line, attaching to the next decl
+    -- the env walk will identify.
+    if hasExpose then
+      let col := (line.takeWhile Char.isWhitespace).length
+      out := out.push
+        { attrLine := lineNum, attrCol := col + 1, scope := .decl }
+      continue
+    -- An `@[expose]` could be on its own line followed by a decl
+    -- whose modifiers/keyword sit on later lines. The decl-level
+    -- branch above already covers `@[expose]` alone (afterMods becomes
+    -- empty, `opensScope` false). We don't need a separate pending
+    -- state because the caller resolves decl attachment by source
+    -- range, not by syntactic adjacency.
+  -- Sections that run to EOF without an explicit `end` still cover
+  -- everything between their opener and the last line of the file.
+  -- Flush any remaining `@[expose]` frames.
+  for frame in stack do
+    match frame with
+    | some (openLine, openCol) =>
+      out := out.push
+        { attrLine := openLine, attrCol := openCol,
+          scope := .section_ lines.size }
+    | none => ()
+  return out
+
+end NoExpose
diff --git a/scripts/README.md b/scripts/README.md
index d2d5a2dc822347..7d2cee77796e76 100644
--- a/scripts/README.md
+++ b/scripts/README.md
@@ -186,6 +186,21 @@ to module `Foo.Bar` (no `srcDir` indirection).
   lists (which occasionally leave lines over the 100-char limit).
   Usage: `scripts/fix_long_lines.py path:line ...`
 
+- `lake exe no_expose [collect|report|edit|clean]`
+  Tool for finding `@[expose]`-annotated defs that aren't needed
+  downstream and removing the attribute. `collect` walks the built
+  Mathlib environment (and, without `--skip-build`, runs a full
+  `lake build` with `diagnostics=true`) and writes
+  `scripts/.no_expose/{exposed,static_refs,decl_refs,diagnostics,report}.jsonl`.
+  `report PATH...` renders per-file safe-to-unexpose / needed
+  classifications (text or json). `edit PATH...` applies the
+  removal (default; `--dry-run` previews) using a section-level or
+  per-decl strategy auto-detected from the file. With `--verify`,
+  re-runs `lake build` on the touched module and rolls back on
+  failure.
+  The exe deliberately does not `import Mathlib` (so it builds in
+  seconds); it loads the env at runtime via `Lean.withImportModules`.
+
 **CI workflow**
 - `lake-build-with-retry.sh`
   Runs `lake build` on a target until `lake build --no-build` succeeds. Used in the main build workflows.
diff --git a/scripts/no_expose.lean b/scripts/no_expose.lean
new file mode 100644
index 00000000000000..8b265e5db9bb79
--- /dev/null
+++ b/scripts/no_expose.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import NoExpose.Cli
+import NoExpose.Collect
+import NoExpose.Edit
+import NoExpose.Paths
+import NoExpose.Report
+
+/-!
+# `lake exe no_expose` — entry point
+
+Tiny dispatcher. All work lives in `NoExpose.*` modules.
+-/
+
+open NoExpose
+
+unsafe def main (args : List String) : IO UInt32 := do
+  match parseArgs args with
+  | .error msg => do
+    IO.eprintln s!"no_expose: {msg}"
+    IO.eprintln ""
+    IO.eprintln helpText
+    return 2
+  | .ok .help => do
+    IO.println helpText
+    return 0
+  | .ok .clean => do
+    if ← System.FilePath.pathExists dataDir then
+      IO.FS.removeDirAll dataDir
+      IO.println s!"removed {dataDir}"
+    else
+      IO.println s!"{dataDir} does not exist; nothing to clean"
+    return 0
+  | .ok (.collect a) => runCollect a
+  | .ok (.report a) => runReport a
+  | .ok (.edit a) => runEdit a