FABRIC-2.md item 5.2: both lemmas described as deliberately oops-flagged
(ROLL semantics, pipeline pm_wf invariant) were actually resolved
2026-08-13, same day, but FABRIC-2.md was never updated to match --
found during a docs-tree maintainability sweep. Corrected both, and
flagged a real untracked finding the pipeline fix surfaced: the Isabelle
model's accuracy num/den fraction pair doesn't correspond to the real
PipelineGlobalMetrics C struct at all. Also reconciled the theory-count
drift (53/54 mid-sweep numbers vs. the actual current 52, matching
proof/COVERAGE.md; proof/FINDINGS.md's own stale "53" flagged but not
fixed, out of this pass's scope).
docs/CLAUDE.md described a docs/Makefile with docs-formal/docs-working/
docs-index/docs-audit targets that doesn't exist anywhere in the tree.
The real build is docs/formal/Makefile with a completely different
target set (vol1/vol2/vol3/books/standalone/doxygen/clean) -- corrected
to match, and noted docs/INDEX.md has no automation and goes stale
between manual triage passes.
doxygen installed on this machine (was missing entirely, blocking the
API-reference build target).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
