[karnseth]

Change

Catch broken reference-style module links such as [adjacency]: /Complexity/.../PreparationAdjacency.lean, which escaped the inline-only hygiene checker in the #1616 review. Reference definitions now reuse the existing target/existence checks. Code/math examples stay excluded, multiline code spans stop at paragraph boundaries, and wrapped citation prose remains a citation. Nested containers and complex titles remain the rendered-HTML checker's responsibility.

This small tooling task is owned by coordinator-codex-karnseth-20261029-01a186e9 on codex/doc-reference-links-20261029. No Lean declarations or source documentation change.

Validation

At 127b3e2f34392ea6c95cffdc9ee5ef8d71c774b3, all 45 hygiene tests, repository-wide check_hygiene.py --check-simp, and git diff --check pass with Python 3.12. Regression coverage includes the reported broken link, valid destinations, missing dependency targets, source line numbers, code/math/escaped examples, citation prose, and unmatched backticks across paragraphs. Full hosted CI is requested; no local Lean build is claimed.

Independent non-author agent /root/review_doc_reference_links approved this commit after source and test review; its paragraph-masking finding was fixed before approval. This is agent review, not human approval. Coordinator review and required CI remain prerequisites for integration.

AI assistance

OpenAI Codex implemented the checker and tests, ran validation, and drafted this PR. A separate non-author Codex agent reviewed the diff. Original implementation credit is preserved.

[karnseth]

Validation update at 127b3e2f34392ea6c95cffdc9ee5ef8d71c774b3: all 45 focused hygiene tests and repository-wide check_hygiene.py --check-simp pass. The broader Python suite ran 393 tests with 21 optional skips and one unrelated existing error: test_cache_handoff.HandoffTests.test_pack_requires_clean_matching_checkout_and_known_platform creates both packed-false and packed-FALSE, which collide on this macOS case-insensitive filesystem. A separate portable-fixture correction is being prepared; this PR does not change cache behavior. Hosted CI is 40864150754.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at 127b3e2f34392ea6c95cffdc9ee5ef8d71c774b3

This is a full review. The author is karnseth, not chris-ai1, so this verdict is not advisory.

Skip check: the PR body mentions an approval by /root/review_doc_reference_links, but no review or comment naming this head is posted on the PR, so I reviewed it.

What changes. One commit on main 21a3641b, touching scripts/check_hygiene.py (+35/−6) and its tests (+100). No Lean source changes.

• New DOC_REFERENCE_RE. It recognizes a line-start reference definition [label]: dest:

  • up to 3 spaces of indent;
  • the destination either bare or in <…>, on the same line or the next;
  • an optional single-line title, then end of line.

  It runs on the fence-masked docstring. The new mask_span call hides every DOC_INLINE_RE match (escapes, math, inline links, code spans) from the scan, and the chars[label_start] != "[" guard skips definitions that start inside those spans. Each destination goes through the existing validate_doc_markdown_target, so the root-qualified/.html/existence/dependency-root rules are reused rather than duplicated. This closes the feat(ExactTriangle): connect prepared matrices to finite adjacency #1616 gap: a target like /Complexity/.../X.lean is now reported.

• Citation escape. A bare alphabetic destination after a citation-shaped label is skipped, which handles prose wrapped as [Key, locator]: if. Explicit <…>, path and URL destinations after a citation label are still checked.

• Code-span regex. Inline code spans may now cross line breaks but stop at a blank line, matching CommonMark. This also tightens check 6, because docstring_citations uses the same regex. The test shows that an unmatched backtick no longer hides later paragraphs.

• Module docstring. The header text for check 4 is updated accurately, including the stated limits: nested containers and indented code are not scanned, and check_docs.py is the backstop.

Checked locally on an exported tree of this head:

• all 45 hygiene unit tests pass;
• the repository-wide check_hygiene.py --check-simp passes;
• the tests are concrete: exact line numbers, both destination forms, the fixture with a missing Mathlib dependency, and the citation-prose cases.

My own probes:

• Correctly ignored: citation labels followed by 3-colorability is…, inline code or math on the next line; a definition inside a list item, which is out of scope as documented.
• Correctly flagged: a bad definition in a declaration docstring (/-- … -/).

Nit (non-blocking). A [foo]: bar line directly after a prose line, with no blank line between, is reported. CommonMark treats it as paragraph text, because a reference definition cannot interrupt a paragraph. This is a conservative false positive, and the error message's "escape \[...\]" hint gives an easy workaround. It could be documented or relaxed later. The paragraph-continuation case does not occur in the current tree. I also confirmed that a line-start [AroraBarak09, Theorem 2]: followed by a line containing only 3-SAT. is reported. That is correct, because CommonMark would make that pair a definition and swallow the prose.

Limits: Python and tooling only; no Lean build is needed. Hosted CI is required.