Report unused statement dependencies, and count paths from every owning article

[Deicyde]

Replaces #147. This is #147 rebased onto 8f4f5c8, the final head of split/revision-impact, after #136 was rebuilt (9c2b43a). #136 merged into main while this was being tested, so it targets main; it merges cleanly with main's #149 docs changes.

autoform-impact/v1 is now on main without unused_statement_dependencies. This adds the key to v1 instead of bumping the schema, because no release ships v1 yet (the only release, v0, predates the impact layer).

The rebuilt layer's 901f5f8 already claims a revised declaration that no article names under every owner's target, or under its own lean/<slug>-<digest> key when it has no owner. That is what #147's 8940cc8 did, so this PR drops 8940cc8 and keeps 901f5f8's _claim_targets_for; the README sentence for that case follows 901f5f8's wording. The other three commits carry over unchanged apart from the rebase.

Commit	What it does	Was in #147
0364e0f	Adds unused_statement_dependencies: the stated articles whose Markdown statement rests on the revision through statement edges, but which are not statement-impacted. They join claim_targets and rule out contained. The probe follows names, so it misses a dependent whose Lean inlines a revised definition's body.	fff95bd (H7 from #142's d9f9e94, adapted)
7a23a94	Leaves mathlib: true articles out of that list. Their statement is a Mathlib declaration, and the loader refuses to retract them.	0f5d787 (#142 review item 2, 3bc24df)
e1301c6	Counts Markdown paths from every article that a revised declaration belongs to: the revised article, every article naming a revised declaration and, when none names it, its owners.	70fe798 (#142 review item 3)

Before e1301c6, --declaration X checked paths only from the selected article, which had two failures when X was named by another article T:

• A stated article whose statement rests on T was neither reported nor claimed.
• T itself, and the articles that depend on T, were reported as missing a dependency path.

The fff95bd port keeps this layer's plural helper owners, its exact source inventory, and its Markdown, Lean-source and build revision lines. The exact-format test now pins those revision lines (review item 4).

The revision-contract text that says how to handle an unused statement dependency belongs with the contract in the open-statements layer. It goes in the companion PR into split/open-statements.

Tests (on e1301c6)

• ruff check is clean.
• Without Lean, tests/test_impact.py gave 72 passed, 1 skipped. tests/test_claims.py and tests/test_work.py gave 117 passed.
• With real Lean (AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1), tests/test_impact.py gave 73 passed.
• Mutation check: dropping the owner loop or the anchor exclusion each fails test_markdown_paths_count_from_every_article_a_revised_declaration_belongs_to.

[Deicyde]

Exact-head review is complete at e1301c6. The net code/tests match the independently integrated H7 candidate: unused Markdown statement dependents are reported and claimed, Mathlib articles are excluded from impossible retraction, and reachability starts from every naming/owning article. #136's _claim_targets_for, plural ownership, bound source evidence, control snapshots, and revision lines are preserved. Both Python 3.10/3.13 runs, both Windows runs, both real-Lean runs, CLA, Ruff, and focused mutation/regression checks pass. No known blocker remains.