[Deicyde]

Step 6 of the revision contract now gives a call that works on a mathlib: true article. It also unsets the article's Mathlib facts, since a revision voids the Mathlib claim as it voids the statement.

Premise

• User: Roadmap, when it records a revision of an article that restates a Mathlib declaration.
• Problem: step 6 retracts a revised article with autoform links set blueprint <ARTICLE_PATH> statement=retracted --unset proof (autoform_cli/reference/claims-and-revisions.md:149-156 on main). On a mathlib: true article, links set refuses that call with roadmap/result.md: with statement=retracted --unset proof, a mathlib: true article cannot record statement: retracted. The loader rejects statement: retracted beside mathlib: true (autoform_cli/graph.py:1415-1416), and the annotation reader leaves such a status out (autoform_cli/annotations.py:465-466). I probed main on a frontmatter vault and on one migrated with migrate links --write. Both refuse the documented call, and both accept it with --unset mathlib --unset mathlib_declaration --unset mathlib_file added. So the contract named a call the code refuses, and the refusal didn't say what to do instead.
• Replaces: step 6's one call, with two forms. With lean:, it is statement=retracted --unset proof plus the three unsets. Without lean:, it is the three unsets alone, since statement: retracted needs a lean: to keep.
• Deletes: nothing in code. The loader refuses the same facts with the same exit status; only the message text changes.

What changes

• claims-and-revisions.md, step 6: both forms. mathlib: true and its names are a verified claim about the old statement, so a revision voids them, as it voids statement: formalized.
• graph.py:1416, the load error that links set also reports: "... cannot record statement: retracted; to retract it, also omit mathlib, mathlib_declaration and mathlib_file".
• annotations.py:466, the warning: "status retracted is left out beside org.autoform mathlib true; to retract, also unset mathlib, mathlib_declaration and mathlib_file".
• Tests: the four tests that pin those texts (test_graph, test_contract, test_links_set and test_annotations) are updated. Two new links set tests each run on a frontmatter vault and on a migrated one:
  • test_a_revised_mathlib_article_is_retracted_without_its_mathlib_facts (with lean:): the documented call exits 0. The article reads back statement: retracted with lean kept, no Mathlib facts, and the state can_state. It kills reader-drops-every-retraction (annotations.py:465 leaves out every retracted status, not only one beside mathlib true) and retracted-counts-as-stated (status.py:240 counts a retracted statement as stated).
  • test_a_revised_mathlib_article_without_lean_loses_only_its_mathlib_facts (without lean:): the three unsets exit 0 and leave the article unstated, with no Mathlib facts. It kills unset-keeps-mathlib-flag (Edits.apply in links_set.py keeps mathlib through --unset mathlib).
  • Mutant run, 3 of 3 killed, with the baseline passing (4 passed): https://github.com/facebookresearch/autoform-bot/actions/runs/43428608743
• CHANGELOG: one Unreleased Fixed line, since step 6 as documented is refused today.

Checks

• Docs net zero (K5): claims-and-revisions.md stays at 161 lines.
  • Step 6 grows by one line. It drops "edits only the blueprint" and "leaves the Lean side to Formalize", which the section's opening already says: "Roadmap records a requested revision in the blueprint (step 6); Formalize carries out the Lean side (steps 1 to 5)."
  • Step 3 drops "(or, without claims, have the lead confirm it)", which repeats its earlier "Without claims, a Formalize subagent has its lead confirm the set instead." A pure rewrap of step 3 saves nothing, so that line is a real cut.
• No new refusal in the loader: the same facts are refused, with the same exit status.
• ruff check with the locked ruff 0.15.17 passes on the changed files, and this PR's CI runs the suite.
• File overlap: Claims: remove renew, cleanup and --ttl #795 edits claims-and-revisions.md:65 and Migrate: remove article-ids #796 edits test_annotations.py:738-762, both separate hunks.

Posted by Claude Code, at Jack's request.

[Deicyde]

No blockers. Step 6 states both forms and the file stays at 161 lines, none over 80 columns; the step 3 cut loses nothing, since Formalize's SKILL.md already has the lead confirm grown claim targets. graph.py and annotations.py change only their text, under the same conditions, so the same facts are refused with the same exit status. The two new tests kill their named mutants (baseline 4 passed, 3 of 3 killed: https://github.com/facebookresearch/autoform-bot/actions/runs/43428608743); Edits.apply treats --unset of an absent key as a no-op, so the call also works on an article missing one of the three keys; and the CHANGELOG has one Fixed entry. CI is green at eda83e9.

Posted by Claude Code, at Jack's request.