Reject formalized work the Lean cannot back, and report unused statement dependencies

[Deicyde]

Stacked on #115: the base is open-statements-revision, so the diff is this PR's commits only. Retarget to main once #115 lands.

This fixes two gaps from the #115 contract audit: H2 and H7.

What was wrong

• H2. proof: formalized without statement: formalized, or either one without a lean: name, showed as proved and passed autoform check. Only autoform audit flagged these states (proof-without-statement, missing-lean-target), and CI never runs audit. Open statements and a revision contract for shared Lean declarations #115 makes retraction routine, so a half-retracted article gets more likely.
• H7. work impact follows names. A Markdown statement dependent whose Lean inlines the revised definition's body, instead of naming it, was therefore not impacted, and the revision left it fully proved under the old meaning.

Changes

• The loader rejects both H2 states, under the audit's exact conditions: mathlib: true exempts neither, and lean: must yield a declaration name. The new load errors are:
  • ID: proof: formalized needs statement: formalized
  • ID: statement: formalized needs the lean: declaration that formalizes it (or proof: when only the proof is recorded)
• The two audit findings are now unreachable and are removed. So are doctor's missing-lean-target code and work's roadmap:proof-without-statement blocker, whose only path was the same state. Status derivation needed no change, since proved now implies stated.
• work impact reports unused_statement_dependencies. These are the stated articles that reach the revised article through Markdown statement edges, transitively, but are not statement-impacted. They join claim_targets and keep the revision from being contained, and the text report prints them on one line.
• The README covers the new load rule in the assertion table, the new field, and what contained now requires. It also says how the revision contract treats such an article: it is re-reviewed under the new meaning like a statement-impacted one, keeps statement only after an Agent Review, and otherwise records statement: retracted.
• In tests/test_contract.py, the random roadmaps now emit only states the loader accepts, and the invalid cases cover both new refusals.

Tests

New:

• tests/test_graph.py::test_rejects_formalized_work_the_lean_does_not_show
• tests/test_impact.py::test_stated_markdown_statement_dependents_the_lean_does_not_show_are_reported
• tests/test_impact.py::test_an_unused_statement_dependency_alone_keeps_a_revision_from_being_contained

Local runs at 3d1eb7d:

• ruff check autoform_cli servers tests: clean.
• Real Lean (AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1), tests/test_contract.py tests/test_impact.py: 64 passed; tests/test_lake_artifact_audit.py: 74 passed, 1 skipped. The skip is test_helper_runs_on_python_310, because python3.10 is not installed on this machine.
• Real Lean, the CI skeleton step's selection, tests/test_skeleton.py plus tests/test_project_inspect.py::test_stale_inherited_mathlib_is_ignored_by_real_lake: 162 passed.
• Full suite without Lean: 1260 passed, 45 skipped, 4 failed. The 4 failures are the tests/test_scaffold.py pin tests. They fail only because my local clone has no origin remote, so plugin_pin() finds no pin. In a clone with origin they pass (63 of 63), and they pass in CI.

Caveats

• Fixtures changed. Tests that built such articles for other purposes now name a lean: declaration or drop the assertion. Two tests are deleted along with the behavior they covered: test_proof_without_statement_returns_to_roadmap and test_work_assumptions_bounds_a_proof_recorded_without_its_statement. test_audit_reports_formalizable_structure_and_inconsistent_checked_facts loses its inconsistent-facts half and is renamed test_audit_reports_formalizable_structure.
• A project with such an article now fails autoform check where it passed before. The fix is to add the lean: name or drop the assertion, which autoform audit already asked for.
• A mathlib: true article counts as stated. One whose Markdown statement depends on the revised article can therefore appear in unused_statement_dependencies and in claim_targets, although it has nothing to retract.
• The comment at autoform_cli/__main__.py:556 still says the text report of work assumptions names conditional articles without lean:. After this change no such article exists, so the runtime-graph load that comment justifies is redundant. It is left as is.

[Deicyde]

This cannot be retargeted or merged as-is.

1. It is based on closed Open statements and a revision contract for shared Lean declarations #115. The valid replacement is Add all-or-nothing multi-target claims #135→Report Lean revision impact and deprecated targets #136→Add opt-in open statements and conditional proof status #138, but that split currently omitted four final Open statements and a revision contract for shared Lean declarations #115 commits (cc36d27e, 433de303, 88e2da46, 0237cd66). Your third commit modifies the missing contract test, so transplanting now produces a modify/delete conflict. Restore/adapt those fixes first.
2. unused_statement_dependencies gives mathlib nodes an impossible remediation: they count as stated and can be reported, but the prescribed statement: retracted state is forbidden with mathlib: true. Exclude them or define/test a mathlib-specific disposition.
3. With --declaration X, Markdown reachability is anchored only at the selected article. If X is named/owned by another article T, descendants of T are missed and left unreported/unclaimed. Anchor at every naming/owning article (including unowned/shared-owner cases) or restrict the override.
4. When porting H7 into Report Lean revision impact and deprecated targets #136, preserve plural helper owners/claim targets, Markdown/Lean/build revisions, exact source inventory, and post-probe freshness checks. The current exact-format test omits the newer revision lines.

Architecturally, fold H7 into #136 before autoform-impact/v1 freezes; place the H2 graph invariant after #138. Add mathlib, other-owner override, plural-owner/evidence, unowned revised-declaration, and restored real-Lean contract tests.

[Deicyde]

Replaced by #158 and #159. #158 carries the H2 commits (03bb33f, 3d1eb7d, 9446635) onto main. #159, stacked on #158, carries the revision-contract text from d9f9e94; the impact half of d9f9e94 is already on main through #150. This PR's base, open-statements-revision, will not merge now that #115 has landed in split form.