Correct declaration, proof, recursion, and dependency metrics

[Vasily Ilin (Vilin97)]

The audit found several metrics that changed for reasons unrelated to the authored Lean code. For example, Peano's two local instances were reported as a theorem and a definition, and ODE's three instance-registration commands inflated its declaration count from 43 to 46. This change corrects the underlying counting and classification rules and adds reproducible regression projects.

Changes:

• Identify generated parent projections using Lean's structure metadata. Handwritten declarations such as Box.toNat and CommRing.toCommSemiring now remain in the graph and documentation metrics.
• Recover local instance identities from source selection ranges, including anonymous, private, and Prop-valued instances, since their registrations disappear on import.
• Count attribute [instance] separately from new declarations and instances.
• Ignore parentheses, type ascriptions, set_option … in, and open … in when classifying tactic proofs and term rfl; preserve actual tactic nesting depth.
• Use Lean's well-founded equation metadata instead of summing termination annotations. This includes inferred measures, excludes structural recursion, and counts a definition only once.
• Export unique graph node IDs, readable names, modules, isolated nodes, and root_id, so private names shared across modules do not collapse.
• Render valid plain import directives for files without a module header.

Bumps the tool to 0.2.0 and output schema to 2. Consumers should remeasure old baselines and use graph IDs for identity. The README also clarifies that the wrapper does not port the tool to arbitrary Lean releases.

Validation:

• lake test: all 34 fixture projects and four integration checks pass. The seven added projects cover six bug cases and a generated-parent-projection control; all six bug cases reproduce failures on the original binary.
• The import integration test applies the exact emitted directives and compiles the result. The emitted suggestions also compile for the symplectic determinant and ODE submissions.
• Ran all metrics on six submissions with Lean 4.34.0. Independent source and compiled-expression checks agree on 172 authored nodes, all 355 internal edges, chain lengths, root reachability, unrolled cost, and compression. Source counts, build-log counts, and output consistency checks also pass (108 checks total).

Submission	Authored graph nodes	Internal edges
Symplectic determinant	1	0
Banach–Alaoglu	6	8
Pascal	53	129
Linear ODE stability	43	52
Peano existence (new sample)	34	100
Abel–Ruffini (new sample)	35	66

Peano now reports 29 theorems, 3 definitions, and 2 local instances. Abel has 34 source declarations plus one authored local-notation parser, consistent with the graph's documented inclusion rule. Its graph checks found no additional defect. Restoring handwritten Mathlib declarations increases external dependency counts in all six samples; internal edges and graph costs remain unchanged.

Inputs: AxiomMath/lean-eval-rho at c645c4caf28ed1540bafe922bd61513e6e9e951c, over benchmark workspaces at e8eb893903723ec730c84e55b8eceb75916cf2f3, with Mathlib 5ed2965256430c3649e86755f9576b54eca72435. Each workspace was built first and measured with --lib Submission --module Submission --details, excluding challenge scaffolding. These checks exercise the metric implementation; they are not a claim of exhaustive correctness for every Lean construct.