diff --git a/LeanMetrics/Authored.lean b/LeanMetrics/Authored.lean
index 1c105f8..0b965b8 100644
--- a/LeanMetrics/Authored.lean
+++ b/LeanMetrics/Authored.lean
@@ -7,7 +7,6 @@ module
 
 public import Lean.Environment
 import Lean.AuxRecursor
-import Lean.Class
 import Lean.DeclarationRange
 import Lean.Meta.Match.MatcherInfo
 import Lean.ProjFns
@@ -38,26 +37,10 @@ For example a constructor, a `where` helper, a `deriving` instance, or a parser
 def hasOwnDeclaration (env : Environment) (n : Name) : Bool :=
   (declRangeExt.find? env n).isSome && !sameOrigin env n n.getPrefix
 
-/-- Whether structure `s` has `target` among its ancestors. -/
-partial def hasAncestor (env : Environment) (s target : Name) (visited : NameSet := {}) : Bool :=
-  if visited.contains s then false
-  else (getStructureInfo? env s).any fun info =>
-    info.parentInfo.any fun p =>
-      p.structName == target || hasAncestor env p.structName target (visited.insert s)
-
-/-- Whether `n` converts a structure to one it builds on: the coercion `extends` generates, or a
-`toX` in the structure's namespace when the structure is a class or `X` is an ancestor
-(`Field.toSemifield`). -/
+/-- Whether `n` is a parent projection registered by `extends`. Names alone are not evidence:
+an author can write an ordinary function such as `Box.toNat` in a class namespace. -/
 def isParentProjection (env : Environment) (n : Name) : Bool :=
-  match getStructureInfo? env n.getPrefix, n with
-  | none, _ => false
-  | some info, .str p s =>
-    info.parentInfo.any (·.projFn == n) ||
-      (s.startsWith "to" && s.length > 2 &&
-        let target := (s.drop 2).toString
-        (target.startsWith "OfNat" && target.any Char.isDigit) || isClass env p ||
-          (getStructureInfo? env (.mkSimple target)).isSome && hasAncestor env p (.mkSimple target))
-  | some info, _ => info.parentInfo.any (·.projFn == n)
+  (getStructureInfo? env n.getPrefix).any fun info => info.parentInfo.any (·.projFn == n)
 
 /-- Namespaces of tactic implementations. -/
 def tacticNamespaces : List Name :=
diff --git a/LeanMetrics/Driver.lean b/LeanMetrics/Driver.lean
index d381127..cc528cc 100644
--- a/LeanMetrics/Driver.lean
+++ b/LeanMetrics/Driver.lean
@@ -42,10 +42,10 @@ partial def Output.render (o : Output) (indent : String := "") : String :=
 
 /-- Version of the output format, raised whenever a column is renamed, removed or changes
 meaning. -/
-def schemaVersion : Nat := 1
+def schemaVersion : Nat := 2
 
 /-- The version of `lean-metrics`, reported in its output. -/
-def toolVersion : String := "0.1.0"
+def toolVersion : String := "0.2.0"
 
 /-- What to measure and how to report it. -/
 structure Options where
diff --git a/LeanMetrics/Metrics/Declarations.lean b/LeanMetrics/Metrics/Declarations.lean
index 0fb20c9..2f9fc72 100644
--- a/LeanMetrics/Metrics/Declarations.lean
+++ b/LeanMetrics/Metrics/Declarations.lean
@@ -8,6 +8,7 @@ module
 public import LeanMetrics.Basic
 import LeanMetrics.Stats
 import LeanMetrics.Syntax
+import Lean.Elab.PreDefinition.WF.Eqns
 
 /-! # Declarations
 
@@ -75,7 +76,7 @@ def declarations : Metric where
         counts := counts.insert k (counts.getD k 0 + 1)
         if k != "example" && (signatureBinders d).any isImplicitBinder then
           nImplicit := nImplicit + 1
-    -- `deriving` clauses and `attribute [instance]` commands also declare instances
+    -- `deriving` creates instances; `attribute [instance]` only registers existing constants.
     let mut nDerived := 0
     let mut nAttrInstance := 0
     for f in ctx.files do
@@ -90,7 +91,7 @@ def declarations : Metric where
         for a in nodesOfKind ``Command.attribute c do
           if (attributesUnder a).contains `instance then
             nAttrInstance := nAttrInstance + 1
-    counts := counts.insert "instance" (counts.getD "instance" 0 + nDerived + nAttrInstance)
+    counts := counts.insert "instance" (counts.getD "instance" 0 + nDerived)
     let n (k : String) := counts.getD k 0
     let nDefLike := defLike.foldl (· + n ·) 0
     return { columns :=
@@ -99,7 +100,8 @@ def declarations : Metric where
       #[("n_def_like", toJson nDefLike),
         ("def_like_to_theorem_ratio", ratio nDefLike (n "theorem")),
         ("n_decls_implicit_args", toJson nImplicit), ("n_new_classes", toJson (n "class")),
-        ("n_new_instances", toJson (n "instance"))] }
+        ("n_new_instances", toJson (n "instance")),
+        ("n_instance_attribute_commands", toJson nAttrInstance)] }
 
 /-- Metric `implicit_args`: Binder groups in declaration signatures, by kind. -/
 def implicitArgs : Metric where
@@ -125,7 +127,7 @@ def proofMode : Metric where
   needsSource := true
   run ctx := do
     let bodies := ctx.declarations.filter isTheorem |>.filterMap bodyOf?
-    let nTactic := (bodies.filter isTacticBody).size
+    let nTactic := (bodies.filter (isTacticBody ∘ unwrapProof)).size
     let nTerm := bodies.size - nTactic
     return { columns := #[("n_pm_term", toJson nTerm), ("n_pm_tactic", toJson nTactic),
       ("pm_term_ratio", ratio nTerm bodies.size)] }
@@ -153,18 +155,20 @@ def reducibility : Metric where
       ("red_irreducible_per_def", ratio nIrreducible nDef 4),
       ("red_abbrev_per_def", ratio nAbbrev nDef 4)] }
 
-/-- Metric `recursion_style`: `termination_by` and `decreasing_by` clauses. -/
+/-- Metric `recursion_style`: Source termination annotations and authored definitions Lean
+compiled with well-founded recursion, including inferred measures and counting each once. -/
 def recursionStyle : Metric where
   name := "recursion_style"
-  description := "`termination_by` and `decreasing_by` clauses"
+  description := "termination annotations and definitions compiled with well-founded recursion"
   needsSource := true
   run ctx := do
     let cmds := ctx.files.foldl (· ++ ·.commands) #[]
     let sum (k : SyntaxNodeKind) := cmds.foldl (· + countKind k ·) 0
     let t := sum ``Termination.terminationBy
     let d := sum ``Termination.decreasingBy
+    let wf := (ctx.authored.filter fun n => (Elab.WF.eqnInfoExt.find? ctx.env n).isSome).size
     return { columns := #[("n_rec_termination_by", toJson t), ("n_rec_decreasing_by", toJson d),
-      ("n_rec_well_founded", toJson (t + d)),
-      ("rec_uses_well_founded", toJson (decide (t + d > 0)))] }
+      ("n_rec_well_founded", toJson wf),
+      ("rec_uses_well_founded", toJson (decide (wf > 0)))] }
 
 end LeanMetrics
diff --git a/LeanMetrics/Metrics/Graph.lean b/LeanMetrics/Metrics/Graph.lean
index 25e9a41..0b57bd0 100644
--- a/LeanMetrics/Metrics/Graph.lean
+++ b/LeanMetrics/Metrics/Graph.lean
@@ -8,6 +8,8 @@ module
 public import LeanMetrics.Basic
 public import LeanMetrics.Authored
 import LeanMetrics.Stats
+import LeanMetrics.Syntax
+import Lean.Elab.DeclarationRange
 import Lean.Meta.Instances
 import Lean.ProjFns
 import Lean.Util.Recognizers
@@ -185,13 +187,32 @@ private def log10Nat (x : Nat) : Float :=
   let shift := x.log2 - min x.log2 52
   (x >>> shift).toFloat.log10 + shift.toFloat * Float.log10 2
 
+/-- Local instance registrations disappear on import. Recover their declaration identities
+from source selection ranges, including anonymous and private instances. -/
+private def sourceInstances (ctx : Context) : NameSet := Id.run do
+  let mut positions : Std.HashSet (Name × Nat × Nat) := {}
+  for file in ctx.files do
+    for cmd in file.commands do
+      for decl in declarationsOf cmd do
+        if decl.isOfKind ``Parser.Command.instance then
+          if let some pos := (Elab.getDeclarationSelectionRef decl).getPos? then
+            let p := file.fileMap.toPosition pos
+            positions := positions.insert (file.module, p.line, p.column)
+  let mut names : NameSet := {}
+  for n in ctx.authored do
+    if let some mod := ctx.moduleOf? n then
+      if let some ranges := declRangeExt.find? ctx.env n then
+        let p := ranges.selectionRange.pos
+        if positions.contains (mod, p.line, p.column) then names := names.insert n
+  return names
+
 /-- Metric `dep_graph`: Shape of the declaration dependency graph: degrees, roots and leaves,
 longest chain, and sharing of sub-results. -/
 def depGraph : Metric where
   name := "dep_graph"
   description := "shape of the declaration dependency graph: degrees, roots and leaves, longest \
     chain, and sharing of sub-results"
-  needsSource := false
+  needsSource := true
   run ctx := do
     let g := depGraphOf ctx
     let idx : Std.HashMap Name Nat := g.internal.foldl (fun m n => m.insert n m.size) {}
@@ -246,8 +267,9 @@ def depGraph : Metric where
     let extAll : NameSet := ext.foldl (fun s e => e.foldl (·.insert ·) s) {}
     let rootCost := root?.map (cost[·]!) |>.getD 0
     -- instances first: Prop-valued ones are theorems, and every instance is also a definition
+    let declaredInstances := sourceInstances ctx
     let kinds := g.internal.map fun c =>
-      if isInstanceCore ctx.env c then "instance"
+      if declaredInstances.contains c || isInstanceCore ctx.env c then "instance"
       else match ctx.env.find? c with
         | some (.thmInfo _) => "theorem"
         | some (.defnInfo _) | some (.opaqueInfo _) | some (.inductInfo _) => "def"
@@ -266,6 +288,7 @@ def depGraph : Metric where
       ("ext_deps_per_decl_mean", mean (ext.map (·.size)) 2), ("n_ext_consts", toJson extAll.size),
       ("longest_pole", toJson (maximum depth)),
       ("root", toJson ((root?.map (displayName g.internal[·]!)).getD "")),
+      ("root_id", toJson ((root?.map (toString g.internal[·]!)).getD "")),
       ("cost_root_log10", if rootCost == 0 then .null else decimal (log10Nat rootCost)),
       ("reachable_from_root", toJson reachable),
       ("compression_log10", if rootCost == 0 || reachable == 0 then .null
@@ -280,7 +303,14 @@ def depGraph : Metric where
       ("n_theorems_single_use", count fun i => kind i == "theorem" && inDeg[i]! == 1),
       ("n_defs_unused", count fun i => kind i == "def" && inDeg[i]! == 0),
       ("n_defs_no_theorem_user", count fun i => kind i == "def" && !usedByTheorem.contains i)]
-    let edges := g.edges.map fun (d, u) => Json.arr #[displayName d, displayName u]
-    return { columns, details := Json.mkObj [("edges", Json.arr edges)] }
+    -- Private declarations can have the same user name in different modules. Preserve Lean's
+    -- unique names as IDs and keep their readable names separately, including isolated nodes.
+    let nodeNames := g.internal.foldl (·.insert ·) extAll
+    let nodes := nodeNames.foldl (init := #[]) fun acc name => acc.push <| Json.mkObj [
+      ("id", toJson name.toString), ("name", toJson (displayName name)),
+      ("module", toJson ((ctx.moduleOf? name).map toString |>.getD "")),
+      ("internal", toJson (idx.contains name))]
+    let edges := g.edges.map fun (d, u) => Json.arr #[toJson d.toString, toJson u.toString]
+    return { columns, details := Json.mkObj [("nodes", Json.arr nodes), ("edges", Json.arr edges)] }
 
 end LeanMetrics
diff --git a/LeanMetrics/Metrics/Imports.lean b/LeanMetrics/Metrics/Imports.lean
index be3ae92..3863cff 100644
--- a/LeanMetrics/Metrics/Imports.lean
+++ b/LeanMetrics/Metrics/Imports.lean
@@ -188,7 +188,9 @@ def importMinimizability : Metric where
     let nAdd := total (·.add)
     let byModule (f : Shake.Verdict → Array Import) := Json.mkObj <| verdicts.toList.filterMap
       fun (i, v) => let is := authored f i v
-        if is.isEmpty then none else some (vnames[i]!.toString, toJson (is.map toString))
+        let render (imp : Import) := if view.header.moduleData[i]!.isModule then toString imp
+          else s!"import {imp.module}"
+        if is.isEmpty then none else some (vnames[i]!.toString, toJson (is.map render))
     -- the same count, from constants alone
     let closure := transitiveImports env
     let required := requiredModules env own
diff --git a/LeanMetrics/Metrics/Tactics.lean b/LeanMetrics/Metrics/Tactics.lean
index cca032f..b1bdb16 100644
--- a/LeanMetrics/Metrics/Tactics.lean
+++ b/LeanMetrics/Metrics/Tactics.lean
@@ -123,7 +123,7 @@ def decideUsage : Metric where
       nodesOfKind ``Tactic.simpAll c ++ nodesOfKind ``Tactic.simpa c ++
       nodesOfKind ``Tactic.dsimp c) #[]
     let termRfl := ctx.declarations.filter fun d =>
-      (bodyOf? d).any fun b => b.isIdent && b.getId == `rfl
+      (bodyOf? d).any fun b => let b := unwrapProof b; b.isIdent && b.getId == `rfl
     let nNativeDecide := cmds.foldl (· + countKind ``Tactic.nativeDecide ·) 0
     return { columns := #[
       ("n_dec_decide", toJson (decides.size - nKernel - nNative)), ("n_dec_kernel", toJson nKernel),
diff --git a/LeanMetrics/Syntax.lean b/LeanMetrics/Syntax.lean
index 2aed20a..dda7408 100644
--- a/LeanMetrics/Syntax.lean
+++ b/LeanMetrics/Syntax.lean
@@ -120,7 +120,15 @@ def bodyOf? (decl : Syntax) : Option Syntax :=
     | some e => some e[0][0]
     | none => none
 
-/-- Whether a body is a tactic block (`:= by …`). -/
+/-- Remove wrappers that do not change a proof's tactic/term mode. Keep the original syntax
+for source size and `by` depth: treating a wrapper as a `by` node would count it twice. -/
+partial def unwrapProof (body : Syntax) : Syntax :=
+  if body.isOfKind ``Term.paren || body.isOfKind ``Term.typeAscription then unwrapProof body[1]
+  else if body.isOfKind ``Term.set_option then unwrapProof body[5]
+  else if body.isOfKind ``Term.open then unwrapProof body[3]
+  else body
+
+/-- Whether this syntax node itself is a tactic block. -/
 def isTacticBody (body : Syntax) : Bool :=
   body.isOfKind ``Term.byTactic || body.isOfKind ``Term.byTactic'
 
diff --git a/Main.lean b/Main.lean
index 36b6eb9..9260f1a 100644
--- a/Main.lean
+++ b/Main.lean
@@ -45,7 +45,7 @@ def runCmd (p : Parsed) : IO UInt32 := do
 
 /-- The command line of `lean-metrics`. -/
 def cmd : Cmd := `[Cli|
-  "lean-metrics" VIA runCmd; ["0.1.0"]
+  "lean-metrics" VIA runCmd; ["0.2.0"]
   "Measure a built Lake project: size, declarations, proofs, tactics, imports, dependency \
   structure, documentation and build warnings. Run `lake build` in the project first."
 
diff --git a/README.md b/README.md
index 5fd76ac..6ffdc5a 100644
--- a/README.md
+++ b/README.md
@@ -36,7 +36,9 @@ every module they import from the project itself. Dependencies such as Mathlib a
 measured.
 
 Alternatively, `lean-metrics.sh` does both steps: run from the root of a project, it builds the
-project, builds `lean-metrics` with the same toolchain, and runs it.
+project, builds `lean-metrics` with the same toolchain, and runs it. This checkout supports Lean
+`v4.34.0`; the wrapper changes the selected toolchain but does not port Lean API usage or dependency
+versions to other releases.
 ```sh
 ../lean-metrics/lean-metrics.sh > metrics.json
 ```
@@ -55,7 +57,7 @@ monorepo, for example `--module MyMonorepo.ProjectA`, and loads only what those
 `--metric M,N` runs only these metrics; `--list` lists all of them with a one-line description.
 
 `--details` adds structured detail to the document, such as the tactic histogram, the dependency
-graph's edges, and the imports `lake shake` would remove and add in each module.
+graph's nodes and edges, and the imports `lake shake` would remove and add in each module.
 
 `--main A,B` names the project's main results, as they are written in the source. The dependency
 graph (`dep_graph`) is measured from the largest of them; by default, from the largest declaration
diff --git a/SCHEMA.md b/SCHEMA.md
index 1b9dbdd..7e4519d 100644
--- a/SCHEMA.md
+++ b/SCHEMA.md
@@ -1,4 +1,4 @@
-# `lean-metrics` output format: version 1
+# `lean-metrics` output format: version 2
 
 `lean-metrics` writes one JSON object. It begins with version information for the format, the tool
 and Lean, and a description of the project, followed by the metrics:
@@ -34,6 +34,11 @@ and, within a metric, in the order its columns are listed below.
 `schema_version` is raised whenever a column is renamed, removed, or changes meaning. Adding a
 column or a metric does not raise it.
 
+Version 2 corrects instance declaration counts and well-founded recursion counts. It also fixes
+proof-wrapper classification, authored declarations with `to…` names, and local instance kinds.
+Graph detail edges now use unique declaration IDs; use each node's `name` for display. Consumers
+comparing results with version 1 should remeasure their baseline.
+
 ## What is measured
 
 The project is the root package of the Lake workspace. Its libraries are those `lake build` builds:
@@ -80,14 +85,16 @@ the order statistics at rank `1 + p(n-1)/100`. A ratio with a zero denominator i
 ### `declarations`
 - `n_theorem` (theorems and `lemma`s), `n_def`, `n_abbrev`, `n_instance`, `n_structure`, `n_class`
   (`class` and `class inductive`), `n_inductive`, `n_axiom`, `n_opaque`, `n_example`: counts by
-  kind. `n_instance` also counts instances declared by `deriving` clauses (one per class and type)
-  and `attribute [instance]` commands.
+  kind. `n_instance` also counts instances declared by `deriving` clauses (one per class and type).
+  Registering an existing declaration with `attribute [instance]` does not create a declaration.
 - `n_decls`: all of the above except `example`.
 - `n_def_like`: `def`, `abbrev`, `class`, `structure`, `inductive` and `instance` together.
 - `def_like_to_theorem_ratio`: `n_def_like` over `n_theorem`.
 - `n_decls_implicit_args`: declarations whose signature has an implicit (`{…}`) or strict-implicit
   (`⦃…⦄`) binder group. `variable` binders do not count.
 - `n_new_classes`, `n_new_instances`: same as `n_class` and `n_instance`.
+- `n_instance_attribute_commands`: commands applying `[instance]`, regardless of how many names
+  each command registers. These do not contribute to `n_decls` or `n_new_instances`.
 
 ### `implicit_args`
 - `n_ia_explicit`, `n_ia_implicit`, `n_ia_strict`, `n_ia_inst`: binder groups in declaration
@@ -96,7 +103,8 @@ the order statistics at rank `1 + p(n-1)/100`. A ratio with a zero denominator i
 
 ### `proof_mode`
 - `n_pm_tactic`, `n_pm_term`: theorems proved by a tactic block (`:= by …`), and all others, which
-  includes pattern-matching alternatives.
+  includes pattern-matching alternatives. Parentheses, type ascriptions, `set_option … in` and
+  `open … in` around a proof do not change its mode.
 - `pm_term_ratio`: share of theorems proved by a term.
 
 ### `reducibility`
@@ -106,7 +114,10 @@ the order statistics at rank `1 + p(n-1)/100`. A ratio with a zero denominator i
 
 ### `recursion_style`
 - `n_rec_termination_by`, `n_rec_decreasing_by`: clauses giving a termination measure or proof.
-- `n_rec_well_founded`: their sum; `rec_uses_well_founded`: whether it is positive.
+- `n_rec_well_founded`: authored definitions compiled with well-founded recursion, identified
+  by Lean's well-founded equation metadata. Inferred termination measures count; explicitly
+  structural recursion does not. Each definition counts once even if it has both annotations.
+- `rec_uses_well_founded`: whether `n_rec_well_founded` is positive.
 
 ### `tactics`
 A tactic call is a syntax node whose kind is in the environment's `tactic` category. That includes
@@ -132,7 +143,8 @@ theorem bodies.
 - `n_dec_native_decide`: `native_decide` calls; `dec_uses_native_decide`: whether there are any.
 - `n_dec_simp_arith`: `simp`, `simp_all`, `simpa` and `dsimp` calls whose configuration turns on
   `arith`.
-- `n_dec_rfl`: the `rfl` tactic, and declarations whose body is the term `rfl`.
+- `n_dec_rfl`: the `rfl` tactic, and declarations whose body is the term `rfl`, ignoring the same
+  wrappers as `proof_mode`.
 
 ### `sorry_axiom`
 - `n_sorry`, `n_admit`: `sorry` (tactic or term) and `admit`.
@@ -220,7 +232,8 @@ Unused imports as `lake shake` finds them. See `LeanMetrics.Shake`.
 - `n_impmin_tactic_imports`: imports of tactic modules (`Mathlib.Tactic.*`, `Lean.Elab.Tactic.*`).
 - `impmin_uses_import_mathlib`: whether any module imports from `Mathlib`.
 - `n_impmin_import_cone_size`: modules reachable from the project's imports.
-- Details: `remove_by_module`, `add_by_module`.
+- Details: `remove_by_module`, `add_by_module`. Directives are rendered for each file's module
+  mode: a file without a `module` header gets plain `import`, never `public import`.
 
 ### `dep_graph`
 Nodes are the authored declarations (see `LeanMetrics.Authored`). An edge runs from `d` to `u` when
@@ -242,6 +255,8 @@ Columns:
 - `longest_pole`: edges on the longest dependency chain. A cycle counts as one step.
 - `root`: the main result, the declaration with the largest cost (next column) among those given
   with `--main`, or among the declarations nothing depends on when none are given.
+- `root_id`: the same declaration's unique Lean name, retaining private-name mangling. Both
+  `root` and `root_id` are empty strings when there is no candidate.
 - `cost_root_log10`: `log10` of the main result's cost, the size of its dependency tree fully
   unrolled (`cost(v) = 1 + Σ cost(dependencies)`).
 - `reachable_from_root`: declarations the main result depends on, itself included.
@@ -251,12 +266,19 @@ Columns:
   come from compiled bodies, where structural and well-founded recursion no longer name the
   functions they call, so only `unsafe` definitions produce one. A self-reference is not an edge.
 - `n_internal_theorems`, `n_internal_defs`, `n_internal_instances`: nodes by kind. Instances are
-  classified first, then theorems, then definitions (`def`, `opaque`, inductive types). Other nodes,
+  classified first, including local instance declarations whose registrations are not exported,
+  then theorems, then definitions (`def`, `opaque`, inductive types). Other nodes,
   such as constructors and axioms, are in none of the three.
 - `n_theorems_unused`, `n_defs_unused`, `n_instances_unused`: nodes nothing depends on.
 - `n_theorems_single_use`: theorems exactly one declaration depends on.
 - `n_defs_no_theorem_user`: definitions no theorem mentions.
 
+Details contain `nodes` and `edges`. Each node has `id` (unique Lean name), `name` (readable name),
+`module`, and `internal` (whether it belongs to the measured project). Isolated internal nodes
+are included. Each edge is `[dependency_id, user_id]`; external leaves are included in detail
+but excluded from `n_graph_decls` and `n_edges`. Private declarations in different modules can
+share a readable name, so use IDs to reconstruct the graph.
+
 ### `docstrings`
 - `n_doc_decls`, `n_doc_documented`: authored declarations, and those with a docstring.
 - `doc_coverage`: their ratio.
diff --git a/Test.lean b/Test.lean
index cb6f29b..9d100d2 100644
--- a/Test.lean
+++ b/Test.lean
@@ -65,6 +65,46 @@ def check (exe : FilePath) (dir : FilePath) (c : Case) : IO (Array String) := do
   | .ok actual =>
     return if c.expect.isNull then #[] else (mismatches "" c.expect actual).map (label ++ ·)
 
+/-- The exported graph must preserve two private helpers with the same readable name and an
+isolated node, so consumers can reconstruct the graph without conflating identities. -/
+def checkGraphIds (exe : FilePath) : IO Unit := do
+  let out ← run exe.toString #["--root", (fixtures / "private-node-ids").toString,
+    "--metric", "dep_graph", "--details"]
+  unless out.exitCode == 0 do throw <| .userError out.stderr
+  let doc ← IO.ofExcept <| Json.parse out.stdout
+  let graph ← IO.ofExcept <| doc.getObjVal? "details" >>= (·.getObjVal? "dep_graph")
+  let nodes ← IO.ofExcept <| graph.getObjValAs? (Array Json) "nodes"
+  let ids ← nodes.mapM fun n => IO.ofExcept <| n.getObjValAs? String "id"
+  let names ← nodes.mapM fun n => IO.ofExcept <| n.getObjValAs? String "name"
+  unless ids.size == 5 && ids.toList.eraseDups.length == 5 && ids.contains "isolated" &&
+      (names.filter (· == "helper")).size == 2 do
+    throw <| .userError "graph nodes lost a private identity or isolated declaration"
+  let edges ← IO.ofExcept <| graph.getObjValAs? (Array (Array String)) "edges"
+  unless edges.all (fun e => e.size == 2 && e.all ids.contains) do
+    throw <| .userError "graph edge endpoint is missing from nodes"
+
+/-- Apply the exact emitted directives, then let Lean check them. Always restore the fixture. -/
+def checkImportReplacement (exe : FilePath) : IO Unit := do
+  let dir := fixtures / "legacy-imports"
+  let out ← run exe.toString #["--root", dir.toString, "--module", "Case",
+    "--metric", "import_minimizability", "--details"]
+  unless out.exitCode == 0 do throw <| .userError out.stderr
+  let doc ← IO.ofExcept <| Json.parse out.stdout
+  let detail ← IO.ofExcept <| doc.getObjVal? "details" >>= (·.getObjVal? "import_minimizability")
+  let removed ← IO.ofExcept <| detail.getObjVal? "remove_by_module" >>=
+    (·.getObjValAs? (Array String) "Case")
+  let added ← IO.ofExcept <| detail.getObjVal? "add_by_module" >>=
+    (·.getObjValAs? (Array String) "Case")
+  let file := dir / "Case.lean"
+  let original ← IO.FS.readFile file
+  let body := removed.foldl (fun s imp => s.replace (imp ++ "\n") "") original
+  try
+    IO.FS.writeFile file ("\n".intercalate added.toList ++ "\n" ++ body)
+    runOk "lake" #["build"] dir
+  finally
+    IO.FS.writeFile file original
+    runOk "lake" #["build"] dir
+
 def main : IO UInt32 := do
   runOk "lake" #["build", "lean-metrics"]
   let exe := (← IO.currentDir) / ".lake" / "build" / "bin" / "lean-metrics"
@@ -87,6 +127,10 @@ def main : IO UInt32 := do
       failed := failed + 1
       IO.println s!"FAIL  {dir.fileName}"
       for p in problems do IO.println s!"       {p}"
+  checkGraphIds exe
+  IO.println "ok    unique graph IDs and isolated nodes"
+  checkImportReplacement exe
+  IO.println "ok    emitted legacy imports compile"
   -- a source touched but unchanged is still what Lake built from
   let dir := fixtures / "scopes"
   runOk "touch" #[(dir / "Scopes" / "A.lean").toString]
diff --git a/lakefile.toml b/lakefile.toml
index 6c825f7..0753f7d 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,5 @@
 name = "leanMetrics"
-version = "0.1.0"
+version = "0.2.0"
 description = "Source and dependency-structure metrics for a Lean 4 Lake project."
 license = "Apache-2.0"
 licenseFiles = ["LICENSE", "NOTICE"]
diff --git a/test/fixtures/authored-projections/Case.lean b/test/fixtures/authored-projections/Case.lean
new file mode 100644
index 0000000..10fe4c6
--- /dev/null
+++ b/test/fixtures/authored-projections/Case.lean
@@ -0,0 +1,7 @@
+class Box where
+  value : Nat
+
+/-- This is an authored function, not a parent projection. -/
+def Box.toNat (b : Box) : Nat := b.value
+
+theorem read_box (b : Box) : b.toNat = b.value := rfl
diff --git a/test/fixtures/authored-projections/expected.json b/test/fixtures/authored-projections/expected.json
new file mode 100644
index 0000000..4472596
--- /dev/null
+++ b/test/fixtures/authored-projections/expected.json
@@ -0,0 +1,20 @@
+{
+  "metrics": {
+    "dep_graph": {
+      "n_graph_decls": 3,
+      "n_edges": 3,
+      "longest_pole": 2,
+      "n_internal_defs": 2,
+      "n_internal_theorems": 1
+    },
+    "docstrings": {
+      "n_doc_decls": 3,
+      "n_doc_documented": 1,
+      "doc_coverage": 0.333
+    }
+  },
+  "schema_version": 2,
+  "tool": {
+    "version": "0.2.0"
+  }
+}
diff --git a/test/fixtures/authored-projections/lakefile.toml b/test/fixtures/authored-projections/lakefile.toml
new file mode 100644
index 0000000..112e9bf
--- /dev/null
+++ b/test/fixtures/authored-projections/lakefile.toml
@@ -0,0 +1,5 @@
+name = "authored-projections"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
diff --git a/test/fixtures/authored-projections/lean-toolchain b/test/fixtures/authored-projections/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/authored-projections/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0
diff --git a/test/fixtures/instance-identity/Case.lean b/test/fixtures/instance-identity/Case.lean
new file mode 100644
index 0000000..6f4cc13
--- /dev/null
+++ b/test/fixtures/instance-identity/Case.lean
@@ -0,0 +1,17 @@
+module
+public section
+class Marker (α : Type) where
+  value : α
+
+@[expose, instance_reducible] def registered : Marker Nat := ⟨0⟩
+attribute [instance] registered
+attribute [instance] registered
+
+class Law : Prop where
+  proof : True
+
+section
+private local instance localNamed : Marker Bool := ⟨true⟩
+local instance : Marker Unit := ⟨()⟩
+local instance propNamed : Law := ⟨True.intro⟩
+end
diff --git a/test/fixtures/instance-identity/cases.json b/test/fixtures/instance-identity/cases.json
new file mode 100644
index 0000000..7be4c73
--- /dev/null
+++ b/test/fixtures/instance-identity/cases.json
@@ -0,0 +1,19 @@
+[
+  {
+    "args": [
+      "--metric",
+      "dep_graph"
+    ],
+    "expect": {
+      "metrics": {
+        "dep_graph": {
+          "n_graph_decls": 6,
+          "n_internal_instances": 4,
+          "n_internal_defs": 2,
+          "n_internal_theorems": 0
+        }
+      }
+    },
+    "exit": 0
+  }
+]
diff --git a/test/fixtures/instance-identity/expected.json b/test/fixtures/instance-identity/expected.json
new file mode 100644
index 0000000..0c39c01
--- /dev/null
+++ b/test/fixtures/instance-identity/expected.json
@@ -0,0 +1,19 @@
+{
+  "metrics": {
+    "declarations": {
+      "n_decls": 6,
+      "n_class": 2,
+      "n_def": 1,
+      "n_instance": 3,
+      "n_new_instances": 3,
+      "n_def_like": 6,
+      "n_instance_attribute_commands": 2
+    },
+    "dep_graph": {
+      "n_graph_decls": 6,
+      "n_internal_instances": 4,
+      "n_internal_defs": 2,
+      "n_internal_theorems": 0
+    }
+  }
+}
diff --git a/test/fixtures/instance-identity/lakefile.toml b/test/fixtures/instance-identity/lakefile.toml
new file mode 100644
index 0000000..22af021
--- /dev/null
+++ b/test/fixtures/instance-identity/lakefile.toml
@@ -0,0 +1,5 @@
+name = "instance-identity"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
diff --git a/test/fixtures/instance-identity/lean-toolchain b/test/fixtures/instance-identity/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/instance-identity/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0
diff --git a/test/fixtures/legacy-imports/Case.lean b/test/fixtures/legacy-imports/Case.lean
new file mode 100644
index 0000000..d0656c6
--- /dev/null
+++ b/test/fixtures/legacy-imports/Case.lean
@@ -0,0 +1,3 @@
+import Umbrella
+
+def result : Nat := keep
diff --git a/test/fixtures/legacy-imports/Dropped.lean b/test/fixtures/legacy-imports/Dropped.lean
new file mode 100644
index 0000000..aeff139
--- /dev/null
+++ b/test/fixtures/legacy-imports/Dropped.lean
@@ -0,0 +1 @@
+def drop : Nat := 2
diff --git a/test/fixtures/legacy-imports/Kept.lean b/test/fixtures/legacy-imports/Kept.lean
new file mode 100644
index 0000000..1c16bb5
--- /dev/null
+++ b/test/fixtures/legacy-imports/Kept.lean
@@ -0,0 +1 @@
+def keep : Nat := 1
diff --git a/test/fixtures/legacy-imports/Umbrella.lean b/test/fixtures/legacy-imports/Umbrella.lean
new file mode 100644
index 0000000..c9420b9
--- /dev/null
+++ b/test/fixtures/legacy-imports/Umbrella.lean
@@ -0,0 +1,2 @@
+import Kept
+import Dropped
diff --git a/test/fixtures/legacy-imports/cases.json b/test/fixtures/legacy-imports/cases.json
new file mode 100644
index 0000000..7eb2ef4
--- /dev/null
+++ b/test/fixtures/legacy-imports/cases.json
@@ -0,0 +1,28 @@
+[
+  {
+    "args": [
+      "--module",
+      "Case",
+      "--metric",
+      "import_minimizability",
+      "--details"
+    ],
+    "expect": {
+      "details": {
+        "import_minimizability": {
+          "remove_by_module": {
+            "Case": [
+              "import Umbrella"
+            ]
+          },
+          "add_by_module": {
+            "Case": [
+              "import Kept"
+            ]
+          }
+        }
+      }
+    },
+    "exit": 0
+  }
+]
diff --git a/test/fixtures/legacy-imports/expected.json b/test/fixtures/legacy-imports/expected.json
new file mode 100644
index 0000000..5791468
--- /dev/null
+++ b/test/fixtures/legacy-imports/expected.json
@@ -0,0 +1,3 @@
+{
+  "metrics": {}
+}
diff --git a/test/fixtures/legacy-imports/lakefile.toml b/test/fixtures/legacy-imports/lakefile.toml
new file mode 100644
index 0000000..e7d072c
--- /dev/null
+++ b/test/fixtures/legacy-imports/lakefile.toml
@@ -0,0 +1,6 @@
+name = "legacy-imports"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
+roots = ["Case", "Umbrella", "Kept", "Dropped"]
diff --git a/test/fixtures/legacy-imports/lean-toolchain b/test/fixtures/legacy-imports/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/legacy-imports/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0
diff --git a/test/fixtures/parent-projection/Case.lean b/test/fixtures/parent-projection/Case.lean
new file mode 100644
index 0000000..be929f0
--- /dev/null
+++ b/test/fixtures/parent-projection/Case.lean
@@ -0,0 +1,3 @@
+class Parent where
+  value : Nat
+class Child extends Parent
diff --git a/test/fixtures/parent-projection/expected.json b/test/fixtures/parent-projection/expected.json
new file mode 100644
index 0000000..253dc5b
--- /dev/null
+++ b/test/fixtures/parent-projection/expected.json
@@ -0,0 +1,10 @@
+{
+  "metrics": {
+    "dep_graph": {
+      "n_graph_decls": 2
+    },
+    "docstrings": {
+      "n_doc_decls": 2
+    }
+  }
+}
diff --git a/test/fixtures/parent-projection/lakefile.toml b/test/fixtures/parent-projection/lakefile.toml
new file mode 100644
index 0000000..0910279
--- /dev/null
+++ b/test/fixtures/parent-projection/lakefile.toml
@@ -0,0 +1,5 @@
+name = "parent-projection"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
diff --git a/test/fixtures/parent-projection/lean-toolchain b/test/fixtures/parent-projection/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/parent-projection/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0
diff --git a/test/fixtures/private-node-ids/Case.lean b/test/fixtures/private-node-ids/Case.lean
new file mode 100644
index 0000000..bd19dfe
--- /dev/null
+++ b/test/fixtures/private-node-ids/Case.lean
@@ -0,0 +1,4 @@
+import Case.A
+import Case.B
+
+def isolated : Nat := 0
diff --git a/test/fixtures/private-node-ids/Case/A.lean b/test/fixtures/private-node-ids/Case/A.lean
new file mode 100644
index 0000000..faace6c
--- /dev/null
+++ b/test/fixtures/private-node-ids/Case/A.lean
@@ -0,0 +1,2 @@
+private def helper : Nat := 1
+def resultA : Nat := helper
diff --git a/test/fixtures/private-node-ids/Case/B.lean b/test/fixtures/private-node-ids/Case/B.lean
new file mode 100644
index 0000000..bd9b83f
--- /dev/null
+++ b/test/fixtures/private-node-ids/Case/B.lean
@@ -0,0 +1,2 @@
+private def helper : Nat := 2
+def resultB : Nat := helper
diff --git a/test/fixtures/private-node-ids/cases.json b/test/fixtures/private-node-ids/cases.json
new file mode 100644
index 0000000..2f8faa5
--- /dev/null
+++ b/test/fixtures/private-node-ids/cases.json
@@ -0,0 +1,63 @@
+[
+  {
+    "args": [
+      "--main",
+      "resultA",
+      "--metric",
+      "dep_graph",
+      "--details"
+    ],
+    "expect": {
+      "metrics": {
+        "dep_graph": {
+          "root": "resultA",
+          "root_id": "resultA",
+          "reachable_from_root": 2
+        }
+      },
+      "details": {
+        "dep_graph": {
+          "edges": [
+            [
+              "_private.Case.A.0.helper",
+              "resultA"
+            ],
+            [
+              "_private.Case.B.0.helper",
+              "resultB"
+            ]
+          ]
+        }
+      }
+    },
+    "exit": 0
+  },
+  {
+    "args": [
+      "--main",
+      "_private.Case.A.0.helper",
+      "--metric",
+      "dep_graph"
+    ],
+    "exit": 0,
+    "expect": {
+      "metrics": {
+        "dep_graph": {
+          "root": "helper",
+          "root_id": "_private.Case.A.0.helper",
+          "reachable_from_root": 1
+        }
+      }
+    }
+  },
+  {
+    "args": [
+      "--main",
+      "helper",
+      "--metric",
+      "dep_graph"
+    ],
+    "exit": 2,
+    "expect": null
+  }
+]
diff --git a/test/fixtures/private-node-ids/expected.json b/test/fixtures/private-node-ids/expected.json
new file mode 100644
index 0000000..6245e8e
--- /dev/null
+++ b/test/fixtures/private-node-ids/expected.json
@@ -0,0 +1,8 @@
+{
+  "metrics": {
+    "dep_graph": {
+      "n_graph_decls": 5,
+      "n_edges": 2
+    }
+  }
+}
diff --git a/test/fixtures/private-node-ids/lakefile.toml b/test/fixtures/private-node-ids/lakefile.toml
new file mode 100644
index 0000000..394251a
--- /dev/null
+++ b/test/fixtures/private-node-ids/lakefile.toml
@@ -0,0 +1,5 @@
+name = "private-node-ids"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
diff --git a/test/fixtures/private-node-ids/lean-toolchain b/test/fixtures/private-node-ids/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/private-node-ids/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0
diff --git a/test/fixtures/proof-wrappers/Case.lean b/test/fixtures/proof-wrappers/Case.lean
new file mode 100644
index 0000000..8921bc3
--- /dev/null
+++ b/test/fixtures/proof-wrappers/Case.lean
@@ -0,0 +1,10 @@
+theorem termPlain : (0 : Nat) = 0 := rfl
+theorem termParen : (0 : Nat) = 0 := (rfl)
+theorem termTyped : (0 : Nat) = 0 := (rfl : (0 : Nat) = 0)
+theorem termOption : (0 : Nat) = 0 := set_option pp.universes true in rfl
+theorem termOpen : (0 : Nat) = 0 := open Nat in rfl
+theorem tacticPlain : (0 : Nat) = 0 := by rfl
+theorem tacticParen : (0 : Nat) = 0 := (by rfl)
+theorem tacticTyped : (0 : Nat) = 0 := (by rfl : (0 : Nat) = 0)
+theorem tacticOption : (0 : Nat) = 0 := set_option pp.universes true in by rfl
+theorem tacticOpen : (0 : Nat) = 0 := open Nat in by rfl
diff --git a/test/fixtures/proof-wrappers/expected.json b/test/fixtures/proof-wrappers/expected.json
new file mode 100644
index 0000000..8a10a1c
--- /dev/null
+++ b/test/fixtures/proof-wrappers/expected.json
@@ -0,0 +1,19 @@
+{
+  "metrics": {
+    "proof_mode": {
+      "n_pm_term": 5,
+      "n_pm_tactic": 5,
+      "pm_term_ratio": 0.5
+    },
+    "decide_usage": {
+      "n_dec_rfl": 10
+    },
+    "tactics": {
+      "n_tactic_calls": 5
+    },
+    "proof_size": {
+      "ps_calls_max": 1,
+      "ps_by_depth_max": 1
+    }
+  }
+}
diff --git a/test/fixtures/proof-wrappers/lakefile.toml b/test/fixtures/proof-wrappers/lakefile.toml
new file mode 100644
index 0000000..bb3a0a5
--- /dev/null
+++ b/test/fixtures/proof-wrappers/lakefile.toml
@@ -0,0 +1,5 @@
+name = "proof-wrappers"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
diff --git a/test/fixtures/proof-wrappers/lean-toolchain b/test/fixtures/proof-wrappers/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/proof-wrappers/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0
diff --git a/test/fixtures/recursion-strategy/Case.lean b/test/fixtures/recursion-strategy/Case.lean
new file mode 100644
index 0000000..236a669
--- /dev/null
+++ b/test/fixtures/recursion-strategy/Case.lean
@@ -0,0 +1,3 @@
+import Case.Structural
+import Case.Inferred
+import Case.Annotated
diff --git a/test/fixtures/recursion-strategy/Case/Annotated.lean b/test/fixtures/recursion-strategy/Case/Annotated.lean
new file mode 100644
index 0000000..ac935a2
--- /dev/null
+++ b/test/fixtures/recursion-strategy/Case/Annotated.lean
@@ -0,0 +1,7 @@
+module
+public section
+
+def annotated (n : Nat) : Nat :=
+  if n = 0 then 0 else annotated (n - 1)
+termination_by n
+decreasing_by omega
diff --git a/test/fixtures/recursion-strategy/Case/Inferred.lean b/test/fixtures/recursion-strategy/Case/Inferred.lean
new file mode 100644
index 0000000..8a857ea
--- /dev/null
+++ b/test/fixtures/recursion-strategy/Case/Inferred.lean
@@ -0,0 +1,2 @@
+def inferred (n : Nat) : Nat :=
+  if n = 0 then 0 else inferred (n - 1)
diff --git a/test/fixtures/recursion-strategy/Case/Structural.lean b/test/fixtures/recursion-strategy/Case/Structural.lean
new file mode 100644
index 0000000..e262d7b
--- /dev/null
+++ b/test/fixtures/recursion-strategy/Case/Structural.lean
@@ -0,0 +1,4 @@
+def length : (xs : List Nat) → Nat
+  | [] => 0
+  | _ :: xs => length xs + 1
+termination_by structural xs => xs
diff --git a/test/fixtures/recursion-strategy/cases.json b/test/fixtures/recursion-strategy/cases.json
new file mode 100644
index 0000000..ab60d19
--- /dev/null
+++ b/test/fixtures/recursion-strategy/cases.json
@@ -0,0 +1,40 @@
+[
+  {
+    "args": [
+      "--module",
+      "Case.Structural",
+      "--metric",
+      "recursion_style"
+    ],
+    "expect": {
+      "metrics": {
+        "recursion_style": {
+          "n_rec_termination_by": 1,
+          "n_rec_decreasing_by": 0,
+          "n_rec_well_founded": 0,
+          "rec_uses_well_founded": false
+        }
+      }
+    },
+    "exit": 0
+  },
+  {
+    "args": [
+      "--module",
+      "Case.Inferred",
+      "--metric",
+      "recursion_style"
+    ],
+    "expect": {
+      "metrics": {
+        "recursion_style": {
+          "n_rec_termination_by": 0,
+          "n_rec_decreasing_by": 0,
+          "n_rec_well_founded": 1,
+          "rec_uses_well_founded": true
+        }
+      }
+    },
+    "exit": 0
+  }
+]
diff --git a/test/fixtures/recursion-strategy/expected.json b/test/fixtures/recursion-strategy/expected.json
new file mode 100644
index 0000000..20cd08a
--- /dev/null
+++ b/test/fixtures/recursion-strategy/expected.json
@@ -0,0 +1,10 @@
+{
+  "metrics": {
+    "recursion_style": {
+      "n_rec_termination_by": 2,
+      "n_rec_decreasing_by": 1,
+      "n_rec_well_founded": 2,
+      "rec_uses_well_founded": true
+    }
+  }
+}
diff --git a/test/fixtures/recursion-strategy/lakefile.toml b/test/fixtures/recursion-strategy/lakefile.toml
new file mode 100644
index 0000000..7904eb9
--- /dev/null
+++ b/test/fixtures/recursion-strategy/lakefile.toml
@@ -0,0 +1,5 @@
+name = "recursion-strategy"
+defaultTargets = ["Case"]
+
+[[lean_lib]]
+name = "Case"
diff --git a/test/fixtures/recursion-strategy/lean-toolchain b/test/fixtures/recursion-strategy/lean-toolchain
new file mode 100644
index 0000000..12359f9
--- /dev/null
+++ b/test/fixtures/recursion-strategy/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.0