docs: fix stale proof-suite claims in FABRIC-2.md; correct docs/CLAUDE.md's Makefile pointer

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>

FABRIC-2.md

@@ -232,7 +232,10 @@ and recorded.
   > tactics tried, and the explicit-quantifier form sidesteps that mechanism entirely.
   >
   > **Two genuine, non-tactical bugs found and deliberately left `oops`-flagged rather
-  > than fixed, each documented in place with a full explanation:**
+  > than fixed, each documented in place with a full explanation.** ***Both resolved the
+  > same day, 2026-08-13 — corrected here 2026-08-18, found stale during a docs-tree sweep;
+  > FABRIC-2.md had never been updated to match, even though both `.thy` files themselves
+  > record the fix in place.*** No live `oops` remains anywhere in `proof/` today.
   > - `StarForth_Stack_Words.thy`'s `roll_two_is_rot` — a three-way inconsistency between
   >   `forth_roll_def`'s own index arithmetic (off-by-one against what the lemma expects),
   >   the lemma's own expected ROT-equivalent output, and the real C `stack_word_roll`
@@ -240,13 +243,30 @@ and recorded.
   >   bottom-indexed convention ("1-indexed from bottom: n=1 moves bottom item to top")
   >   matching neither. Not a proof-script issue — a genuine open question about what
   >   `ROLL` is supposed to do, needing a decision before it can be closed either
-  >   direction.
+  >   direction. ~~Genuine open question.~~ **RESOLVED 2026-08-13**: `forth_roll_def`
+  >   rewritten to match the real C's bottom-indexed convention exactly (traced from
+  >   `stack_words.c:291-320`, its own comment is explicit: "1-indexed from bottom: n=1
+  >   moves bottom item to top") — a deliberately different operation from the
+  >   standard/gforth "count from top" ROLL, not a bug in either the C or the original
+  >   lemma's expectation, just two different definitions of ROLL that needed reconciling
+  >   toward the real one. `roll_two_is_rot` now proves.
   > - `StarForth_Loop4_Pipeline.thy`'s `pm_record_hit_preserves_wf`/
   >   `pm_record_miss_preserves_wf` — `pm_wf` only requires `pm_last_accuracy_den > 0`
   >   when `pm_prefetch_attempts > 0`; both operations increment `attempts` from 0 to 1
   >   without ever having required `den > 0` beforehand, so the postcondition needs
   >   something the precondition never guaranteed. A genuine invariant-maintenance gap in
-  >   `pm_wf`'s own definition, not fixed here.
+  >   `pm_wf`'s own definition, not fixed here. **RESOLVED 2026-08-13**: both lemmas gained
+  >   an explicit `pm_last_accuracy_den pm > 0` hypothesis, matching the precondition to
+  >   what the postcondition actually needs — the invariant-maintenance gap this bullet
+  >   describes, closed by stating it rather than by strengthening `pm_wf` itself. **A
+  >   deeper, previously untracked issue surfaced by this fix, still open**: the model's
+  >   `pm_last_accuracy_num`/`pm_last_accuracy_den` fraction pair does not correspond to the
+  >   real C struct at all — `PipelineGlobalMetrics` (`include/vm.h`) has a single `double
+  >   last_checked_accuracy` field, no num/den pair anywhere (confirmed against
+  >   `src/vm_bootstrap.c:290-295`, `src/vm_time.c:412-413,627-628`). Flagged in the `.thy`
+  >   file itself as its own separate future task ("a full field-level pass over
+  >   `pipeline_metrics_state`"), not attempted as a side effect of this fix, and not
+  >   tracked anywhere outside that one code comment until now.
   >
   > Toolchain: `/home/rajames/CLionProjects/Isabelle2011-1` now genuinely runs
   > Isabelle2025-2 (old 2011 install preserved as `Isabelle2011-1.old`). Gitea Actions CI
@@ -311,6 +331,13 @@ and recorded.
   > structurally different DF usage — dispatch reassignment via a stored pointer, not a
   > plain value). Full suite: 54 theories, green.
   >
+  > **Theory count reconciled 2026-08-18** — this entry's own running count (53 here, then
+  > 54 two paragraphs up) reflects the suite's state at each point in this multi-session
+  > sweep, not a final figure; neither is current. **The actual, current count is 52** (`proof/`
+  > file count matches `proof/ROOT`'s registration exactly, verified directly, no orphans, no
+  > gaps) — matching `proof/COVERAGE.md`'s own count. `proof/FINDINGS.md` still says 53;
+  > that file was not corrected here (out of this pass's scope; flagged, not fixed).
+  >
   > **Continued, commit `6f59e4f`.** IS/DEFER@ (`StarForth_Defer_Words.thy`) now modelled
   > end to end too, sidestepping the FIND-family name-resolution gap (still itself
   > unmodelled everywhere in this suite) the same way `physics_freeze_words.c`'s

docs/CLAUDE.md

@@ -42,15 +42,33 @@ is audience and stability, not quality.
 
 ## Makefile Targets
 
+**Corrected 2026-08-18** — this section previously described a `docs/Makefile` with
+`docs-formal`/`docs-working`/`docs-index`/`docs-audit`/`docs`/`docs-clean` targets. That file
+does not exist and none of those targets exist anywhere in the tree. The real build lives one
+level down, at `docs/formal/Makefile`, with a different target set entirely:
+
 ```
-make docs-formal     — build all three LaTeX volumes → PDFs in formal/build/
-make docs-working    — render working/ markdown to HTML (optional, low priority)
-make docs-index      — generate docs/INDEX.md inventory of all doc files
-make docs-audit      — list files tagged OBSOLETE or SUPERSEDED in INDEX.md
-make docs            — run docs-formal + docs-index
-make docs-clean      — remove formal/build/ artifacts
+# Run from docs/formal/
+
+make            — everything: all three volumes + books + standalone docs + doxygen
+make vols       — vol1 + vol2 + vol3 (the three-volume LaTeX set)
+make vol1       — Volume I only
+make vol2       — Volume II only
+make vol3       — Volume III only
+make books      — dev-guide + user-guide + cookbook
+make standalone — experiments + proofs + ssrn + patent (standalone LaTeX docs)
+make doxygen    — API reference PDF (requires the `doxygen` binary installed;
+                  runs doxygen → fix-doxygen-unicode.py → doxygen/latex → PDF)
+make clean      — remove build artifacts
 ```
 
+`docs/working/` has no build step of its own (no HTML rendering target exists) — it's read
+directly as markdown. `docs/INDEX.md` exists but is maintained manually, following this
+file's own Phase 1 triage process below — there is no `docs-index`/`docs-audit` automation
+that generates or checks it; treat `INDEX.md` as something a triage pass produces by hand,
+and expect it to go stale between passes (confirmed stale as of this correction — check its
+own date against `git log -1` before trusting it).
+
 ---
 
 ## Phase 1: Triage (DO THIS FIRST)