From 8940cc8f64b919e3b97b612b0a27b85c4c106d98 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 5 Oct 2026 15:29:26 -0400
Subject: [PATCH 1/4] Claim a revised declaration no article names like an
 unowned helper

`work impact R --declaration X` skipped X when listing helpers, so when no
article named X its claim set held only R's target. Two revisions of the same
unowned helper from different articles then each claimed only their own
article and could both edit X. A revised declaration no article names is now
claimed under every owner's target, or under the `lean/<slug>-<digest>` key an
unowned helper gets, and `contained` holds exactly when the revised article's
target is the only one, so such a revision is never reported as safe to make
in place under R's claim alone.

Restored from closed #115 (cc36d27), which the split omitted, and adapted to
plural helper owners.
---
 autoform_cli/README.md |  7 +++++--
 autoform_cli/impact.py | 18 ++++++++++-------
 tests/test_impact.py   | 44 ++++++++++++++++++++++++++++++++++++++++--
 3 files changed, 58 insertions(+), 11 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index bd842fa1..513d4504 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -534,8 +534,11 @@ statement-impacted and proof-impacted articles, unnamed helpers, missing
 Markdown dependency paths, deprecated declarations and their users, whether
 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. Project locality is an exact inventory of
-regular repository source modules, never a namespace-prefix guess.
+stable `lean/<slug>-<digest>` target. A `--declaration` no article names is
+claimed the same way, under every owner's target or its own key, so a revision
+is contained only when the revised 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 both the roadmap and repository Lean sources
 around the probe. JSON uses `autoform-impact/v1` and binds its answer to the
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index ed7f9fed..d0153947 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -444,14 +444,13 @@ 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.
+        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.
         """
 
-        return not (
-            self.statement_impacted
-            or self.proof_impacted
-            or any(set(helper.owners) != {self.article.id} for helper in self.helpers)
-        )
+        return self.claim_targets == (self.article.claim_target,)
 
     def as_dict(self) -> dict[str, object]:
         return {
@@ -594,10 +593,15 @@ def compute_impact(
     )
 
     # A helper is repaired under every owning article's claim; an unowned
-    # helper contributes the key derived from its own name.
+    # 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
     }
+    for name in revised_names:
+        if name not in named:
+            owners = _owners(records[name], records, named)
+            others |= {by_id[owner].claim_target for owner in owners if owner in by_id} or {_helper_claim_key(name)}
     claim_targets = (revised.claim_target, *sorted(others - {revised.claim_target}))
     return ImpactReport(
         source_revision=source_revision,
diff --git a/tests/test_impact.py b/tests/test_impact.py
index 4e03e054..def930ad 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -553,6 +553,45 @@ def test_revisions_touching_one_unowned_helper_contend_for_its_claim() -> None:
     assert json.loads(right.to_json())["helpers"][0]["claim_targets"] == [key]
 
 
+def test_a_revised_declaration_no_article_names_is_claimed_like_a_helper() -> None:
+    records = _records(
+        _rec("A.R", "def"),
+        _rec("A.R.aux", "def", parent="A.R"),
+        _rec("A.S", "def"),
+        _rec("A.T", "inductive"),
+        _rec("A.T.aux", "def", parent="A.T"),
+        _rec("A.U", "def"),
+        _rec("A.U.aux", "def", parent="A.U"),
+        _rec("A.loose", "def"),
+    )
+    articles = [
+        _article("r", "A.R"),
+        _article("s", "A.S"),
+        _article("t", "A.T"),
+        _article("u-b", "A.U"),
+        _article("u-a", "A.U"),
+    ]
+
+    from_r = _impact(records, articles, "r", ["A.loose"])
+    from_s = _impact(records, articles, "s", ["A.loose"])
+    owned = _impact(records, articles, "r", ["A.T.aux"])
+    shared = _impact(records, articles, "r", ["A.U.aux"])
+    own = _impact(records, articles, "r", ["A.R.aux"])
+
+    # Nothing uses A.loose, yet two revisions of it contend for the claim
+    # keyed by its name; a revised declaration other articles own is claimed
+    # under every one of them, and one the revised article owns adds no claim.
+    assert from_r.claim_targets == ("r", _lean_key("A.loose"))
+    assert from_s.claim_targets == ("s", _lean_key("A.loose"))
+    assert not from_r.contained
+    assert owned.claim_targets == ("r", "t")
+    assert not owned.contained
+    assert shared.claim_targets == ("r", "u-a", "u-b")
+    assert not shared.contained
+    assert own.claim_targets == ("r",)
+    assert own.contained
+
+
 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))
@@ -1017,8 +1056,9 @@ def test_cli_declaration_flag_replaces_the_article_s_names(tmp_path: Path, monke
     report = json.loads(output.out)
     assert report["article"] == {"id": "chapter/empty", "article_id": None, "claim_target": "chapter/empty"}
     assert report["declarations"] == ["Demo.gone"]
-    assert report["contained"] is True
-    assert report["claim_targets"] == ["chapter/empty"]
+    # No article names Demo.gone, so revising it claims its own key too.
+    assert report["contained"] is False
+    assert report["claim_targets"] == ["chapter/empty", _lean_key("Demo.gone")]
 
 
 def test_cli_text_escapes_terminal_control_characters(tmp_path: Path, monkeypatch, capsys) -> None:

From fff95bdfb97e8ab32a0fe28c0c7e40a549822b16 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 2/4] 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 |  9 ++++-
 autoform_cli/impact.py | 51 +++++++++++++++++++-----
 tests/test_impact.py   | 90 +++++++++++++++++++++++++++++++++++++++---
 3 files changed, 134 insertions(+), 16 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index 513d4504..7060dfa0 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -537,8 +537,13 @@ by several articles contribute every owner's claim; an unowned helper gets a
 stable `lean/<slug>-<digest>` target. A `--declaration` no article names is
 claimed the same way, under every owner's target or its own key, so a revision
 is contained only when the revised article's target is its only claim target.
-Project locality is an exact inventory of regular repository source modules,
-never a namespace-prefix guess.
+`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`, so they too rule out
+`contained`. Project locality is an exact inventory of regular repository
+source modules, never a namespace-prefix guess.
 
 The command snapshots and rereads both the roadmap and repository Lean sources
 around the probe. JSON uses `autoform-impact/v1` and binds its answer to the
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index d0153947..9c9483eb 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -345,6 +345,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:
@@ -434,6 +436,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, ...]
@@ -445,9 +451,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,)
@@ -469,6 +476,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),
@@ -576,6 +584,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():
@@ -595,9 +615,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:
             owners = _owners(records[name], records, named)
@@ -613,6 +635,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,
@@ -711,14 +734,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:
@@ -785,6 +811,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
     }
@@ -888,6 +916,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 def930ad..9af03fa8 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -53,9 +53,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):
@@ -290,6 +295,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"),
@@ -885,7 +948,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"])
@@ -905,6 +968,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
 
@@ -925,6 +994,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),
 ]
@@ -985,12 +1055,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"
@@ -1022,10 +1099,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
 
@@ -1452,6 +1530,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 0f5d7875e8ad47f7946a5a69e92b8e4e0ec9c35c 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 3/4] 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 |  6 ++++--
 autoform_cli/impact.py | 20 +++++++++++++-------
 tests/test_impact.py   | 25 ++++++++++++++++++++++++-
 3 files changed, 41 insertions(+), 10 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index 7060dfa0..9a4cec78 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -542,8 +542,10 @@ 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`, so they too rule out
-`contained`. Project locality is an exact inventory of regular repository
-source modules, never a namespace-prefix guess.
+`contained`. 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`. Project locality is an exact inventory of regular
+repository source modules, never a namespace-prefix guess.
 
 The command snapshots and rereads both the roadmap and repository Lean sources
 around the probe. JSON uses `autoform-impact/v1` and binds its answer to the
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index 9c9483eb..f1007c78 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -347,6 +347,7 @@ class ImpactArticle:
     dependencies: tuple[str, ...] = ()
     statement_dependencies: tuple[str, ...] = ()
     stated: bool = False
+    mathlib: bool = False
 
     @property
     def claim_target(self) -> str:
@@ -436,9 +437,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, ...]
@@ -452,9 +454,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,)
@@ -586,12 +588,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)
@@ -813,6 +818,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 9af03fa8..a6943de2 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -59,8 +59,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):
@@ -317,6 +318,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")
@@ -1013,6 +1016,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 70fe798efad8dc37f2da6ad06e9611bf6438265a 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 4/4] 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 | 19 ++++++++++--------
 autoform_cli/impact.py | 32 ++++++++++++++++++++----------
 tests/test_impact.py   | 45 +++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 77 insertions(+), 19 deletions(-)

diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index 9a4cec78..ae6a8fc4 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -538,14 +538,17 @@ stable `lean/<slug>-<digest>` target. A `--declaration` no article names is
 claimed the same way, under every owner's target or its own key, so a revision
 is contained only when the revised article's target is its only claim target.
 `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`, so they too rule out
-`contained`. 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`. Project locality is an exact inventory of regular
-repository source modules, never a namespace-prefix guess.
+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`, so they
+too rule out `contained`. 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 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 both the roadmap and repository Lean sources
 around the probe. JSON uses `autoform-impact/v1` and binds its answer to the
diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
index f1007c78..ab81196c 100644
--- a/autoform_cli/impact.py
+++ b/autoform_cli/impact.py
@@ -15,7 +15,7 @@
 import json
 import os
 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
 
@@ -436,9 +436,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, ...]
@@ -455,8 +458,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,)
@@ -584,8 +588,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
@@ -599,7 +611,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]] = {}
@@ -740,9 +752,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]
@@ -750,7 +762,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)
@@ -919,7 +931,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 a6943de2..475e051d 100644
--- a/tests/test_impact.py
+++ b/tests/test_impact.py
@@ -658,6 +658,49 @@ def test_a_revised_declaration_no_article_names_is_claimed_like_a_helper() -> No
     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))
@@ -1121,7 +1164,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",