[Deicyde]

Summary

• keep mathematical articles to frontmatter and informal mathematics
• store versioned implementation handoffs in one hidden file per article: blueprint/.implementation-notes/<article_id>.md
• key notes by durable article_id, so article moves preserve them and independent article claims never share a note file
• make autoform check reject noncanonical, malformed, empty, symlinked, unreadable, or orphaned notes, ignore hidden entries such as editor lock files, and say how to repair an orphan
• make autoform audit report a note left after its article is proved, or after every formalizable descendant of a container is proved
• leave ordinary agents.md and standard AGENTS.md untouched as normal content/instructions
• teach Roadmap and Formalize to use the per-article note and keep transcripts, secrets, and machine-local paths out; Formalize deletes every note the audit reports as stale, including a container's note its proof completes; Agent Review reads the notes and expects Mathlib candidates there, never in articles

Why this design

Implementation details should not clutter the mathematical wiki, but a shared agents.md created a reserved-name collision, cross-worker merge hotspot, filename-based stale state, and a hard migration for older pinned projects.

The hidden per-article directory avoids those problems. Existing and older graph loaders scan only blueprint/roadmap/, while existing renderers and structure views already omit hidden path components. No renderer exception or pin migration is required.

Contract

• filenames are existing durable article IDs plus .md
• one regular, nonempty UTF-8 Markdown file belongs to one article claim
• roadmap path moves do not rename the note
• the file is deleted after leaf proof or completion of a container's formalizable subtree (a container with no formalizable descendant keeps its note); audit reports stale notes
• hidden implementation notes are neither mathematics nor dependency-graph state and never enter publication hashes
• the stale finding names the file to delete (.implementation-notes/<article_id>.md); any worker may delete a stale note, or repair an orphan a merge left behind by restoring a lost article_id or by moving useful content to the surviving article's note and deleting the orphan

Validation

At exact implementation head before the final clean merge from current main:

• full suite: 1,842 passed, 6 skipped, 1 expected failure
• focused graph/audit/render/visualization/skill suites: 229 passed
• container cleanup roll-up regression: 1,200 containment levels without recursion
• make lint and make check-example: passed
• Formalize and Roadmap skill validation: passed
• independent code and architecture re-reviews: approved

After merging current main, the focused tests, lint, diff check, and
example build pass. GitHub CI at b032c03f was green, including both Windows
and real-Lean jobs.

At 3e95335, which has Formalize delete stale notes, states the container rule exactly in the README and Roadmap skill, and passes a statement string to _ArticleShape in the deep-containment test to match main: make lint passes locally, and GitHub CI is green for both the push and the merge with main, including the Python 3.10 and 3.13 test jobs (lint, full suite, example build), Windows, and real-Lean jobs.

At 6c46193, after a deep multi-agent review (graph validation, audit rule, publication, docs, tests with mutation checks, compatibility, product judgment, merge interaction with main, and consumer runs on the bundled example, hartshorne and hatcher-at), four follow-up commits add orphan-note repair guidance, point Agent Review at the notes, add negative container-rollup tests, and tighten edge cases. The affected suites pass on the branch merged with main at 93c5d28 (289 passed), lint is clean, and GitHub CI is green for both the push and the merge with main, including the Python 3.10 and 3.13 test jobs (lint, full suite, example build), Windows, and real-Lean jobs.

At 13a8567d, a merge of main at 76e486d5: four files conflicted (audit.py, the Formalize and Roadmap skills, and tests/test_audit.py imports), each resolved by keeping both sides, with main's migrate article-ids --write wording. migrate article-ids --write refuses while an orphaned note exists, so a lost article_id cannot be replaced by a fresh one. Lint passes and the affected suites pass locally (490 passed), and GitHub CI is green for both the push and the merge with main, including the Python 3.10 and 3.13 test jobs (lint, full suite, example build), Windows, and real-Lean jobs.

[Deicyde]

Superseded by the review of f13757c after the per-article notes redesign: #172 (comment)

Review of #172 at 8e372ad. The graph, render, and hash changes are sound, but coverage still accepts the notes file as article evidence, and the old-pin caveat is wrong for notes files with an H1.

Should fix

• autoform_cli/coverage.py:574 _is_roadmap_article still accepts any existing .md under roadmap/. A DECOMPOSED row whose only evidence is [Notes](../roadmap/agents.md) therefore passes load_coverage (no issues) and autoform check (rc 0). On base the same project fails with agents: missing H1 title. After render_site, the coverage page links to ../roadmap/agents.md, which is never written. Fix: import is_agent_notes from .graph and append and not is_agent_notes(candidate). Add a test_coverage case that expects "DECOMPOSED coverage evidence has no link to an existing roadmap article". With both changes, test_coverage gives 54 passed and ruff is clean.
• autoform_cli/README.md:85 (same wording at skills/formalize/SKILL.md:125 and skills/roadmap/SKILL.md:71): the claim that an older AUTOFORM_REF "reads it as an article and fails" holds only when the file has no H1. On base, agents.md = # top.md\n\nMathlib gap.\n passes check ("OK: 4 articles"), becomes node agents, and render publishes roadmap/agents.md. That is the leak this PR exists to stop, on exactly the pinned projects the caveat targets. Fix: state the format ("one ## <file>.md section per article, no H1") in README:81 and both skills, or reword the caveat to say an old pin either fails or publishes the notes.

Golf

• tests/test_skill_examples.py:72 the "agents.md" entry duplicates the stricter assertions in the new test (line 110). Delete the line without replacing it. test_skill_examples still gives 26 passed.

Nits

• autoform_cli/render.py:333 render skips agents.md, but _rewrite_links still rewrites links to it, so an article that links its notes gets a dead link on the site (roadmap/README.md -> agents.md exists: False). check does not flag it. Drop the link and keep its label when the target is_agent_notes, or say "never linked from an article" in the skills.
• autoform_cli/README.md:1040 says to record revision outcomes "in the agents.md beside each touched article", while skills/formalize/SKILL.md:124 says to delete the section once the article is proved. Repaired in-place dependents and proof-impacted articles stay proved, so their record is lost, including the note that they still rest on deprecated X. Exempt revision records until the migration lands, or put them in the commit or report.
• autoform_cli/README.md:13 the match is name.casefold() == "agents.md", so an article named Agents.md drops out with no error. Write "except agents.md (in any letter case)".
• skills/formalize/SKILL.md:64 the line is 49 columns between 74-column neighbors. Reflow lines 62-66.

Checked, no change needed

• Merged tree: test_graph 58, test_render 78, test_visualization 24, test_skill_examples 26, test_coverage 53, all passed. ruff on the seven changed Python files passes.
• Graph discovery, the orphaned-chapter check, render_site, _published_source_files, and both structure pages all skip agents.md. Editing the notes leaves the publication revision unchanged.
• Parallel workers appending to one agents.md conflict textually. The PR body accepts this tradeoff, and the skill says to keep both sections.
• No Execution notes references remain outside the test that forbids them.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Review of #172 at f13757c (replaces the review of 8e372ad). The per-article hidden-notes design is sound and nothing blocks the merge, but audit reports note errors at wrong paths and the revision contract conflicts with the new audit rule.

The earlier coverage, old-pin, dead-agents.md-link and casefold findings are moot because notes no longer live under roadmap/. The revision-record finding is still present and worse (see Should fix). The duplicate skill assertion and the ragged lines are still present.

Should fix

• autoform_cli/audit.py:549 _validation_article_path treats the .implementation-notes/... prefix as a node ID, so every note error is reported at a nonexistent file. An orphaned note is reported at roadmap/.implementation-notes/af_111111111111111111111111.md.md. A file in place of the directory gives roadmap/.implementation-notes.md, and an alias gives roadmap/.Implementation-Notes.md. This breaks README:808 ("structured findings at blueprint-relative paths"). Fix: after the return "." guard add if node_id.split("/", 1)[0].casefold() == IMPLEMENTATION_NOTES_DIR: return node_id, then add an orphan-note audit test. That test fails on the head and passes with the fix (test_audit 27 passed, ruff clean).
• autoform_cli/README.md:1092 the revision contract says to record the outcome in each touched article's note. Repaired in-place dependents and expand-route proof-impacted articles stay proved, though, and audit.py:176 then reports stale-implementation-note. A proved article with a revision note passes check and fails audit. Workers either fail audit or delete the record that the article still rests on deprecated X. On main that record lived in ## Execution notes and was never forced out. Fix: "Record what happened in the revision commit and report; use an article's implementation note only while that article remains unproved."
• skills/roadmap/SKILL.md:71 Roadmap is told to put prior art in the note but never told to delete it. A note on an article marked mathlib: true fails audit, because status counts that as proved. Deleting or merging an article leaves an orphan, which stops every graph command: on the bundled example with one leftover note, check rc=1, render rc=1 and work list rc=2. README:83 says only that autoform check rejects bad notes. Fix: add "Delete the note when the article is proved or marked mathlib: true, and in the same commit that deletes or merges the article; an orphaned note fails every command that loads the graph." Reword README:83 to "Every command that loads the graph, including autoform check, rejects".
• autoform_cli/audit.py:176 no test covers a note on an unproved article. With and derived[node_id].proved removed, test_audit still gives 25 passed, so audit could reject every in-progress note unnoticed. Fix: add an unproved-theorem-with-note case next to test_audit_rejects_implementation_notes_left_after_proof that asserts no stale-implementation-note.

Golf

These edits, applied together with the audit fix and two new tests, keep the suites passing: test_graph 61 (the drop is the 2 agents.md cases), test_audit 27, test_render 78, test_skill_examples 26, ruff clean.

• autoform_cli/graph.py:407 replace node_id = article_ids.get(path.stem) / if node_id is None: with if path.stem not in article_ids:, and put the four wrapped issues.append calls on one line each (limit is 120). Keep the separate symlink and not-a-directory messages.
• tests/test_graph.py:526 delete test_agents_filenames_remain_ordinary_articles; it guards the abandoned design, and main has no agents.md handling. Fold test_implementation_notes_directory_has_canonical_spelling (593) into the fail-closed parametrize as a directory column. In tests/test_render.py delete 1048-1050 and 1058, and assert == before at 1062.
• tests/test_skill_examples.py:72 duplicates line 107. Line 110 pins rationale prose, and line 120 guards agents.md, which main never had. Delete all three, and drop the rationale sentence at skills/formalize/SKILL.md:124-125, which repeats README:80-83.

Nits

• autoform_cli/graph.py:410 a parse error in the note's own article (for example a missing H1) also reports its valid note as "names no roadmap article", which invites deleting a good handoff. Skip the orphan check when parse issues exist.
• autoform_cli/graph.py:397 the dotfile skip runs before the symlink and naming checks. A misnamed .af_<id>.md and a .secret symlink to $HOME both pass check. Nothing leaks, but the body says symlinks are rejected. Separately, at line 418 a BOM-only or zero-width-only note passes the nonempty check. Reject symlinks before the skip, and strip \ufeff and \u200b before the nonempty check.
• skills/formalize/SKILL.md:119 an article link to ../.implementation-notes/<id>.md passes check and renders as a dead link. Add "and never links its note".
• autoform_cli/graph.py:377 the note tests cover only the misnamed, orphan, empty and alias cases. Add rows for a symlinked note, a symlinked directory, <id>.txt, non-UTF-8 content and a .DS_Store positive case.
• autoform_cli/templates/github/workflows/autoform-verify.yml:39 generated CI runs check and render, never audit, so the body's "audit enforces cleanup" overstates it. README:87 ("reports") is accurate. Fix the body.
• autoform_cli/README.md:13 lines 13-16 reflow unchanged text; revert them. Reflow the ragged new lines: README:85 (49 cols), README:1091 and 1093 (39), formalize SKILL.md:62 (30) and 65 (36), roadmap SKILL.md:94 (85).

Checked, no change needed

• Notes live outside roadmap/, so coverage cannot cite them. Render, the structure pages and publication_source_revision omit the directory. Base 4c80749 check and render ignore it, so no AUTOFORM_REF migration is needed.
• Moves keep notes valid because notes are keyed by article_id. Uppercase IDs, .MD, nested directories, symlinked notes or directories (except hidden ones, see Nits), invalid UTF-8 and whitespace-only content are rejected.
• Failing closed in load_graph matches how other graph errors behave. Only the deletion guidance and the README wording need to change.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Re-checked at c2528c7. All four should-fix items from the review of f13757c5 are fixed, and each fix has a test that fails without it. Nothing blocks the merge.

• Note errors are now reported at the note's own blueprint path (audit.py:560). test_audit_reports_invalid_note_at_its_blueprint_path fails 3 of 3 when that branch is removed.
• The revision contract keeps the record in the revision commit and report, and uses a note only while its article is unproved.
• Roadmap deletes the note on proof, on mathlib: true, and in the commit that deletes or merges the article. The README now says every command that loads the graph rejects bad notes.
• test_audit_allows_implementation_notes_while_work_is_unproved fails when the proved guard at audit.py:186 is dropped.

The nits are closed too:

• an article parse error no longer reports its note as orphaned;
• symlinks are rejected before the dotfile skip;
• BOM-only and zero-width-only notes count as empty;
• both skills say never to link the note;
• the five missing fail-closed cases have tests;
• the body says audit "reports";
• the README reflow at line 13 is reverted, and the ragged lines are reflowed.

Optional golf, still open

• tests/test_graph.py:527, tests/test_render.py:1048-1050 and 1058 (then assert == before at 1062), and tests/test_skill_examples.py:125 guard the abandoned agents.md design; main has no agents.md handling.
• Five note tests in tests/test_graph.py (577, 596, 613, 630 and 652) build the same one-article blueprint in 8 lines each. One _note_blueprint(tmp_path) helper would remove about 25 lines.
• tests/test_skill_examples.py:72 is implied by line 107. Line 110 pins the rationale sentence at skills/formalize/SKILL.md:124-125, which repeats README:80-83.
• autoform_cli/graph.py lines 379, 386, 407, 412 and 422 still wrap issues.append calls that fit on one line.

Validation at c2528c7: test_audit 29, test_graph 69 and test_skill_examples 26 pass locally. Both mutations above were run against those tests. The CI test jobs are green; real Lean was still running at the time of writing.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Supersedes the “not ready” review of f13757c5: #172 (comment)

Final exact-head review at c2528c7a: ready for human review. The follow-up fixes:

• preserve complete blueprint-relative diagnostic paths for malformed note filenames, including spaces and colons;
• keep revision outcomes in the revision commit/report when touched articles remain proved, using implementation notes only for unproved work;
• require Roadmap to delete notes on proof/mathlib: true and atomically with article deletion or merge;
• verify that unproved work may retain a note and that proved work may not;
• avoid false orphan findings while an article itself is malformed;
• reject symlinked directories/files, malformed extensions, invalid UTF-8, BOM/zero-width-only notes, and orphan notes while allowing .DS_Store;
• forbid links from mathematical articles to hidden notes.

Validation at this exact head:

• focused graph/audit/render/visualization/skill suites: 226 passed;
• Ruff, git diff --check, and make check-example: pass;
• Formalize and Roadmap skill validation: pass;
• all exact-head GitHub checks pass, including Windows and both real-Lean jobs;
• independent code and architecture re-reviews: approved with no remaining blockers.

[Deicyde]

Gap in the stale-note audit: stale-implementation-note fires only when status.derive(graph)[node].proved, and proved is per-node (status.py:111: formalized proof, Mathlib, or a stated definition). A chapter or other container article is never proved, so a note keyed to its article_id is never flagged and can stay forever.

In hartshorne and hatcher-at, the 9 Lean-side notes left after cleaning proved articles are all on chapter READMEs, and some are already stale.

Possible fix: flag a container's note once every article it contains is proved.

[Deicyde]

Supersedes the container stale-note gap reported here: #172 (comment)

Fixed at exact head b032c03f. Container notes are now stale when the container has at least one formalizable descendant and every such descendant is derived proved; a container with any unfinished formalizable descendant may retain its note.

The roll-up is computed once, bottom-up and iteratively. A 1,200-level containment regression verifies that the audit does not recurse or rescan each subtree.

Validation at this exact head:

• focused graph/audit/render/visualization/skill suites: 229 passed;
• dedicated audit/skill suite: 58 passed;
• Ruff, git diff --check, and make check-example: pass;
• all exact-head GitHub checks pass, including Windows and both real-Lean jobs;
• independent code and architecture reviews: approved with no remaining blockers.

#172 is ready for human review.

[Deicyde]

Correction to my earlier comment: its suggested fix ("every article it contains is proved") misses 5 of the 9 book notes, because sub-container READMEs and other non-formalizable pages don't derive proved. The subtree rule in b032c03f is the right one: with the 9 chapter- and section-level notes in hartshorne and hatcher-at converted to .implementation-notes/ files, b032c03f flags all 9; c2528c7a flagged none.

Two gaps remain at b032c03f:

1. Nothing tells Formalize to delete a container's note. The PR that proves a container's last formalizable descendant creates stale-implementation-note on the container, but the skill keeps the worker to the claimed article (formalize/SKILL.md:64-65, :118-126) and its findings (:133-137); only Roadmap has the container rule (roadmap/SKILL.md:76-77). autoform doctor fails on the finding, so in a book whose CI runs doctor (hartshorne's does), that PR fails unless the worker leaves the skill's scope. If two PRs finish a container in parallel, the finding first appears on main, where Formalize only reports it. Suggest: Formalize deletes any container note the audit reports as stale.
2. README.md:1093-1094 still limits a note to "while that article remains unproved", which never ends for a container, and :85-86 drops the code's "at least one formalizable descendant" condition.

[Deicyde]

Pre-merge review of 6c46193, the head after my previous reply.

Review. A multi-agent review covered note validation (about 30 edge-case fixtures), the stale-note rule (15 blueprints, a 2,121-article graph, mutated rollups), publication (notes never reach the site, views, search, or publication hash, including under the 1cf2ca8 renderer), docs and skills against the code, test strength (27 mutations), CLI and JSON compatibility, product judgment, and the merge with main. On the bundled example, and on hartshorne and hatcher-at with notes added, output differed from main only by the intended stale-note finding. Two independent verifiers checked every substantive finding.

Fixed:

1. d48e2f5: the Agent Review rubric asked for explicit Mathlib candidates without pointing at the hidden notes, so a reviewer would ask for Lean text back in articles. It now reads each node's note and expects Mathlib candidates there, never in the article. New negative tests catch a rollup that ignores an unproved nested article or lets one sibling overwrite another; both mutations passed the whole suite before.
2. 3ab3f3d, 6c46193: one branch deleting or merging an article while another writes its note orphans the note without a Git conflict, and every graph-loading command then refuses. The error now says how to repair it, and Formalize, Roadmap and the README describe the repair: restore a lost article_id, or move anything useful to the surviving article's note and delete the orphan. Any worker may do this.
3. 76ff8fc: errors under a misplaced roadmap/.implementation-notes/ point at the real path again, as on main; hidden entries such as Emacs lock symlinks no longer block every command; the stale finding names .implementation-notes/<article_id>.md; Formalize commits stale-note deletions after rebasing; the README's claims sentence and Roadmap's no-transcript/secret rule now match the code and this PR's description.

Left as is: a traceback when the notes directory is not searchable (main crashes the same way for roadmap directories), a KeyError from audit_graph on hand-built graphs with default depths (no command reaches it), and rejection of editor backup files in the notes directory (fail-closed naming). Open design question: only a worker's own leaf note is ever read, so container notes are cleaned up but not read, and notes on exposition pages are never flagged.

Validation: the affected suites pass on this head merged with main at 93c5d28 (289 passed), lint is clean, and GitHub CI is green for both the push and the merge with main, including the Python 3.10 and 3.13 test jobs (lint, full suite, example build), Windows, and real-Lean jobs.

[Deicyde]

Review at 13a8567

Verdict: merge-ready. This head merges main at 76e486d5 into the reviewed 6c46193 (results above). CI is green for both the push and the merge with main, including real Lean, and the PR has no conflicts.

• Merge. Four files conflicted, and each resolution keeps both sides: audit.py runs the stale-note check and then main's unclosed-fence check, and the Formalize and Roadmap skills take main's migrate article-ids --write wording alongside the notes rules. The six files Git merged on its own match its automatic merge byte for byte. Against main, the PR's changes are the same as before the merge, apart from one rewrapped paragraph and the merged import line in test_audit.py.
• Interactions with main. I reproduced each one. The roadmap symlink refusal returns before note validation, so it never reports a false orphan. migrate article-ids --write and autoform search refuse while a note is orphaned, so a lost article_id cannot be replaced by a fresh one before it is restored. One article can carry both stale-implementation-note and unclosed-code-fence.
• Earlier fixes. All of them survived the merge: hidden entries are skipped before the symlink check, misplaced-notes errors point at their real path, the stale finding names .implementation-notes/<article_id>.md, the orphan error carries the repair hint, the Agent Review rubric points at the notes, and the negative rollup tests pass.
• Tests. 490 passed locally across the audit, graph, skill-example, article-identity, render, visualization, markdown, search and scope-completion suites. Lint is clean. The only local failures are project-inspection FIFO probes timing out under load, and they fail on main alone too.

Follow-ups, none blocking:

1. When Roadmap moves a note into a new page that has no article_id yet, deleting the old article first orphans the note, and migrate article-ids then refuses too. One sentence in the Roadmap skill would avoid it: give the surviving page its ID before deleting the old one.
2. Only a worker's own leaf note is ever read, so container notes are cleaned up but not read, and notes on exposition pages are never flagged.
3. Since Show finished scopes as complete, and draw containers as scopes #196 the site keeps a scope open while it has not_ready leaves, but the container-note rule counts only formalizable descendants, so a container's note can be flagged stale while the site still shows that scope open.