From 0364e0fea6895798b6f61a216812f911adccac80 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 5 Oct 2026 15:02:32 -0400
Subject: [PATCH 1/3] Report stated statement dependents that work impact
 cannot see

The impact probe follows names, so a Markdown statement dependent whose Lean
inlines the revised definition's body instead of naming it was not impacted,
and the revision left it fully proved under the old meaning. The report now
lists unused_statement_dependencies: 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 describes the field and what contained now requires. How the
revision contract treats such an article belongs with the contract, in the
open-statements layer.

Restored from closed #115 (d9f9e94) and adapted to this layer's plural
helper owners and Lean source and build revision lines.
---
 autoform_cli/README.md | 11 ++++--
 autoform_cli/impact.py | 51 +++++++++++++++++++-----
 tests/test_impact.py   | 90 +++++++++++++++++++++++++++++++++++++++---
 3 files changed, 135 insertions(+), 17 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index d59bb6fd..f3211d03 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -536,9 +536,14 @@ the change is contained, and the complete `claim_targets` set. Helpers shared
 by several articles contribute every owner's claim; an unowned helper gets a
 stable `lean/<slug>-<digest>` target. A revised declaration that no article
 names is claimed the same way, under every nearest owner's target or its own
-stable key. A revision is contained exactly when the selected article's target
-is its only claim target. Project locality is an exact inventory of regular
-repository source modules, never a namespace-prefix guess.
+stable key. `unused_statement_dependencies` lists the stated articles whose
+Markdown statement rests on the revised article, directly or through other
+statement dependencies, that are not statement-impacted: the probe follows
+names, so a dependent whose Lean inlines a revised definition's body shows no
+use although its statement changes meaning. They join `claim_targets` too. A
+revision is contained exactly when the selected article's target is its only
+claim target. Project locality is an exact inventory of regular repository
+source modules, never a namespace-prefix guess.
 
 The command snapshots and rereads the roadmap around the probe. It retains one
 bound Lean source generation, derives module inventory and locations from that
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index a470081e..047675dd 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -320,6 +320,8 @@ class ImpactArticle:
     article_id: str | None
     declarations: tuple[str, ...]
     dependencies: tuple[str, ...] = ()
+    statement_dependencies: tuple[str, ...] = ()
+    stated: bool = False
 
     @property
     def claim_target(self) -> str:
@@ -409,6 +411,10 @@ class ImpactReport:
     proof_impacted: tuple[ImpactedArticle, ...]
     helpers: tuple[ImpactHelper, ...]
     undeclared_dependencies: tuple[str, ...]
+    #: Stated articles whose Markdown statement rests on the revised article,
+    #: through statement edges only, that are not statement-impacted: their Lean
+    #: may inline a revised definition's body instead of naming it.
+    unused_statement_dependencies: tuple[str, ...]
     deprecated: tuple[DeprecatedConstant, ...]
     deprecated_unused: tuple[str, ...]
     claim_targets: tuple[str, ...]
@@ -420,9 +426,10 @@ def contained(self) -> bool:
         A helper the revised article owns, such as a structure's generated
         constructor or recursor, is repaired under that article's claim, so it
         does not count; any other helper, owned or not, does, and so does a
-        revised declaration that belongs to another article or to none. The
-        revision is contained exactly when its only claim target is the
-        revised article's.
+        revised declaration that belongs to another article or to none, or a
+        stated article whose Markdown statement rests on the revised one, even
+        when its Lean shows no use. The revision is contained exactly when its
+        only claim target is the revised article's.
         """
 
         return self.claim_targets == (self.article.claim_target,)
@@ -444,6 +451,7 @@ def as_dict(self) -> dict[str, object]:
             "proof_impacted": [item.as_dict() for item in self.proof_impacted],
             "helpers": [helper.as_dict() for helper in self.helpers],
             "undeclared_dependencies": list(self.undeclared_dependencies),
+            "unused_statement_dependencies": list(self.unused_statement_dependencies),
             "deprecated": [item.as_dict() for item in self.deprecated],
             "deprecated_unused": list(self.deprecated_unused),
             "claim_targets": list(self.claim_targets),
@@ -549,6 +557,18 @@ def compute_impact(
 
     impacted = (*statement_impacted, *proof_impacted)
     undeclared = sorted(item.id for item in impacted if not _reaches(item.id, revised.id, by_id))
+    # The probe sees only names, so a dependent whose Lean inlines a revised
+    # definition's body instead of naming it would keep its statement under the
+    # old meaning; its Markdown statement dependency is the only trace.
+    statement_ids = {item.id for item in statement_impacted}
+    unused = sorted(
+        article.id
+        for article in articles
+        if article.stated
+        and article.id != revised.id
+        and article.id not in statement_ids
+        and _reaches(article.id, revised.id, by_id, statement_only=True)
+    )
 
     deprecated_users: dict[str, set[str]] = {}
     for record in records.values():
@@ -568,9 +588,11 @@ def compute_impact(
     # A helper is repaired under every owning article's claim; an unowned
     # helper contributes the key derived from its own name.
     # A revised declaration no article names is claimed the same way.
-    others = {item.claim_target for item in impacted} | {
-        target for helper in helpers for target in helper.claim_targets
-    }
+    others = (
+        {item.claim_target for item in impacted}
+        | {by_id[article_id].claim_target for article_id in unused}
+        | {target for helper in helpers for target in helper.claim_targets}
+    )
     for name in revised_names:
         if name not in named:
             others.update(_claim_targets_for(name, _owners(records[name], records, named), by_id))
@@ -585,6 +607,7 @@ def compute_impact(
         proof_impacted=tuple(proof_impacted),
         helpers=tuple(helpers),
         undeclared_dependencies=tuple(undeclared),
+        unused_statement_dependencies=tuple(unused),
         deprecated=deprecated,
         deprecated_unused=tuple(item.name for item in deprecated if not item.users and not item.articles),
         claim_targets=claim_targets,
@@ -694,14 +717,17 @@ def _descends_from(record: ConstantRecord, ancestor: str, records: Mapping[str,
     return False
 
 
-def _reaches(start: str, target: str, articles: Mapping[str, ImpactArticle]) -> bool:
-    """Whether ``start`` reaches ``target`` through Markdown dependencies."""
+def _reaches(
+    start: str, target: str, articles: Mapping[str, ImpactArticle], *, statement_only: bool = False
+) -> bool:
+    """Whether ``start`` reaches ``target`` through Markdown dependencies, or only statement ones."""
 
     seen = {start}
     work = [start]
     while work:
         article = articles.get(work.pop())
-        for dependency in article.dependencies if article is not None else ():
+        edges = () if article is None else article.statement_dependencies if statement_only else article.dependencies
+        for dependency in edges:
             if dependency == target:
                 return True
             if dependency not in seen:
@@ -779,6 +805,8 @@ def revision_impact(
             node.article_id,
             tuple(dict.fromkeys(target.declaration for target in node.lean_targets)),
             tuple(node.dependencies),
+            tuple(node.statement_dependencies),
+            node.status.stated,
         )
         for node in runtime.nodes
     }
@@ -891,6 +919,11 @@ def format_impact(report: ImpactReport) -> list[str]:
             "Impacted without a Markdown dependency path to the revised article: "
             + ", ".join(report.undeclared_dependencies)
         )
+    if report.unused_statement_dependencies:
+        lines.append(
+            "Statement dependents in Markdown that are not statement impacted: "
+            + ", ".join(report.unused_statement_dependencies)
+        )
     if report.deprecated:
         lines.append("Deprecated:")
         for item in report.deprecated:
diff --git a/tests/test_impact.py b/tests/test_impact.py
index 564d9ff2..06e3802d 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -56,9 +56,14 @@ def _records(*records: ConstantRecord) -> dict[str, ConstantRecord]:
 
 
 def _article(
-    node_id: str, *declarations: str, article_id: str | None = None, dependencies: tuple[str, ...] = ()
+    node_id: str,
+    *declarations: str,
+    article_id: str | None = None,
+    dependencies: tuple[str, ...] = (),
+    statement_dependencies: tuple[str, ...] = (),
+    stated: bool = False,
 ) -> ImpactArticle:
-    return ImpactArticle(node_id, article_id, declarations, dependencies)
+    return ImpactArticle(node_id, article_id, declarations, dependencies, statement_dependencies, stated)
 
 
 def _impact(records, articles, revised: str, declarations=None, **kwargs):
@@ -293,6 +298,64 @@ def test_undeclared_dependencies_and_claim_targets() -> None:
     assert report.claim_targets == ("af_base", "af_detached", "af_direct", "af_loose", "chapter/transitive")
 
 
+def test_stated_markdown_statement_dependents_the_lean_does_not_show_are_reported() -> None:
+    records = _records(
+        _rec("A.base", "def"),
+        _rec("A.direct", type_uses=("A.base",)),
+        _rec("A.inlined"),
+        _rec("A.proofOnly", value_uses=("A.base",)),
+        _rec("A.unstated"),
+        _rec("A.viaProof"),
+    )
+
+    def stated(node_id: str, *declarations: str, on: str = "base", **fields: object) -> ImpactArticle:
+        return _article(node_id, *declarations, dependencies=(on,), statement_dependencies=(on,), stated=True, **fields)
+
+    articles = [
+        _article("base", "A.base", article_id="af_base", stated=True),
+        stated("direct", "A.direct"),
+        # Unstated and named by no article: it only carries the statement edge.
+        _article("middle", dependencies=("base",), statement_dependencies=("base",)),
+        stated("inlined", "A.inlined", on="middle", article_id="af_inlined"),
+        stated("proof-only", "A.proofOnly"),
+        _article("unstated", "A.unstated", dependencies=("base",), statement_dependencies=("base",)),
+        _article("via-proof", "A.viaProof", dependencies=("base",), stated=True),
+    ]
+
+    report = _impact(records, articles, "base")
+
+    assert _ids(report.statement_impacted) == ["direct"]
+    assert _ids(report.proof_impacted) == ["proof-only"]
+    assert report.unused_statement_dependencies == ("inlined", "proof-only")
+    assert report.as_dict()["unused_statement_dependencies"] == ["inlined", "proof-only"]
+    assert report.claim_targets == ("af_base", "af_inlined", "direct", "proof-only")
+    assert "Statement dependents in Markdown that are not statement impacted: inlined, proof-only" in (
+        format_impact(report)
+    )
+
+
+def test_an_unused_statement_dependency_alone_keeps_a_revision_from_being_contained() -> None:
+    records = _records(_rec("A.leaf", "def"), _rec("A.inlined"))
+    articles = [
+        _article("leaf", "A.leaf", stated=True),
+        _article("inlined", "A.inlined", dependencies=("leaf",), statement_dependencies=("leaf",), stated=True),
+    ]
+
+    report = _impact(records, articles, "leaf")
+
+    assert not report.contained
+    assert report.claim_targets == ("leaf", "inlined")
+    lines = format_impact(report)
+    assert lines.pop(2) == "Lean source revision: unbound"
+    assert re.fullmatch(r"Lean build revision: [0-9a-f]{64}", lines.pop(2))
+    assert lines == [
+        "Revising A.leaf of leaf",
+        "Graph source revision: rev",
+        "Statement dependents in Markdown that are not statement impacted: inlined",
+        "Claim targets: leaf, inlined",
+    ]
+
+
 def test_deprecated_constants_report_users_through_internal_details() -> None:
     records = _records(
         _rec("A.new"),
@@ -928,7 +991,7 @@ def _write_article(
 
 
 def _blueprint_project(tmp_path: Path, prefix: str) -> Path:
-    """A roadmap whose articles name ``{prefix}.base``, ``.uses``, ``.loose`` and nothing."""
+    """A roadmap whose articles name ``{prefix}.base``, ``.uses``, ``.loose``, ``.inlines`` and nothing."""
 
     project = tmp_path / "project"
     _write_article(project, "README.md", title="Chapter", metadata=["article_id: af_0000000000000000000000c0"])
@@ -948,6 +1011,12 @@ def _blueprint_project(tmp_path: Path, prefix: str) -> Path:
         "loose.md",
         metadata=["declaration: theorem", "statement: formalized", f"lean: {prefix}.loose"],
     )
+    _write_article(
+        project,
+        "inlines.md",
+        metadata=["declaration: theorem", "statement: formalized", f"lean: {prefix}.inlines"],
+        depends=("base.md",),
+    )
     _write_article(project, "empty.md", metadata=["declaration: theorem"])
     return project
 
@@ -968,6 +1037,7 @@ def _stub_lean_root(tmp_path: Path) -> Path:
     _payload("Demo.uses", type_uses=["Demo.base"]),
     _payload("Demo.base_eq", type_uses=["Demo.base"]),
     _payload("Demo.loose", value_uses=["Demo.base", "Demo.old"], uses_deprecated=["Demo.old"]),
+    _payload("Demo.inlines"),
     _payload("Demo.old", deprecated=True, replacement="Demo.base_eq"),
     _payload("Demo.gone", deprecated=True),
 ]
@@ -1028,12 +1098,19 @@ def test_cli_writes_the_impact_report_as_canonical_json(tmp_path: Path, monkeypa
             }
         ],
         "undeclared_dependencies": ["chapter/loose"],
+        "unused_statement_dependencies": ["chapter/inlines"],
         "deprecated": [
             {"name": "Demo.gone", "replacement": None, "users": [], "articles": []},
             {"name": "Demo.old", "replacement": "Demo.base_eq", "users": ["Demo.loose"], "articles": []},
         ],
         "deprecated_unused": ["Demo.gone"],
-        "claim_targets": [_BASE_ID, _USES_ID, "chapter/loose", "lean/demo-base-eq-7f17aa41d1461243"],
+        "claim_targets": [
+            _BASE_ID,
+            _USES_ID,
+            "chapter/inlines",
+            "chapter/loose",
+            "lean/demo-base-eq-7f17aa41d1461243",
+        ],
     }
     (call,) = calls
     assert call["label"] == "impact probe"
@@ -1065,10 +1142,11 @@ def test_cli_text_report_lists_each_section(tmp_path: Path, monkeypatch, capsys)
         "Helpers no article names:",
         "  Demo.base_eq (theorem, statement) Demo.lean:5; no owner; claims lean/demo-base-eq-7f17aa41d1461243",
         "Impacted without a Markdown dependency path to the revised article: chapter/loose",
+        "Statement dependents in Markdown that are not statement impacted: chapter/inlines",
         "Deprecated:",
         "  Demo.gone: no users, safe to delete",
         "  Demo.old -> Demo.base_eq: used by Demo.loose",
-        f"Claim targets: {_BASE_ID}, {_USES_ID}, chapter/loose, lean/demo-base-eq-7f17aa41d1461243",
+        f"Claim targets: {_BASE_ID}, {_USES_ID}, chapter/inlines, chapter/loose, lean/demo-base-eq-7f17aa41d1461243",
     ]
     assert calls[0]["timeout"] == skeleton.DEFAULT_PROBE_TIMEOUT
 
@@ -1597,6 +1675,8 @@ def recorded(*args: object, **kwargs: object) -> str:
         ("Imp.usesOld", "theorem", "statement", "Imp/Extra.lean", 10, []),
     ]
     assert report["undeclared_dependencies"] == ["chapter/simp"]
+    # proved.md states on uses.md in Markdown, but its Lean statement does not mention base.
+    assert report["unused_statement_dependencies"] == ["chapter/proved"]
     # The equation lemma `@[simp]` gives oldSeed goes when oldSeed does.
     assert report["deprecated"] == [
         {"name": "Imp.oldEq", "replacement": "Imp.base_eq", "users": ["Imp.usesOld"], "articles": []},

From 7a23a946aec8e78ccb20d5b183ad16128419dfa6 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 5 Oct 2026 17:31:56 -0400
Subject: [PATCH 2/3] Leave Mathlib articles out of unused statement
 dependencies

A mathlib: true article counts as stated, so one whose Markdown statement
depends on the revised article was reported in unused_statement_dependencies
and claimed, although its statement is a Mathlib declaration that cannot use
the revised one and the loader refuses to retract it.

Restored from closed #115's review follow-ups (3bc24df).
---
 autoform_cli/README.md |  4 +++-
 autoform_cli/impact.py | 20 +++++++++++++-------
 tests/test_impact.py   | 25 ++++++++++++++++++++++++-
 3 files changed, 40 insertions(+), 9 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index f3211d03..67c7d735 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -541,7 +541,9 @@ Markdown statement rests on the revised article, directly or through other
 statement dependencies, that are not statement-impacted: the probe follows
 names, so a dependent whose Lean inlines a revised definition's body shows no
 use although its statement changes meaning. They join `claim_targets` too. A
-revision is contained exactly when the selected article's target is its only
+`mathlib: true` article is left out: its statement is a Mathlib declaration,
+which cannot use the revised one, and it cannot record `statement: retracted`.
+A revision is contained exactly when the selected article's target is its only
 claim target. Project locality is an exact inventory of regular repository
 source modules, never a namespace-prefix guess.
 
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index 047675dd..6d3aaaff 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -322,6 +322,7 @@ class ImpactArticle:
     dependencies: tuple[str, ...] = ()
     statement_dependencies: tuple[str, ...] = ()
     stated: bool = False
+    mathlib: bool = False
 
     @property
     def claim_target(self) -> str:
@@ -411,9 +412,10 @@ class ImpactReport:
     proof_impacted: tuple[ImpactedArticle, ...]
     helpers: tuple[ImpactHelper, ...]
     undeclared_dependencies: tuple[str, ...]
-    #: Stated articles whose Markdown statement rests on the revised article,
-    #: through statement edges only, that are not statement-impacted: their Lean
-    #: may inline a revised definition's body instead of naming it.
+    #: Stated articles other than Mathlib ones whose Markdown statement rests on
+    #: the revised article, through statement edges only, that are not
+    #: statement-impacted: their Lean may inline a revised definition's body
+    #: instead of naming it.
     unused_statement_dependencies: tuple[str, ...]
     deprecated: tuple[DeprecatedConstant, ...]
     deprecated_unused: tuple[str, ...]
@@ -427,9 +429,9 @@ def contained(self) -> bool:
         constructor or recursor, is repaired under that article's claim, so it
         does not count; any other helper, owned or not, does, and so does a
         revised declaration that belongs to another article or to none, or a
-        stated article whose Markdown statement rests on the revised one, even
-        when its Lean shows no use. The revision is contained exactly when its
-        only claim target is the revised article's.
+        stated article, other than a Mathlib one, whose Markdown statement rests
+        on the revised one, even when its Lean shows no use. The revision is
+        contained exactly when its only claim target is the revised article's.
         """
 
         return self.claim_targets == (self.article.claim_target,)
@@ -559,12 +561,15 @@ def compute_impact(
     undeclared = sorted(item.id for item in impacted if not _reaches(item.id, revised.id, by_id))
     # The probe sees only names, so a dependent whose Lean inlines a revised
     # definition's body instead of naming it would keep its statement under the
-    # old meaning; its Markdown statement dependency is the only trace.
+    # old meaning; its Markdown statement dependency is the only trace. A
+    # Mathlib article's statement is a Mathlib declaration, which cannot use the
+    # revised one, and the loader refuses to retract it, so it is left out.
     statement_ids = {item.id for item in statement_impacted}
     unused = sorted(
         article.id
         for article in articles
         if article.stated
+        and not article.mathlib
         and article.id != revised.id
         and article.id not in statement_ids
         and _reaches(article.id, revised.id, by_id, statement_only=True)
@@ -807,6 +812,7 @@ def revision_impact(
             tuple(node.dependencies),
             tuple(node.statement_dependencies),
             node.status.stated,
+            node.mathlib,
         )
         for node in runtime.nodes
     }
diff --git a/tests/test_impact.py b/tests/test_impact.py
index 06e3802d..008dc4e6 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -62,8 +62,9 @@ def _article(
     dependencies: tuple[str, ...] = (),
     statement_dependencies: tuple[str, ...] = (),
     stated: bool = False,
+    mathlib: bool = False,
 ) -> ImpactArticle:
-    return ImpactArticle(node_id, article_id, declarations, dependencies, statement_dependencies, stated)
+    return ImpactArticle(node_id, article_id, declarations, dependencies, statement_dependencies, stated, mathlib)
 
 
 def _impact(records, articles, revised: str, declarations=None, **kwargs):
@@ -320,6 +321,8 @@ def stated(node_id: str, *declarations: str, on: str = "base", **fields: object)
         stated("proof-only", "A.proofOnly"),
         _article("unstated", "A.unstated", dependencies=("base",), statement_dependencies=("base",)),
         _article("via-proof", "A.viaProof", dependencies=("base",), stated=True),
+        # Stated by Mathlib, whose declaration cannot use A.base.
+        stated("in-mathlib", mathlib=True),
     ]
 
     report = _impact(records, articles, "base")
@@ -1056,6 +1059,26 @@ def run_probe(probe: str, lean_root: Path, **kwargs: object) -> str:
     return calls
 
 
+def test_cli_leaves_a_mathlib_statement_dependent_unclaimed(tmp_path: Path, monkeypatch, capsys) -> None:
+    project = _blueprint_project(tmp_path, "Demo")
+    _write_article(
+        project,
+        "known.md",
+        metadata=["declaration: theorem", "mathlib: true", "mathlib_declaration: Nat.add_zero"],
+        depends=("base.md",),
+    )
+    lean_root = _stub_lean_root(tmp_path)
+    _stub_probe(monkeypatch)
+
+    code = cli.main(["work", "impact", _BASE_ID, str(project), "--lean-root", str(lean_root), "--json"])
+
+    output = capsys.readouterr()
+    assert code == 0, output.err
+    report = json.loads(output.out)
+    assert report["unused_statement_dependencies"] == ["chapter/inlines"]
+    assert "chapter/known" not in report["claim_targets"]
+
+
 def test_cli_writes_the_impact_report_as_canonical_json(tmp_path: Path, monkeypatch, capsys) -> None:
     project = _blueprint_project(tmp_path, "Demo")
     lean_root = _stub_lean_root(tmp_path)

From e1301c6478940c0ddac30be9f33cf130fdce8285 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 5 Oct 2026 19:23:21 -0400
Subject: [PATCH 3/3] Count Markdown paths from every article a revised
 declaration belongs to

work impact checked Markdown paths only against the selected article. With
--declaration X where another article T names X, or owns it when no article
does, a stated article whose Markdown statement rests on T was neither
reported in unused_statement_dependencies nor claimed, although inlining X
changes its statement, while T and the articles depending on T were reported
as missing a dependency path. Both checks now start from the revised article
and every article naming a revised declaration or, when none names it, owning
it; an unowned declaration adds no article.
---
 autoform_cli/README.md |  9 ++++++---
 autoform_cli/impact.py | 32 ++++++++++++++++++++----------
 tests/test_impact.py   | 45 +++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 72 insertions(+), 14 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index 67c7d735..f638c6a6 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -537,15 +537,18 @@ by several articles contribute every owner's claim; an unowned helper gets a
 stable `lean/<slug>-<digest>` target. A revised declaration that no article
 names is claimed the same way, under every nearest owner's target or its own
 stable key. `unused_statement_dependencies` lists the stated articles whose
-Markdown statement rests on the revised article, directly or through other
+Markdown statement rests on the revised declarations, directly or through other
 statement dependencies, that are not statement-impacted: the probe follows
 names, so a dependent whose Lean inlines a revised definition's body shows no
 use although its statement changes meaning. They join `claim_targets` too. A
 `mathlib: true` article is left out: its statement is a Mathlib declaration,
 which cannot use the revised one, and it cannot record `statement: retracted`.
 A revision is contained exactly when the selected article's target is its only
-claim target. Project locality is an exact inventory of regular repository
-source modules, never a namespace-prefix guess.
+claim target. A Markdown path reaches the revised declarations when it ends at
+the revised article or at an article that names one of them or, when none names
+it, owns it; missing dependency paths are counted the same way. Project
+locality is an exact inventory of regular repository source modules, never a
+namespace-prefix guess.
 
 The command snapshots and rereads the roadmap around the probe. It retains one
 bound Lean source generation, derives module inventory and locations from that
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index 6d3aaaff..a1cee21a 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -14,7 +14,7 @@
 import hashlib
 import json
 import re
-from collections.abc import Callable, Iterable, Mapping, Sequence
+from collections.abc import Callable, Collection, Iterable, Mapping, Sequence
 from dataclasses import asdict, dataclass
 from pathlib import Path
 
@@ -411,9 +411,12 @@ class ImpactReport:
     statement_impacted: tuple[ImpactedArticle, ...]
     proof_impacted: tuple[ImpactedArticle, ...]
     helpers: tuple[ImpactHelper, ...]
+    #: Impacted articles with no Markdown dependency path to the revised
+    #: declarations: to the revised article, or to an article naming one of
+    #: them or, when none names it, owning it.
     undeclared_dependencies: tuple[str, ...]
     #: Stated articles other than Mathlib ones whose Markdown statement rests on
-    #: the revised article, through statement edges only, that are not
+    #: the revised declarations, through statement edges only, that are not
     #: statement-impacted: their Lean may inline a revised definition's body
     #: instead of naming it.
     unused_statement_dependencies: tuple[str, ...]
@@ -430,8 +433,9 @@ def contained(self) -> bool:
         does not count; any other helper, owned or not, does, and so does a
         revised declaration that belongs to another article or to none, or a
         stated article, other than a Mathlib one, whose Markdown statement rests
-        on the revised one, even when its Lean shows no use. The revision is
-        contained exactly when its only claim target is the revised article's.
+        on the revised declarations, even when its Lean shows no use. The
+        revision is contained exactly when its only claim target is the revised
+        article's.
         """
 
         return self.claim_targets == (self.article.claim_target,)
@@ -557,8 +561,16 @@ def compute_impact(
             ImpactHelper(name, record.kind, impact, record.module, path, line, owners, targets)
         )
 
+    # A revised declaration belongs to the articles naming it or, when none
+    # does, to its owners, so a Markdown path to any of them reaches the
+    # revision as surely as a path to the revised article does.
+    anchors = {revised.id}
+    for name in revised_names:
+        anchors.update(named.get(name) or _owners(records[name], records, named))
     impacted = (*statement_impacted, *proof_impacted)
-    undeclared = sorted(item.id for item in impacted if not _reaches(item.id, revised.id, by_id))
+    undeclared = sorted(
+        item.id for item in impacted if item.id not in anchors and not _reaches(item.id, anchors, by_id)
+    )
     # The probe sees only names, so a dependent whose Lean inlines a revised
     # definition's body instead of naming it would keep its statement under the
     # old meaning; its Markdown statement dependency is the only trace. A
@@ -572,7 +584,7 @@ def compute_impact(
         and not article.mathlib
         and article.id != revised.id
         and article.id not in statement_ids
-        and _reaches(article.id, revised.id, by_id, statement_only=True)
+        and _reaches(article.id, anchors, by_id, statement_only=True)
     )
 
     deprecated_users: dict[str, set[str]] = {}
@@ -723,9 +735,9 @@ def _descends_from(record: ConstantRecord, ancestor: str, records: Mapping[str,
 
 
 def _reaches(
-    start: str, target: str, articles: Mapping[str, ImpactArticle], *, statement_only: bool = False
+    start: str, targets: Collection[str], articles: Mapping[str, ImpactArticle], *, statement_only: bool = False
 ) -> bool:
-    """Whether ``start`` reaches ``target`` through Markdown dependencies, or only statement ones."""
+    """Whether ``start`` reaches one of ``targets`` through Markdown dependencies, or only statement ones."""
 
     seen = {start}
     work = [start]
@@ -733,7 +745,7 @@ def _reaches(
         article = articles.get(work.pop())
         edges = () if article is None else article.statement_dependencies if statement_only else article.dependencies
         for dependency in edges:
-            if dependency == target:
+            if dependency in targets:
                 return True
             if dependency not in seen:
                 seen.add(dependency)
@@ -922,7 +934,7 @@ def format_impact(report: ImpactReport) -> list[str]:
             )
     if report.undeclared_dependencies:
         lines.append(
-            "Impacted without a Markdown dependency path to the revised article: "
+            "Impacted without a Markdown dependency path to the revised declarations: "
             + ", ".join(report.undeclared_dependencies)
         )
     if report.unused_statement_dependencies:
diff --git a/tests/test_impact.py b/tests/test_impact.py
index 008dc4e6..c14e491a 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -688,6 +688,49 @@ def test_declaration_override_claims_every_owner_of_the_revised_declaration() ->
     assert own.contained
 
 
+def test_markdown_paths_count_from_every_article_a_revised_declaration_belongs_to() -> None:
+    records = _records(
+        _rec("A.R", "def"),
+        _rec("A.X", "def"),
+        _rec("A.O", "def"),
+        _rec("A.O.aux", "def", parent="A.O"),
+        _rec("A.loose", "def"),
+        _rec("A.useX", type_uses=("A.X",)),
+        _rec("A.inlinesX"),
+        _rec("A.inlinesAux"),
+    )
+
+    def stated(node_id: str, *declarations: str, on: str) -> ImpactArticle:
+        return _article(node_id, *declarations, dependencies=(on,), statement_dependencies=(on,), stated=True)
+
+    articles = [
+        _article("r", "A.R"),
+        _article("t", "A.X", stated=True),
+        _article("o-a", "A.O"),
+        _article("o-b", "A.O"),
+        _article("uses-x", "A.useX", dependencies=("t",)),
+        stated("inlines-x", "A.inlinesX", on="t"),
+        stated("inlines-aux", "A.inlinesAux", on="o-b"),
+    ]
+
+    named = _impact(records, articles, "r", ["A.X"])
+    owned = _impact(records, articles, "r", ["A.O.aux"])
+    unowned = _impact(records, articles, "r", ["A.loose"])
+
+    # A.X belongs to t, so t needs no path to r, a path to t declares uses-x,
+    # and inlines-x rests on A.X through t although its Lean shows no use.
+    assert _ids(named.statement_impacted) == ["t", "uses-x"]
+    assert named.undeclared_dependencies == ()
+    assert named.unused_statement_dependencies == ("inlines-x",)
+    assert named.claim_targets == ("r", "inlines-x", "t", "uses-x")
+    # The unnamed A.O.aux belongs to both of A.O's articles.
+    assert owned.unused_statement_dependencies == ("inlines-aux",)
+    assert owned.claim_targets == ("r", "inlines-aux", "o-a", "o-b")
+    # A.loose belongs to no article, so only paths to r count.
+    assert unowned.unused_statement_dependencies == ()
+    assert unowned.claim_targets == ("r", _lean_key("A.loose"))
+
+
 def test_an_unowned_helper_claim_key_is_ref_safe_for_any_name() -> None:
     names = ("_private.Demo.Extra.0.A.priv", "A.«weird name»", "«∀»", "A." + "long" * 20)
     records = _records(_rec("A.base", "def"), *(_rec(name, type_uses=("A.base",)) for name in names))
@@ -1164,7 +1207,7 @@ def test_cli_text_report_lists_each_section(tmp_path: Path, monkeypatch, capsys)
         "  chapter/loose: Demo.loose",
         "Helpers no article names:",
         "  Demo.base_eq (theorem, statement) Demo.lean:5; no owner; claims lean/demo-base-eq-7f17aa41d1461243",
-        "Impacted without a Markdown dependency path to the revised article: chapter/loose",
+        "Impacted without a Markdown dependency path to the revised declarations: chapter/loose",
         "Statement dependents in Markdown that are not statement impacted: chapter/inlines",
         "Deprecated:",
         "  Demo.gone: no users, safe to delete",