Blueprint search and reuse: phase 1 items 1-3 and 5 (#143)

[zibo-yang]

Part of #143: phase 1 items 1, 2, 3 (without --skeleton) and 5. Six commits, reviewable one at a time; each builds on the one before. What phase 1 still needs after this PR is under "Not in this PR".

The branch was rewritten after each of the two reviews: the fixes are folded into the commits they belong to, and the former fifth commit (--skeleton) is removed. The fix from the third review is commit 5 and the fix from the final review is commit 6, both added on top without rewriting the branch.

Commit 1: one definition of an article's statement

audit._read_article and render._split_body each decided where a statement ends, and disagreed: the audit stopped at the first H2, the site at the first heading of any level. An article with an H3 before its first H2 had statement text for the audit and a truncated theorem box on the site.

markdown.article_parts(text) now returns the statement and the H2 sections, and both callers use it. The statement is the body from the end of the frontmatter to the first ## heading, without the H1 line. A ## inside a fenced block or an HTML comment does not end it.

Case	Audit	Site
H3 before the first H2	unchanged	the statement box now runs to the first H2, with the H3 demoted, instead of stopping at the H3
Prose above the H1	now counts as statement text	unchanged
Indented code only	no longer counts as statement text	a statement whose first line is indented code was published as a paragraph and is now published as a code block
## inside an HTML comment	unchanged	no longer cuts the statement

The notes below the statement are rebuilt with a blank line between sections, so the page HTML changes where a ## line had no blank line above it.

The graph loader reads fences and comments through the same helper. It used to remove comments before it recognised fences, so a <!-- shown inside a code block hid every section after it: the article's dependency edges were dropped, and with the audit moved to article_parts nothing reported it. Two rules follow the page:

• A fence closes only on a bare fence line. main also closed it on a fence line with trailing text.
• A fence that never closes hides nothing for the graph and the statement, because the site draws it as plain text with the headings and links after it in view. That holds on a page with one article; on a chapter page the opener can pair with a later article's closing fence, and no tool reports it (Audit should report a code fence that never closes #199). So a ```lean ... ``` -- end block above ## Depends on loses no edge.
• This can change what loads. On an article with a fence that never closes, or a fence line with trailing text, autoform check can newly fail (a # line in what is now plain text is a second H1: multiple H1 titles) and the graph can gain or lose an edge. For example, under ## Depends on, the lines ``` -- end, ```lean, - [a](a.md) and a bare ``` gave the edge to a on main and give none here: the page draws the lean block as code with the link inside it. Where the two differ, this head usually agrees with the rendered page, but not always:
  • If that last ``` is indented by one to three spaces, the page shows a real link to a, main kept the edge, and this head drops it. This is the sloppy-closer limit below.
  • Under ## Depends on, a ```lean line, -- see [a](a.md) and ``` -- end in one paragraph are drawn by the page as inline code with no link, because the unclosed fence line pairs with the later backtick run. main gave no edge to a; this head adds one. The README says so.

The coverage and link checks keep reading an unclosed fence as open, as on main: a table in the same paragraph as such a fence is not published. The bundled example's graph is identical before and after.

The render change in the first row of the table and this loader change are the ones to decide at review. The bundled example has no article in any row: its rendered site is byte-identical to main's.

Commit 2: audit statements that are empty or only a placeholder

A formalizable article passed the audit with TODO as its statement, or with markup that publishes nothing. The statement is judged as the site publishes it, so one whose published prose has a letter or digit is never missing or empty. At most one statement finding now fires per article, in this order:

• missing-statement-text (existing): no prose outside code blocks, HTML comments and headings.
• empty-statement-text: the published prose has no letter or digit.
• placeholder-statement-text: every word is one of pending, placeholder, todo, tbd, unknown, or the statement opens with one of them followed by a colon or a dash.

The prose is judged as the site publishes it, through a new markdown.visible_prose. The placeholder rule is the one coverage evidence already follows; is_placeholder and has_substance move from coverage.py to markdown.py so both share it.

What an existing user will notice:

• A blueprint with such statements gains findings, and autoform audit and autoform doctor then exit 1. No generated workflow runs either command. The bundled example gains none.
• Coverage behaviour change: a single hyphen or en dash marks a placeholder only when a space follows it, so evidence such as Unknown-variance case, ... is no longer rejected. The same rule now also accepts TBD-later, TODO-choose a milestone and pending-review. Across 7,130 generated evidence cells, these hyphen cases were the only verdicts that changed. Unknown–known duality ... passes for the same reason.
• The audit renders each formalizable statement, about 1 ms each: 0.64 s to 1.68 s at 1,000 articles.

Two renderer faults that coverage could already reach would otherwise reach every statement, so they are fixed here. Say if you would rather have them as a separate PR.

• rendered_visible_text raised an uncaught RecursionError on markup nested about 1,000 elements deep. Its tree walk is now iterative. published_tables still recurses and still raises on such input, as it does on main; statements do not go through it.
• A conversion that failed midway left the cached converter returning raw source for every later text. render_html now discards the converter when a conversion raises.

Commit 3: autoform search

autoform search TARGET QUERY [--lean-root PATH] [--state KEY]... [--declaration KIND]... [--limit N] [--json] reports the articles that contain every query term. It is read-only, keeps no index and starts no process. Each hit carries the statement as authored, the derived state, Lean targets with file and line, sources, and up to ten dependents with the full count. --json writes autoform-search/v1; the contract is in autoform_cli/README.md under "Search contract".

Where it departs from the issue, and why:

• Fields. lean and node_id match only the last component of a name, and a new lowest-ranked field, qualified_names, holds the path ID and Lean names in full. With the issue's fields, every article in a chapter matched the chapter's directory name: on a 2,031-article test blueprint, the one article whose statement was about a probability measure ranked 102 of 102 for "measure". It now ranks 2.
• ## Execution notes is not searched, although Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143 item 3 lists it, because Keep implementation notes separate from mathematical articles #172 (open) moves those notes out of the article. Indexing it now would add a matched_fields name to the contract that Keep implementation notes separate from mathematical articles #172 then empties.
• A full Lean name finds its owner first. A term that is a whole lean: or mathlib_declaration name, or its last components (Convex.separation of Project.Convex.separation), counts as a lean match, with or without _root_. and «». A namespace alone still matches only qualified_names. Otherwise an article that cites a declaration in its statement outranked the article that owns it. Commit 5 extends this to names ending in a prime, ? or !.
• Folding goes beyond case: width, accents on letters, typographic dashes and quotes, and invisible characters, so hahn-banach finds "Hahn–Banach". ≠ does not match =. A term sheds the sentence punctuation, quotation marks, backticks, $ and wrapping emphasis around it, and parentheses that are unbalanced or wrap the whole term, in any combination, so Hahn–Banach,, "non-ambiguous", `Nat.succ`, (**weak**), $L^2$, and (f(x)) find what the bare terms find. C*, foo_ and != are kept as typed.
• Titles are matched as the page shows them, like the statement: Non-*ambiguous* map is found by non-ambiguous, and an entity name or a link URL in a title is not searched.
• Softer terms. Words that carry no meaning (of, the, if, ...) are dropped, and a word of letters loses a common ending, so recovered finds recovers, topologies finds topology and cones finds cone. Only the query is shortened, so this only adds hits, and an article holding the words as typed is listed before one reached only through a shortened word.
• Ordering follows the issue (best field, dependents, node ID) with two tie-breaks before dependents: within one best field, an article holding every word as typed comes before one reached only through a shortened word, and then the hit whose weakest term sits in a better field comes first.
• Only the query is shortened. topologies and topology are both searched as topolog, so each finds the other, but a form that does not begin with the shortened word does not: indices does not find "index", sets "set", bodies "body", nor define "defining". Shortening is kept because it only ever adds hits, and a missed hit is what leads to a duplicate. The search contract states the limit.
• Extra keys: article_revision, mathlib_declarations, mathlib_file, shared_title per hit and open_statements at the top, since sibling schemas carry them and a key added later means a version bump.

Search rereads each article and exits 2 on bytes other than those the graph was built from, and refuses what autoform work refuses (a symlinked roadmap entry, an escaping target).

Commit 4: the skills search before adding a result

Search prevents a duplicate only if an agent runs it first, so three skill files gain one paragraph each. None restates a flag; each names autoform search and links to the search contract.

• Roadmap (skills/roadmap/SKILL.md): before adding a formalizable article, search by a few distinctive words and by a Lean name when one is known, read each hit's statement, and retry with fewer words and other usual names before treating the result as new. When another article already states the result, link to it under ## Depends on or ## Proof depends on and from the coverage row. A hit that is more general, a special case, or only similar does not replace the result.
• Formalize (skills/formalize/SKILL.md): before adding a helper, search the blueprint as well. A hit's declaration is used only when the claimed article's dependencies reach that hit's article and the open-statement policy allows it; a hit they do not reach is a missing prerequisite, never something to restate.
• Agent review (references/roadmap-quality.md): a new evidence item runs the search for each main result in scope and lists the queries. Finding no duplicate is not proof, because matching is literal.

Both skills say that a refusal (exit 2) is not an empty result. Two tests back this. One checks that every skill link into autoform_cli/README.md lands on an existing section. The other reads the paragraph that names autoform search in each file and checks that it keeps the rule: the contract link, the retry with fewer words, what to do with a hit (link under ## Depends on instead of adding a node; use a hit only when dependencies reach it, otherwise a missing prerequisite), and that a refusal is not an empty result. It is a presence check: each instruction must be there, in one sentence, but an inverted rule that kept the words would pass.

The paragraphs are insert-only and sit away from the lines #172 rewrites; the merge with #172 is clean in both orders and the merged tree's skill tests pass.

Commit 5: a Lean name ending in a prime, ? or !

A query term sheds the quote or sentence mark at its end, so Project.foo' was searched as Project.foo, while the index kept the name's own ending. The whole-name lookup of commit 3 therefore missed, and the owner of Project.foo', Project.get? or Project.get! was listed below every article citing it. The indexed name now loses the same ending as the term.

• Consequence: Project.foo is also a lean match for Project.foo'. The search contract says so.
• Two more tests cover branches of the full-name match that nothing exercised: a mathlib_declaration name, and a lean: name written with «» and searched without them.

Commit 6: a declaration kind no article uses

autoform search --declaration definition on a blueprint whose definitions are written def printed "No matching articles." and exited 0, which is the answer a new result gets. Search now exits 2 for a kind that no article in the blueprint declares and names the kinds in use:

error: no article declares kind definition; this blueprint uses: def, theorem

A kind in use that the query does not reach is still an ordinary empty result. The README states the rule, and also the second fence case from commit 1 (a link the page shows as inline code but the graph reads as a dependency).

Not in this PR

• Item 4, duplicate-lean-target (criterion: "autoform audit reports duplicate canonical primary ownership ..."). Per the maintainer's comment on Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143 it is to be implemented after Scale roadmap inventories and the full DAG explorer #90 and the refreshed Bind formalized Lean targets to built artifacts in CI #119 artifact layer, and the Reject duplicate formalized Lean targets #127 gate is not to be reused.
• autoform search --skeleton REPORT (the rest of item 3; criterion: "--skeleton refuses a report made for a different blueprint"). A report identifies the whole blueprint, so refusing on any difference makes the flag unusable while articles are being added, and accepting it lets an outdated signature through. The criterion needs a finer identity, to be agreed on Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143; the implementation is kept on a separate branch for a follow-up PR.
• The reverse-edge counter test. The test here counts what search adds per article, one read and one render; the graph and the runtime projection each read the article as well, so "read once" does not hold for a whole call.

Known limits

• Search cost is linear with no index: about 2 ms per article, 1.8 s at 1,000 articles. A statement with very many formulas costs what the site renderer costs.
• Search matching is by substring, all terms required, with no phrase or synonym handling: map matches roadmap, unambiguous does not match non-ambiguous, and ℝ folds to r, which matches nearly every article. The README tells agents to retry with fewer words before treating a result as new.
• --state keys are exact: proved does not include fully_proved.
• source_revision comes from the runtime's read, which upstream does not compare with load_graph's. Search binds its own read to the graph's hashes; closing the remaining gap is a two-line change in runtime.py that I left out of this PR.
• A comment that never closes hides every heading and link after it, for the graph as well, although the site shows them: the audit reports missing-depends-section only when the comment sits above that heading on a formalizable article. This is main's behaviour.
• A real statement that opens Unknown: ... or Pending: ... is reported as a placeholder and needs rewording, and one written in symbols alone (⊥ ≠ ⊤.) is reported as empty; To be written and TODO state it pass and are left to review. The README documents these.
• Search exits 2 on a blueprint the graph rejects, which is common while articles are being written; the skills tell the agent to resolve the refusal and search again.
• A fence whose closing line carries trailing text is closed by a later bare fence line of the same character and at least its length, even one that opens a longer or indented block, where the site asks for the opener's exact length and indent. The headings and links between the two are then hidden from the graph although the page shows them. This needs both a sloppy closer and a later, longer fence in one article; the README says so and a test pins it.
• Reading an unclosed fence as text rereads the article from that fence, which is more than linear on input built for it: 2,000 bare openers of strictly decreasing length take about a second, and about 14 seconds when each has an info string. Ordinary articles are unaffected. One backward pass would remove the reread; I left it for a follow-up.
• autoform_cli/render.py keeps its own fence readers with the old rule, so a ### after an unclosed fence inside a statement is not demoted on the page.
• --declaration is checked against the blueprint, not against a fixed list: a kind no article declares exits 2 and names the kinds in use (commit 6), so the filter cannot be used on a blueprint that has no article of that kind yet.
• The page can pair an unclosed backtick fence line with a later backtick run in the same paragraph and show a link between them as inline code; the graph still reads that link as a dependency.
• A BOM before the frontmatter puts the frontmatter into the statement, as on main; search and the statement audit now read it.
• Square brackets are kept on a term, so [weak] and a pasted [[wikilink]] are searched with them.
• foo' is searched as foo, so a search cannot tell foo from foo': both owners are lean matches for either spelling, bare or qualified. Keeping the quote would make a possessive miss.

Overlap with open PRs

• Keep implementation notes separate from mathematical articles #172: the merge is textually clean, but Keep implementation notes separate from mathematical articles #172's tests/test_audit.py::test_container_note_audit_handles_deep_containment_iteratively builds _ArticleShape(True, True), and commit 1 makes the first field statement: str. Whichever lands second changes that stub to _ArticleShape("x", True). Search reads no notes.
• Allow proof imports with measured impact #183 conflicts in autoform_cli/__main__.py (same spot as the search parser) and in autoform_cli/README.md; whichever lands second needs a small rebase.
• Scale roadmap inventories and the full DAG explorer #90 edits audit._read_article and nearby lines; a small manual rebase for whichever lands second.
• Publish blueprint sites transactionally #165 conflicts in coverage.py (import block), render.py and tests/test_render.py, and touches markdown.__all__; coverage's call sites are unchanged here to keep that small.
• Bind statement: formalized to a recorded statement_hash #141 adds its own article_statement. article_parts(...).statement is meant to be the one definition it reuses.

Testing

• make lint clean; make check-example passes.
• make test in a worktree of 22d1c02: 2,021 passed, 1 failed. The failure is tests/test_claims.py::test_cas_acquire_race_has_exactly_one_winner, in files this PR does not touch; it fails there on untouched main as well.
• Each of the first four commits passes lint and the full suite on its own, apart from that test; commits 5 and 6 were added on top.

🤖 Generated with Claude Code

[zibo-yang]

Code review against #143 phase 1

Reviewed at head faee1c2 (five commits) against the phase 1 items and acceptance criteria in #143. Every blocking item below was reproduced by running the code at that head; line numbers refer to it.

Summary. The PR delivers items 1, 2, 3 and 5 and most of it is ready. It does not yet complete phase 1: item 4 is absent, --skeleton reverses one acceptance criterion, and search has two cases where it reports no match for a result that exists. Of the 15 phase 1 criteria I count 11 met, 2 partly met and 2 not met.

Criterion	Verdict
One statement-span function used by audit, render and search	Met (see B4 for the graph loader)
Tests for each audit/render disagreement case	Met
placeholder-statement-text and empty-statement-text with tests	Met
Search finds by statement, title, lean: name, and two terms in two fields	Met
Frontmatter, fenced, indented and commented text gives no hit	Met
Deterministic order and JSON bytes; source_revision; no timestamp or absolute path	Met
Hit carries statement, state, Lean targets, sources, capped dependents with count	Met
Writes nothing, starts no process, refuses a symlinked roadmap	Met
Human output escapes nonprintable characters	Met
New audit codes give no finding on the bundled example, with its own test	Met
make test, make lint, make check-example	Met (lint clean; 1,987 passed; the one local failure is test_claims.py::test_cas_acquire_race_has_exactly_one_winner, in files this PR does not touch)
Skills state the search-first rule, README documents it, tests assert both	Partly (S2)
Counter test: each article read once, reverse edges built once	Partly (S3)
--skeleton refuses a report made for a different blueprint	Not met (B2)
autoform audit reports duplicate primary ownership	Not met (B1)

Blocking

B1. Item 4 (duplicate-lean-target) is not in the PR, and the PR does not say so

Nothing in the diff implements it, while the title reads "phase 1" and the description opens "Part of #143 (phase 1)". Deferring it is reasonable: the comment on #143 sequences it after #90 and the #119 artifact layer, and rules out reusing #127. The PR should state that.

• Retitle to name the items delivered, for example "Blueprint search and reuse: phase 1 items 1-3 and 5 (Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143)".
• Add a "Not in this PR" section naming item 4, its acceptance criterion, and the sequencing.

B2. --skeleton can attach a stale signature while reporting that the report matches

The issue says search refuses a report whose blueprint identity differs. The PR uses the report and exposes skeleton_matches_blueprint. SkeletonReport.describes (skeleton.py:406) compares one hash over all article Markdown, so the flag is wrong in both directions:

• Lean edited, Markdown untouched. With a report recording Project.separation : True, I changed the source to theorem separation (h : 1 = 2) : False. Search returned "signature": "Project.separation : True" with "skeleton_matches_blueprint": true, exit 0, empty stderr.
• Any article added. The flag becomes false for every later search, which is the normal state while Roadmap is adding articles, so it stops carrying information.
• --json prints no warning, and the human warning says signatures "may be missing", not that they may be outdated or from another project.

The description's argument that whole-blueprint refusal makes the flag unusable during roadmap work is sound, but it shows the criterion needs a finer identity, not a boolean. Options, in my order of preference:

1. Move commit 5 out of this PR and land it after Bind statement: formalized to a recorded statement_hash #141, which adds a per-article statement hash and makes a per-target check cheap. Commits 1 to 4 do not depend on it.
2. Keep it here, refuse on mismatch by default with an explicit override flag, and add a per-target check against the path, start_line and written statement the report already records, emitting signature: null when they differ.

Either way the change to the criterion needs the maintainer's agreement on #143.

B3. Search reports no match for results that exist

Both cases exit 0 with an empty result, which an agent will read as "this result is new".

Punctuation on a hyphenated or alphanumeric word is kept in the term. _words (search.py:302-316) strips sentence punctuation only when the stripped word is alphabetic (bare.isalpha(), line 313). For a statement "The map is non-ambiguous, and Hahn–Banach holds.":

Query	Hits
hahn-banach	1
Hahn–Banach,	0
"non-ambiguous"	0

Suggested fix: always use the stripped word, and fall back to the original only when stripping leaves nothing. Add a test with a trailing comma on a hyphenated word.

Titles and ancestor titles are matched as Markdown source. search.py:380 and :384 normalize node.title directly, while the statement goes through visible_prose. For a title Non-*ambiguous* map at café [linked](http://urlword.example):

Query	Result
non-ambiguous	not found
café	not found
eacute, urlword	hit on title

The issue asks for prose fields to be matched on rendered text, and title is the top-ranked field. Suggested fix: pass titles through visible_prose.

B4. The audit can lose missing-depends-section when the graph drops the edge

audit.py:260-263 now derives the section list from article_parts, while graph._parse_node (graph.py:384) keeps its own comment and fence rules. They disagree on malformed input. Inserting this before ## Depends on in the example's non-ambiguity.md:

```html
<!-- an example of markup
```

makes the graph drop the dependency edge on both main and this PR. main's audit reports missing-depends-section for the file; this PR's audit reports nothing. It needs an unclosed comment inside a fence, so it is rare, but it removes the only finding for a silently lost edge.

Suggested fix: have graph._parse_node take its sections from article_parts, which also makes "one definition" true for the loader. Otherwise keep the audit's depends check on the graph's reading and note the limit.

Should fix

• S1. Query stemming changes the issue's ordering and is asymmetric. With a title "Weak topology" and a statement "Several topologies are compared here", topologies lists the statement match above the title match, and topology does not find the second article. indices is searched as indic (matches "indicator", misses "Index"); mapping as mapp (misses "map"). The issue did not ask for stemming. I would remove _stem, _WORD_ENDINGS and the exact-first sort key, and keep the README's "retry with fewer words" advice. If it stays, the description should say ordering departs from the issue in two ways, not one.
• S2. The skill prose test guards wording, not the rule (tests/test_skill_examples.py:861). Deleting Roadmap's "link to it ... instead of adding a node" instruction leaves it passing, while rewording "Matching is literal, so" fails it. Assert the semantic anchors (## Depends on near the search rule, missing prerequisite, the contract link) and drop the incidental phrases.
• S3. The read-once test counts search's own wrapper (tests/test_search.py:449). Counting real reads gives three per article per search (load_graph, build_runtime_graph, and search's reread). Count real reads and assert the actual number, or rename the test. The reverse-edge counter is still absent, as the description says.
• S4. Description corrections.
  • The hyphen change (markdown.py:101) also accepts TBD-later, TODO-choose a milestone and pending-review as coverage evidence, not only Unknown-variance case.
  • The RecursionError fix covers rendered_visible_text only; _collect_tables and _visible_rows (markdown.py:352, :386) still recurse, so published_tables("<div>" * 1500 + "x") still raises.
• S5. No skill mentions --skeleton or tells an agent how to read its flag, so the feature has no caller in the product. This resolves itself if commit 5 moves out.

Minor

• ℝ and ℕ fold to r and n, which match nearly every article. Worth a README warning or a refusal of one-letter terms.
• --declaration bogus returns "No matching articles" at exit 0. Echoing the active filters and searched terms in the human footer would make a typo visible.
• Lean target resolution in search repeats the runtime's logic without its "escapes the Lean root" guard. I found no triggering input; reusing the helper keeps one enforcement point.
• Commit 3 emits a different autoform-search/v1 than commit 5. Squash on merge, or fold the two keys into commit 3.
• markdown.HTML_COMMENT and markdown.FENCE remain in __all__ with no importer.
• The README's filters sub-keys are not named, and mathlib_declarations is missing from the description's list of extra keys.

What holds up

• article_parts and visible_prose are a clean seam, and audit and render lose their hand-rolled parsers. The example site renders byte-identically to main and gains no audit finding.
• The converter-cache fix is a real bug with a regression test.
• Search is deterministic, read-only, starts no process, refuses symlinked entries and changed bytes, and escapes article text in human output. I found no query input that produces a traceback.
• Matching lean and node_id on the last component, with qualified_names ranked last, is a real improvement on the issue's field list.
• The skills link to the contract and restate no flag, and the description's claims about Bind statement: formalized to a recorded statement_hash #141 and Keep implementation notes separate from mathematical articles #172 compatibility check out.

Suggested path

1. Fix B3 and B4, and remove the stemmer (S1).
2. Retitle and add the "Not in this PR" section (B1); correct the description (S4).
3. Tighten the two tests (S2, S3).
4. Move commit 5 to a follow-up after Bind statement: formalized to a recorded statement_hash #141, or apply option 2 under B2 with the maintainer's agreement.

With 1 to 3 done, commits 1 to 4 are ready to merge as items 1, 2, 3 (without --skeleton) and 5.

[zibo-yang]

Second review against #143 phase 1

Reviewed at head a159b8a (four commits), following the first review at faee1c2. Every blocking item below was reproduced by running the code at this head. Lint is clean, make check-example passes, and the suite gives 1,985 passed with one local failure in test_claims.py::test_cas_acquire_race_has_exactly_one_winner, in files this PR does not touch.

Summary. The rewrite resolves all four blocking findings of the first review, and the PR's scope statement is now accurate: it delivers items 1, 2, 3 (without --skeleton) and 5, and declares what it leaves out. It is not ready to merge yet. The graph loader change introduces one regression against main, and search still hides or misses an existing result in three reproducible ways. Phase 1 as a whole stays open until item 4 and --skeleton land in follow-ups.

Status of the first review

Finding	Status
B1. Item 4 absent and undeclared	Resolved: retitled, "Not in this PR" added
B2. --skeleton attaches a stale signature	Resolved: removed from the PR, no leftovers in code, README or tests
B3. Punctuation and Markdown-title false negatives	Resolved: Hahn–Banach,, "non-ambiguous" and café hit; eacute and urlword do not
B4. Audit loses missing-depends-section	Resolved for the reported case; see N1 for what the fix changed
S1. Query stemming	Kept; it is the cause of N2
S2. Skill test guards wording	Improved, still phrase-pinned (see below)
S3. Read-once test	Resolved by declaring it: the description now says what the test counts
S4. Description corrections	Resolved
S5. No skill mentions --skeleton	Moot

Phase 1 acceptance criteria

12 met, 1 partly met and declared (the read-once and reverse-edge counter test), 2 deferred and declared (--skeleton refuses a foreign report; autoform audit reports duplicate primary ownership). Nothing is silently missing.

Blocking

N1. The graph drops edges that main keeps and the page shows

graph._parse_node now takes its lines from _mask_fences_and_comments (graph.py:397), where a closing fence with trailing text does not close. Inserting this directly under ## Depends on in the example's non-ambiguity.md:

```lean
example : True := trivial
``` -- end

	Dependencies of non-ambiguity	Audit finding for the file	Link on the rendered page
main	eligibility	none	shown
this PR	none	none	shown

The description says a fence "closes only on a bare fence line now, as on the page". The site renderer treats a fence that never closes as no fence, so the page still shows the link and the graph has lost the edge with no diagnostic. The "Known limits" entry covers only the case where the audit reports missing-depends-section, which needs the fence to sit above the heading on a formalizable article.

Suggested fix, either of:

1. Treat a fence still open at the end of the article as not a fence, as the renderer does.
2. Keep the rule and have the audit report an unclosed fence or comment on every article.

Add a graph test for the fence-close rule in both cases; tests/test_graph.py covers only the comment-inside-fence case.

N2. The "as typed" tier outranks field rank and pushes the canonical article past the limit

search.py:221-226 sorts articles holding every word as typed above all others, before the field rank. With a chapter titled "Separating hyperplanes" holding 25 unrelated articles, and an article titled "Hyperplane separation theorem" elsewhere:

Query	Total matches	Position of "Hyperplane separation theorem"
hyperplanes	28	28th; absent from the default 20

The 25 unrelated articles match only through ancestors and all precede a title match. An agent reading the first page concludes the result is new, which is the outcome search exists to prevent.

Suggested fix: apply the as-typed tie-break inside a field rank, not above it. Removing the stemmer (S1 of the first review) also removes the tier.

N3. Search reports no match for results that exist

All cases exit 0 with an empty result. The statement used is "The family of inequalities on boundaries uses `Nat.succ` and f(x)." under the title "Weak topologies".

Query	Terms searched	Hits
`Nat.succ`	`nat.succ`	0
Nat.succ	nat.succ	1
**weak**	**weak**	0
weak topology	weak, topology	0
topologies	topolog	1
inequality, boundary	as typed	0
(see f(x))	see, f(x))	0
(f(x))	(f(x))	0
f(x),	f(x)	1

Three causes, each a few lines in _words or _stem:

• Markdown quoting is not shed. Agents paste backticked Lean names, and the published text carries no backticks. Add ` and * to the stripped set.
• Shortening is one-directional and the README does not say so. The singular in -y never finds the plural in -ies. Either cut a final y after a consonant as well, or remove the stemmer; in both cases state the limit in the search contract, not only in the PR description.
• The unbalanced-bracket fallback is all-or-nothing (search.py:293-296). Strip brackets one at a time while they are unbalanced.

Should fix

• Merging with Keep implementation notes separate from mathematical articles #172 breaks a test. The merge is textually clean, but tests/test_audit.py::test_container_note_audit_handles_deep_containment_iteratively fails on the merged tree with AttributeError at markdown.py:176: Keep implementation notes separate from mathematical articles #172's test builds _ArticleShape(True, True) and commit 1 makes the first field statement: str. The description says "compatible". State it, so whichever lands second updates the stub.
• The overlap section is understated. Trial merges also conflict with Allow proof imports with measured impact #183 in autoform_cli/README.md and with Publish blueprint sites transactionally #165 in render.py and tests/test_render.py.
• The skills never say "exit 2". The description says they do; skills/roadmap/SKILL.md:64 and skills/formalize/SKILL.md:84-86 say only "refusal". Suggest "A refusal (exit 2, an error: line) is not an empty result".
• The skill test still pins phrases (tests/test_skill_examples.py:861-892). Deleting a rule is now caught, which is the main gain. An inverted rule that keeps the keywords passes, "rather than adding a node" fails, and a second paragraph naming autoform search fails with ValueError: too many values to unpack in place of an assertion. Either describe it as a presence check, or assert that "instead of adding" sits in the same sentence as ## Depends on.
• Undocumented statement-audit false positives. Pending: a transaction $t$ is pending if ... and Unknown–known duality holds ... are reported as placeholders, and a symbol-only statement such as ⊥ ≠ ⊤. as empty. The README documents only Unknown:.

Minor

• != and := become the term =, which matches every equation.
• foo' is searched as foo; it still finds the primed name but cannot rank it first.
• graph.py:19 imports the private markdown._mask_fences_and_comments; a public wrapper would drop the throwaway set() argument.
• SearchHit, SearchLeanTarget and SearchResult are in search.__all__ with no importer.
• The audit renders each statement: 0.76 s on main against 2.39 s here at 1,500 synthetic articles. The description states this cost.
• A blueprint the graph rejects makes search exit 2, which is common mid-authoring. Worth a line under "Known limits".

What holds up

• Audit, render and graph now read fences and comments through one helper. The example's graph is field-for-field identical to main's and its rendered site is byte-identical.
• The comment-opener-inside-a-fence fix is real: main loses the edge, this PR keeps it, and a test covers it.
• Search produced no traceback for any input tried, its JSON bytes are identical across hash seeds and working directories, it carries no absolute path, and the emitted keys match the README contract exactly.
• The stemmer has a four-letter minimum and only ever yields a prefix, so the claim that shortening never removes a match is true for the match set. The problem is ordering (N2), not membership.
• Lint is clean at each of the four commits, no commit imports something a later one adds, and the skill paragraphs restate no flag and contradict no neighbouring rule.

Suggested path

1. Fix N1 and add the fence-close graph test.
2. Fix N2 and N3 in _words, _stem and the sort key, with one test per row of the N3 table, and state the shortening limit in the README.
3. Correct the Keep implementation notes separate from mathematical articles #172, Allow proof imports with measured impact #183 and Publish blueprint sites transactionally #165 overlap notes and the "exit 2" sentence.

With 1 and 2 done, this PR is ready to merge as items 1, 2, 3 (without --skeleton) and 5.

[zibo-yang]

Third review against #143 phase 1

Reviewed at head 695650e (four commits), following the second review at a159b8a. Lint is clean, make check-example passes, and the suite gives 2,004 passed with one local failure in test_claims.py::test_cas_acquire_race_has_exactly_one_winner, in files this PR does not touch. Items under "Fix before merge" were reproduced by running the code at this head.

Summary. All three blocking findings of the second review are resolved. The PR is close to ready for the scope it states: items 1, 2, 3 (without --skeleton) and 5. Two small search misses remain and are worth fixing before merge; one rare leftover of the fence regression can be accepted as a documented limit. Phase 1 as a whole stays open for item 4 and --skeleton, as "Not in this PR" says.

Status of the second review

Finding	Status
N1. Graph drops an edge after ``` -- end	Resolved for the reported case: the eligibility edge is kept, as on main. A rarer variant remains (R3)
N2. "As typed" tier outranks field rank	Resolved: "Hyperplane separation theorem" is 3rd of 28 for hyperplanes, was 28th
N3. Misses on backticks, emphasis, -y singulars, brackets	Resolved: `Nat.succ`, **weak**, weak topology, inequality, boundary and (f(x)) all hit
#172 merge breaks an audit test	Still true, now stated in the description
Overlap notes for #183 and #165	Resolved
Skills never say "exit 2"	Resolved
Skill test pins phrases	Now declared a presence check; every rule deletion is caught, and a second paragraph gives a clear assertion message
Undocumented statement-audit false positives	Resolved: the README documents Pending:, the en dash and symbol-only statements
!= and := become =	Resolved: kept as typed

Fix before merge

Both cases exit 0 with an empty result. The test article is titled "Convex cone", with the statement "A face of the cone is an edge or a line in $L^2$ with weak closure and a level set."

R1. A plural in -es with a four-letter singular is never shortened

Query	Terms searched	Hits
convex cone	convex, cone	1
convex cones	convex, cones	0
faces, edges, lines	as typed	0

The loop in _stem (search.py:339-349) matches es first, gets a three-letter stem, and returns the word without trying s. nodes, trees, types, cases and bases behave the same. This also contradicts the search contract, which says a word sheds a final s "when four letters remain": dropping the s from cones leaves four.

Suggested fix: continue to the next ending when the stem is too short, and add cones to the parametrized test.

R2. Wrappers are peeled in a fixed order, so combined ones survive

Query	Terms searched	Hits
$L^2$	l^2	1
L^2,	l^2	1
$L^2$,	l^2$	0
**weak**	weak	1
(**weak**)	**weak**	0

$ is stripped before the sentence punctuation (search.py:288), and emphasis is peeled before brackets, once (:303-311). A formula pasted with its trailing comma is a likely query.

Suggested fix: treat $ as one of the peeling steps in _bare and repeat the steps until the term stops changing.

Document or follow up

R3. Residual fence case

With the sloppy closer from N1 and a later fenced block whose fence is longer or indented, the graph treats that later line as the closer and masks everything between. I inserted the ```lean … ``` -- end block above ## Depends on in the example's non-ambiguity.md and appended a ## Notes section holding a four-backtick block:

	Dependencies of non-ambiguity	Audit finding for the file	Raw render shows the heading
main	eligibility	none	yes
this PR	none	missing-depends-section	yes

Here the audit reports it. With the sloppy fence under the heading instead, a fuzz run found the same edge loss with no finding (not re-run by hand). The cause is that markdown.py:695-699 closes on any bare marker at least as long as the opener at up to three spaces, while the site's fence extension needs the same length and indent.

A differential fuzz against the renderer puts this at 3 to 9 per 40,000 generated articles, down from 70 at the previous head, and over the differing articles this head agrees with the rendered page far more often than main does. I would accept it as a known limit with one test and one sentence under "Known limits" and in the README, which currently says only "closes only on a bare fence line".

Other items

• Test gaps in the fence loop. No test pins "a closed fence after an unclosed one is still hidden" (the existing test has the closed fence first) or that comment state is restored on rewind; both mutants pass the suite. The 20,000-line test has no time bound.
• Worst-case cost. The rewind is super-linear on adversarial input: 2,000 openers of strictly decreasing length (2 MB) take 0.67 s here and more on variants with long marker lines; main is linear. Ordinary articles are unaffected. One backward pass that records the longest later closer per fence character would remove the rewind.
• Stemmer limits the README does not list. level sets does not find "Level set" (three-letter singular); from a wider sweep, body and bodies miss each other, and define does not find "defining". The contract names only irregular forms.
• Brackets means parentheses. [weak] and a pasted [[wikilink]] keep their brackets. The contract sentence on shedding does not mention parentheses or this limit.
• "As typed" is judged over all fields (search.py:219), while the README says "Within one field". Harmless in practice; align one with the other.
• sentence() in the skill test (tests/test_skill_examples.py:883) raises ValueError: too many values to unpack when its phrase occurs in two sentences. Give it the same assertion message as rule().
• foo' has no test, and skills/roadmap/SKILL.md:64 is 89 columns.

What holds up

• The backtracking loop agrees with an independent reference implementation on 450,000 random inputs, in output and hidden set, and it terminates: each rewind strictly lowers the recorded opener length.
• The bundled example's graph, audit findings, site-src and built site are identical to main's.
• The ordering is as documented, and a test asserts that a title match reached by a shortened word precedes a statement match as typed.
• No stem is a non-prefix of its word across 1,083 words, so shortening only adds matches. Over 24 queries on the bundled example no exact hit was lost.
• Search JSON is byte-identical across hash seeds, its keys match the README, and every refusal is a one-line error with exit 2.
• Every deletion of a skill rule is caught by the test, and both skills say "refusal (exit 2)".

Suggested path

1. Fix R1 and R2, with one test row each.
2. Add the R3 test and known-limit sentence, and the closed-after-unclosed fence test.
3. List the remaining stemmer and bracket limits in the search contract.

With step 1 done and R3 documented, I consider this PR ready to merge as items 1, 2, 3 (without --skeleton) and 5.

[zibo-yang]

Fourth review: no blocking findings

Reviewed at head 516a2f0 (four commits), following the third review at 695650e. Lint is clean, make check-example passes, all five CI checks pass, and a local run gives 2,012 passed with one failure in test_claims.py::test_cas_acquire_race_has_exactly_one_winner, in files this PR does not touch.

Summary. Every finding of the third review is resolved, and this round found nothing blocking. The PR is ready for maintainer review for the scope it states: phase 1 items 1, 2, 3 (without --skeleton) and 5. Item 4 (duplicate-lean-target) and --skeleton remain for follow-ups, as "Not in this PR" says.

Status of the third review

Finding	Status
R1. A plural in -es with a four-letter singular is never shortened	Resolved: convex cones, faces, edges and lines find the singular
R2. Combined wrappers survive	Resolved: $L^2$, and (**weak**) hit
R3. Residual fence case	Documented in the README and under "Known limits", and pinned by a test
Test gaps in the fence loop	Resolved: the three mutants that passed the suite last round now fail a named test
Stemmer, bracket and ordering wording in the search contract	Resolved; each listed limit matches behaviour
sentence() error message, foo' test, 89-column line	Resolved

What this round checked

• The two code changes only widen matching. Comparing this head with 695650e over 200,000 generated terms and about 222,000 words, every changed term is a substring of the one it replaces and every changed stem is a prefix of its word. Nothing raises, hangs or becomes empty.
• Each fix is pinned. Reverting the stem fall-through, the repeated peeling, or the $ handling fails a named test, as do the three fence-loop mutations and a second ## Depends on sentence in the Roadmap rule.
• Search output is stable. JSON bytes are identical across hash seeds, the keys match the README contract, and every refusal exits 2 with a one-line error.

For the maintainer to decide

The description flags two behaviour changes as the ones to decide at review:

1. Statement box. With an H3 before the first H2, the published theorem box now runs to the first H2 instead of stopping at the H3.
2. Graph loader. A fence closes only on a bare fence line, and a fence that never closes hides nothing. The bundled example's graph and rendered site are identical to main's.

Follow-up material, none blocking

• Short plural stems match more widely. lines is searched as line, so it also matches "linear". The query line already did; a clause in the search contract would be enough.
• Shortening is still one-directional for short -y words. convex body does not find "Convex bodies"; the contract states only the reverse direction.
• Rewind cost on input built for it. 2,000 fence openers of decreasing length take 0.6 s as bare lines and about 13 s with an info string on each; the description now says so. One backward pass would remove the rewind.
• Merging with Keep implementation notes separate from mathematical articles #172 still needs the one-line stub change the description names, in whichever lands second.

[zibo-yang]

Review of 516a2f0 against #143 phase 1

Summary: no critical defects; two small code fixes and two decisions are requested before merge. The PR delivers items 1, 2 and 5 and most of item 3. Item 4 and --skeleton remain open, so #143 should stay open after this merges.

Verified on this head: make lint is clean on each of the four commits, make check-example passes, and make test gives 2,012 passed with one failure (tests/test_claims.py::test_cas_acquire_race_has_exactly_one_winner) that also fails on cc7e3a8. The bundled example's rendered site, runtime graph and audit output are identical to main's.

Requested before merge

1. An exact Lean name ranks the owning article below articles that only cite it (autoform_cli/search.py, _FIELDS and the lean / qualified_names entries of the field index)

Blueprint: c/owner.md and c/dup.md both declare lean: Project.Convex.separation; three lemmas each say "By Project.Convex.separation the claim follows."

$ autoform search blueprint "Project.Convex.separation"
Corollary 0 (c/user0)      Matched: statement_text
Corollary 1 (c/user1)      Matched: statement_text
Corollary 2 (c/user2)      Matched: statement_text
Separation (c/owner)       Matched: qualified_names
Separation of convex sets (c/dup)   Matched: qualified_names

Convex.separation gives the same order; the bare separation ranks the owners first. The lean field holds only the last component of each name, so a qualified query can match an owner only through qualified_names, the lowest-ranked field. The Roadmap skill in this PR tells agents to search "by a Lean name when one is known", so for a widely cited declaration the owner can fall past --limit.

Suggested fix: when a term equals a full lean: or mathlib_declaration name, or a dot-bounded suffix of one, count it as a lean match. Keep qualified_names for namespace-only matches, which preserves the fix for the chapter-name problem. Please add a test with a citing article and an owning article.

Related, lower priority: _root_.Project.Convex.separation and Project.Convex.«separation» return "No matching articles." with exit 0, which an agent reads as "new". #143 item 4 treats these spellings as one identity.

2. missing-statement-text fires on a statement the site publishes (autoform_cli/audit.py, _statement_finding)

Article body with a fence that never closes:

# T

```
For all n, P(n) holds.

## Depends on

article_parts(...).statement is '```\nFor all n, P(n) holds.' and visible_prose returns '``` For all n, P(n) holds.', but _statement_finding returns missing-statement-text. The first check goes through _content_lines, which keeps the "unclosed fence stays open" rule, while the span and the two later checks use the new "unclosed fence is text" rule. The input is malformed, so the impact is small, but it is two readings inside the function that is meant to have one.

Suggested fix: decide "missing" from the same masking article_parts uses, or from the rendered text.

3. Decision needed: ## Execution notes is not searched

#143 item 3 lists it as an indexed field, and the section is in use on main. The PR's reason is that #172 moves the notes, but #172 is unmerged. Please either index it below statement_text, or confirm here that leaving it out is intended and update #143 to match.

4. Decision needed: the loader change can also remove edges and reject blueprints that load on main

The description presents the fence change as losing no edge. A differential run of load_graph on cc7e3a8 and 516a2f0 over 3,000 generated article bodies found 297 that differ: 176 newly fail with multiple H1 titles, 6 newly load, and 115 change edges, 4 of them losing one. Every case needs an unclosed fence or a fence line with trailing text. One that loses an edge:

## Depends on

``` -- end
```lean
- [a](a.md)
   ```

This yields the edge to a on main and none on this head. Where compared with render_html, the new behaviour matches what the site shows, so the code looks right. The request is to state in the description that autoform check can newly fail or change the graph on such articles, since this is one of the two changes the description asks the maintainer to decide.

Follow-ups, not blocking

• autoform_cli/render.py still has its own fence readers (_outside_fences and two loops on render._FENCE) with the old rule, so an ### after an unclosed fence inside a statement is not demoted.
• --declaration accepts any string: --declaration theorm returns no hits with exit 0. --state is validated.
• The Lean: and Mathlib: lines of the human output are escaped, but no test covers them; removing the escaping there leaves the suite green.
• markdown.HTML_COMMENT is no longer used but is still in __all__.
• A BOM before the frontmatter puts the whole frontmatter into the statement, now reachable through search and the audit.
• The unclosed-fence reread is super-linear on adversarial input (about 13 s for 2,000 openers with info strings) and runs in load_graph; the description already notes this.

Phase 1 status after this PR

Item	Status
1. One statement span	Done, apart from point 2 and the render.py follow-up
2. Statement text contract	Done
3. autoform search	Done except --skeleton, ## Execution notes (point 3) and the ranking in point 1
4. duplicate-lean-target	Not started; two articles with the same primary lean: name still pass the audit
5. Skills search first	Done; the skill test checks that the wording is present, as the description says

Two acceptance criteria are unmet (--skeleton refuses a foreign report; duplicate primary ownership) and one is partly met: the counter test counts only what search adds, while each article is read three times per call and nothing asserts that reverse edges are built once. Deferring item 4 and --skeleton is reasonable for the reasons given in the description; tracking them as separate issues would keep "phase 1" from reading as complete.

[zibo-yang]

Execution notes is left out of search on purpose. #172 moves those notes out of the article, so indexing the section now would add a matched_fields name that #172 then empties. I'll update #143 item 3 to match; if #172 does not land, indexing it below statement_text is a small follow-up.

[zibo-yang]

Final review at 22d1c02

An independent review of the six commits against #143 and this description, run without reference to the earlier review rounds. Every finding below was reproduced by running the code.

Verdict: ready to merge. No finding ships a wrong result or breaks a CLI or JSON contract. One finding is worth fixing before the next release and is tracked in #199.

Validation

Check	Result
make lint	clean
make test	2021 passed, 1 failed, 55 skipped, 1 xfailed
make check-example	exit 0
CI	all jobs pass, including real Lean

The one failure is tests/test_claims.py::test_cas_acquire_race_has_exactly_one_winner. It fails the same way on main at cc7e3a8, in files this PR does not touch. Seven hand-made mutants of the new behaviour were each killed by a named test.

What held up

• One statement definition. A differential fuzz of 3,833 generated articles, main against this head, found only the statement changes this description discloses, plus two benign whitespace changes now added to it.
• Bundled example. Its rendered site differs from main's only in the embedded commit SHA, and its audit output is identical.
• Search safety. Search exits 2 for a symlink at every level, non-UTF-8 bytes and an escaping source target. It starts no process and writes nothing.
• Search output. Human output escapes control and bidirectional characters. JSON is byte-identical across invocation styles and carries no absolute path.

Findings

Important: an unclosed fence now passes every tool while the chapter page is still corrupted (#199). The loader reads a fence that never closes as plain text, on the premise that the page draws it that way. That holds for a page with one article. On a chapter page the opener pairs with a later article's closing fence, and one code block swallows the next article's theorem box. The page was equally corrupted on main, and the graph is more correct here. What is lost is the audit's missing-depends-section finding, which was the only signal the author got. This is not a merge blocker because the trigger is an authoring typo, the corruption is not new, and the fix is additive.

Minor, search (#200):

• --declaration with two kinds exits 2 when only one of them is unused.
• A primed name does not rank its owner first when the unprimed name also exists.
• A space inside «» turns a namespace into a lean match.
• The README's search contract freezes the filler words and stemming rules.

Minor, parsing (#201): graph.py and render.py keep private copies of the fence and heading rules, and four readers in render.py still use the old one.

Description corrections

Edited in place to match what the code does:

• The "Indented code only" row: any statement whose first line is indented code changes from a paragraph to a code block.
• The notes below the statement are rebuilt with blank lines between sections.
• The unclosed-fence premise is qualified for chapter pages, with a link to Audit should report a code fence that never closes #199.
• The reread cost: about 14 seconds for 2,000 openers with an info string, not about a second.

Not checked

• Merge cleanliness against Keep implementation notes separate from mathematical articles #172, Allow proof imports with measured impact #183, Scale roadmap inventories and the full DAG explorer #90, Publish blueprint sites transactionally #165 and Bind statement: formalized to a recorded statement_hash #141.
• The 7,130 evidence-cell figure and the 2,031-article ranking anecdote in this description.
• ## Execution notes is not indexed, although item 3 of Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143 asks for it. The description defers this to Keep implementation notes separate from mathematical articles #172; that is a maintainer decision.

[Deicyde]

Follow-up to our review

We reviewed this PR at 516a2f00, but it merged before we posted. The findings that still hold on main are now in draft #208:

• the docs for where a statement ends when an H1 follows a section;
• four contract tests: a fence closes only on its own character, matched_fields order, the unclosed-fence reread count, and the CLI reference's autoform search examples;
• two small cleanups in markdown.py;
• doc corrections for search title matching, S^1 versus S¹, unclosed HTML comments, and heading-only statements.

The statement-audit fence regression we found at 516a2f00 is already fixed on main. One question is for @zibo-yang: should an exact title rank first in search? #208 has the data (on Hatcher, Homology is 42nd of 147 hits for its own title) and a four-line change.

Posted by PR swarm: PR Swarm Lead