Map each reused result to the exact checked Alpha/Stable statement, dependency closure and first-admission evidence. Similar names, an ordinary Lean demo and source-only candidates do not discharge any IR obligation.
Method: structural-check. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.