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

autoform_cli/README.md

@@ -83,9 +83,9 @@ An article asserts only facts a human or agent verified:
 
 | Key | Meaning |
 | --- | --- |
-| `statement: formalized` | The Lean statement exists and compiles. |
+| `statement: formalized` | The Lean statement exists and compiles. Requires `lean:`. |
 | `statement: retracted` | A revision retracted the statement while `lean:` still names the old declaration, which stays in the build until Formalize restates the article and records `statement: formalized` in its place. Requires `lean:`; invalid with `proof: formalized` or `mathlib: true`. CI's `autoform check` at an older `AUTOFORM_REF` rejects the marker, so move the pin first; until then, retract by removing `statement` and `proof` and keeping `lean:`. |
-| `proof: formalized` | The Lean proof compiles. Under the open policy it may rest on open statements, and the article is then conditional; only the derived `fully_proved` means complete and `sorry`-free. |
+| `proof: formalized` | The Lean proof compiles. Requires `statement: formalized` and `lean:`. Under the open policy it may rest on open statements, and the article is then conditional; only the derived `fully_proved` means complete and `sorry`-free. |
 | `mathlib: true` | The result is upstreamed into Mathlib. |
 | `not_ready: true` | Needs more blueprint work before it can be attempted. |
 | `lean: Ns.decl` | Declaration name(s) that discharge the article. |
@@ -533,12 +533,11 @@ target. The article revision hashes that article's bytes alone. A Lean target's
 local scan does not find the declaration. The scan skips build output and nested
 checkouts, meaning any subdirectory with a `.git` entry, such as a worker's
 worktree or a submodule. Blockers are unmet dependency IDs or one of
-`roadmap:not-a-formalizable-leaf`, `roadmap:proof-without-statement`,
-`roadmap:missing-article-id`, `roadmap:missing-article-revision`, and
-`roadmap:not-ready`. The claim target prefers durable `article_id` metadata.
-`work list` fails explicitly if an unfinished formalizable leaf lacks one; plan
-the missing IDs with `autoform migrate article-ids` and add them to the
-frontmatter. `work context` may still select that article by its path ID to
+`roadmap:not-a-formalizable-leaf`, `roadmap:missing-article-id`,
+`roadmap:missing-article-revision`, and `roadmap:not-ready`. The claim target
+prefers durable `article_id` metadata. `work list` fails explicitly if an
+unfinished formalizable leaf lacks one; plan the missing IDs with `autoform
+migrate article-ids` and add them to the frontmatter. `work context` may still select that article by its path ID to
 report the migration blocker. An item whose article records `statement:
 retracted` is a revision: it carries `revision` true in JSON, and the text of
 `work list` adds a `revision:` line and `work context` a `Revision:` line saying
@@ -605,22 +604,29 @@ SECONDS` sets the probe's budget, 600 seconds by default. The report lists:
 - helpers that no article names, each with an owner when one exists: the
   article naming its nearest ancestor by name, such as `Foo` for `Foo.aux`;
 - impacted articles without a Markdown dependency path to the revised article;
+- in `unused_statement_dependencies`, the stated articles whose Markdown
+  statement rests on the revised article, directly or through other statement
+  dependencies, but which are not statement-impacted: a dependent whose Lean
+  inlines a revised definition's body instead of naming it shows no use, yet
+  its statement changes meaning with the revision;
 - every deprecated project declaration with its replacement, its users, not
   counting companions Lean generates for it such as `X.eq_1`, and the other
   articles whose `lean:` names it, and in `deprecated_unused` those with no
   users and no such article;
 - the claim targets: the revised article's first, then every impacted
-  article's, every helper owner's, and, for a helper without an owner, a
-  `lean/<slug>-<digest>` key derived from its name, so two revisions touching
-  the same helper contend for the same claim; each helper reports its key as
-  `claim_target`. A revised declaration that no article names is claimed the
-  same way, under its owner's target or its own key.
-
-A revision is `contained` when no other article uses it and every helper it
-impacts or revises belongs to the revised article, so its only claim target is
-that article's; it can then be made in place under
-that article's claim. A declaration derived from a revised one without naming
-it in its statement changes with it, but `work impact` does not report that
+  article's, every unused statement dependency's, every helper owner's, and,
+  for a helper without an owner, a `lean/<slug>-<digest>` key derived from its
+  name, so two revisions touching the same helper contend for the same claim;
+  each helper reports its key as `claim_target`. A revised declaration that no
+  article names is claimed the same way, under its owner's target or its own
+  key.
+
+A revision is `contained` when no other article uses it, it has no unused
+statement dependency, and every helper it impacts or revises belongs to the
+revised article, so its only claim target is that article's; it can then be
+made in place under that article's claim. A declaration derived from a
+revised one without naming it in its statement changes with it, but `work
+impact` does not report that
 declaration's users: the additive form `to_additive` writes, which goes
 unreported itself, or a direction `alias ⟨mp, mpr⟩ :=` takes of an `Iff`, which
 shows only as proof-impacted. Check such derivations on the revised set by
@@ -702,8 +708,10 @@ example](../skills/setup/assets/cabannes-thesis-project/mkdocs.yml).
 
 `autoform check` rejects cycles, missing targets, escaping paths,
 self-dependencies, cycles introduced at any rolled-up containment level,
-missing or multiple H1 titles, unsupported frontmatter keys, and assertion
-values it does not recognize. With `--lean-root` it also fails on a `lean:` name
+missing or multiple H1 titles, unsupported frontmatter keys, assertion values
+it does not recognize, and assertions the Lean cannot back: `proof: formalized`
+without `statement: formalized`, or either without a `lean:` name, even beside
+`mathlib: true`. With `--lean-root` it also fails on a `lean:` name
 absent from the sources, as `leanblueprint checkdecls` does for LaTeX
 blueprints. It validates structure and leaves mathematical correctness to the
 agent and the Lean kernel.
@@ -715,8 +723,8 @@ that may be regenerated at any time.
 
 `autoform audit` reports structured findings at blueprint-relative paths. It
 checks that formalizable articles are declaration-sized leaves with statement
-text and an explicit dependency section, that asserted proof and Mathlib facts
-are internally consistent, and that cited work resolves to local source
+text and an explicit dependency section, that asserted Mathlib facts are
+internally consistent, and that cited work resolves to local source
 material without escaping the blueprint. Coverage files are checked for broken
 links and explicitly declared gaps. With `--lean-root`, local declaration names
 and declaration kinds are checked against the Lean source index.
@@ -931,7 +939,8 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5).
      deprecated, `sorry`'d X, show "conditional, assumes R" although R's text
      now describes X', and keep X out of `deprecated_unused`, so R could never
      record its proof. The claim set is every article whose frontmatter or
-     Lean changes: R, the statement-impacted articles, and, in that case, the
+     Lean changes: R, the statement-impacted articles, the unused statement
+     dependencies, and, in that case, the
      proof-impacted ones.
    - **In place**, only when X and X' cannot coexist, for example an instance
      or a structure change: the claim set is every `claim_targets` entry.
@@ -951,6 +960,12 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5).
      uses it. When neither applies, the
      revision is blocked: release the claims and report it. Record what
      happened under `## Execution notes` of each touched article.
+
+   An unused statement dependency, which rules out the contained route, is
+   re-reviewed under X's new meaning like a statement-impacted article: it
+   keeps `statement` only after an Agent Review of its source faithfulness;
+   otherwise it records `statement: retracted`, loses `proof`, and keeps
+   `lean:`.
 3. Claim the route's claim set with one `autoform claim acquire`. When it is
    refused, release everything and report the held claim as the blocker. After
    acquiring, re-run `work impact`; if the set grew, release and start over

autoform_cli/audit.py

@@ -203,15 +203,6 @@ def audit_graph(
                 )
             )
 
-        if node.proof_formalized and not node.statement_formalized:
-            findings.append(
-                AuditFinding(
-                    article_path,
-                    "proof-without-statement",
-                    "proof is marked formalized but the statement is not marked formalized",
-                )
-            )
-
         if node.mathlib and not declaration_names(node.mathlib_declaration or ""):
             findings.append(
                 AuditFinding(
@@ -387,16 +378,6 @@ def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]:
         node = graph.nodes[node_id]
         article_path = _relative_path(node.path, graph.blueprint_dir)
         names = declaration_names(node.lean or "")
-        if (node.statement_formalized or node.proof_formalized) and not names:
-            findings.append(
-                AuditFinding(
-                    article_path,
-                    "missing-lean-target",
-                    "formalized local work has no lean declaration target",
-                )
-            )
-            continue
-
         resolved = []
         for name in names:
             declaration = index.find(name)

autoform_cli/doctor.py

@@ -31,7 +31,6 @@
         "lean-target-deprecated",
         "lean-target-kind-mismatch",
         "lean-target-not-found",
-        "missing-lean-target",
     }
 )
 _CHECK_NAMES = ("blueprint", "runtime", "graph", "references", "audit", "lean targets")

autoform_cli/graph.py

@@ -15,6 +15,8 @@
 from pathlib import Path
 from urllib.parse import unquote, urlsplit
 
+from .lean import declaration_names
+
 
 _HEADING = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.+?)[ \t]*#*[ \t]*$")
 _FENCE = re.compile(r"^ {0,3}(`{3,}|~{3,})")
@@ -488,6 +490,14 @@ def _parse_frontmatter(node_id: str, lines: list[str]) -> tuple[dict[str, str],
             issues.append(f"{node_id}: proof: formalized needs statement: formalized, not retracted")
         if metadata.get("mathlib") in _TRUE:
             issues.append(f"{node_id}: a mathlib: true article cannot record statement: retracted")
+    # Load errors rather than audit findings: the generated workflows never run
+    # the audit, so either state would otherwise publish as proved with no Lean
+    # statement behind it. `mathlib: true` exempts neither.
+    if metadata.get("proof") == _FORMALIZED and metadata.get("statement") not in {_FORMALIZED, _RETRACTED}:
+        issues.append(f"{node_id}: proof: formalized needs statement: formalized")
+    formalized = [key for key in ("statement", "proof") if metadata.get(key) == _FORMALIZED]
+    if formalized and not declaration_names(metadata.get("lean", "")):
+        issues.append(f"{node_id}: {formalized[0]}: formalized needs the lean: declaration that formalizes it")
     return metadata, end + 1, issues
 
 

autoform_cli/impact.py

@@ -301,6 +301,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:
@@ -388,6 +390,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, ...]
@@ -399,9 +405,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,)
@@ -421,6 +428,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),
@@ -523,6 +531,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():
@@ -542,7 +562,11 @@ def compute_impact(
     # A helper is repaired under its owner's claim, so the owner is claimed
     # too; an unowned helper is repaired under a claim keyed by its own name.
     # A revised declaration no article names is claimed the same way.
-    others = {item.claim_target for item in impacted} | {helper.claim_target for helper in helpers}
+    others = (
+        {item.claim_target for item in impacted}
+        | {by_id[article_id].claim_target for article_id in unused}
+        | {helper.claim_target for helper in helpers}
+    )
     for name in revised_names:
         if name not in named:
             owner = _owner(records[name], records, named)
@@ -556,6 +580,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,
@@ -642,14 +667,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:
@@ -716,6 +744,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
     }
@@ -798,6 +828,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:

autoform_cli/work.py

@@ -105,7 +105,7 @@ def _blockers(node: RuntimeNode) -> tuple[str, ...]:
     if not node.dispatchable:
         return ("roadmap:not-a-formalizable-leaf",)
     if node.status.proved:
-        return () if node.status.stated else ("roadmap:proof-without-statement",)
+        return ()
     metadata_blockers: list[str] = []
     if node.article_id is None:
         metadata_blockers.append("roadmap:missing-article-id")

tests/test_audit.py

@@ -109,7 +109,7 @@ def test_clean_audit_has_stable_machine_readable_representation(tmp_path: Path)
     assert str(tmp_path) not in first.to_json()
 
 
-def test_audit_reports_formalizable_structure_and_inconsistent_checked_facts(tmp_path: Path) -> None:
+def test_audit_reports_formalizable_structure(tmp_path: Path) -> None:
     blueprint = tmp_path / "blueprint"
     _coverage(blueprint)
     _article(
@@ -118,7 +118,6 @@ def test_audit_reports_formalizable_structure_and_inconsistent_checked_facts(tmp
         prose="",
         depends=False,
         declaration="theorem",
-        proof="formalized",
     )
     _article(blueprint, "chapter/child.md", declaration="lemma")
 
@@ -129,7 +128,6 @@ def test_audit_reports_formalizable_structure_and_inconsistent_checked_facts(tmp
         "formalizable-container",
         "missing-depends-section",
         "missing-statement-text",
-        "proof-without-statement",
     }
     assert all(reason for _code, reason in findings)
 
@@ -222,12 +220,6 @@ def test_audit_validates_lean_targets_only_when_root_is_supplied(tmp_path: Path)
         statement="formalized",
         lean="Project.missing",
     )
-    _article(
-        blueprint,
-        "untargeted.md",
-        declaration="lemma",
-        statement="formalized",
-    )
     _article(
         blueprint,
         "wrong-kind.md",
@@ -246,9 +238,6 @@ def test_audit_validates_lean_targets_only_when_root_is_supplied(tmp_path: Path)
     assert with_lean["roadmap/missing.md"] == [
         ("lean-target-not-found", "Lean declaration target was not found: Project.missing")
     ]
-    assert with_lean["roadmap/untargeted.md"] == [
-        ("missing-lean-target", "formalized local work has no lean declaration target")
-    ]
     assert with_lean["roadmap/wrong-kind.md"] == [
         ("lean-target-kind-mismatch", "Lean target kind def does not match declaration intent theorem")
     ]