Dependency Distance Audits Descendant Leakage in Lean Proving Benchmarks

Lean proving benchmarks sometimes remove the target theorem from retrieval while importing the completed library. This protocol can still expose target-descendant declarations whose stored types or values transitively depend on the target. A proof using such a declaration is valid in the completed environment but does not establish that the target can be proved from its original environment. We introduce a dependency-distance audit over all project declarations and apply it to a 200-target case study with static and adaptive (agentic) retrieval. About one quarter of completed-valid proofs in each target-excluding BM25 condition use a detected descendant, usually through a direct dependency; extending a theorem-only graph to definitions also exposes a previously missed case. The audit describes the generated proof artifact and does not reconstruct source chronology. We therefore recommend reporting completed-environment validity and descendant-free validity separately, while reserving claims of historical availability for evaluations that recreate the target's source position.