docs: correct 8 prose sites claiming src/abi/ holds the Idris2 modules

[hyperpolymath]

The half of the defect a filename regex cannot see

PR #835 corrected every reference naming a specific src/abi/*.idr file —
8 hits, driven down to 1 (past-tense history). But a .idr-filename regex is
blind to the other half of the same defect: prose that names the directory and
asserts it contains the Idris2 ABI. Those claims are just as false, and #835
left all eight standing.

src/abi/ holds exactly three files:

src/abi/README.adoc
src/abi/hypatia-abi-gen.ipkg
src/abi/hypatia-abi.ipkg

The modules live in src/Hypatia/ABI/. The ipkg sets sourcedir = "..", which
is why build lines legitimately still name src/abi/ — and why a naive
search-and-replace across the path would have broken the build documentation.

Corrected — 8 sites, each read in context first

File	Was
docs/EXPLAINME.adoc:76	``src/abi/ — formal specs for GraphQL, gRPC, REST with dependent type proofs
docs/EXPLAINME.adoc:119	`src/abi/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI)
docs/operations/prover-wars-integration.adoc:39	Idris2 ABI definitions in src/abi/ already export
docs/proofs/gap-analysis.adoc:79	+src/abi/+`, `+verify/src/+
docs/quickstart/llm-warmup-dev.adoc:117	==== Idris2 ABI (src/abi/)
docs/quickstart/llm-warmup-user.adoc:47	`+src/abi/+` | Idris2 ABI definitions
docs/quickstart/user.adoc:43	Idris2 >= 0.7.0 (for ABI definitions in src/abi/)
docs/wiki-pages/Architecture.md:102	**Idris2 ABI** (src/abi/) — Types.idr, GraphQL.idr, …

Two stated counts were wrong in the same sentences and are fixed with them.
The dev warmup said "5 modules" and EXPLAINME/Architecture enumerated five;
there are seven live modules — RuleEngine.idr and Gen.idr (added by
#120) were missing from every list.

Correcting an overclaim #835 introduced

The NOTE #835 added to verification/PROOF-STATUS.adoc read "every one of the
twenty previously recorded here had gone wrong." That is itself false.
Sixteen were wrong; four tilde-approximations landed within two lines:

File	documented	actual
PageRankInvariants	~120	120
ESNSpectralScaling	~145	144
BayesianUpdate	~190	188
ParserTotality	~190	191

The conclusion is unchanged — 16/20 wrong, several by more than double, and
nothing consumed the column — but a false count inside a note about false counts
is not acceptable in either direction. The NOTE now says sixteen and states what
the other four were.

Deliberately NOT changed — each verified correct as written

• verify-proofs.yml paths filters, Justfile, stapeln.toml, every
  idris2 --build src/abi/*.ipkg line — src/abi/ is genuinely where the
  packages live.
• docs/DEBT-REGISTER.adoc, docs/proofs/HANDOVER-neural-convergence.adoc,
  test/unified-api-adapter-contract_test.exs — past-tense records of the
  deleted duplicates. Correct precisely because they name the old path.
• lib/rules/structural_drift.ex:1130 — quotes gitbot-fleet's INTENT file
  as measured evidence for an SD022 defect. Not a claim about this repo.
• .claude/CLAUDE.md's "the two .ipkg files" — accurate. There are two in
  src/abi/; the third Idris2 package is verify/hypatia-verify.ipkg,
  elsewhere.

Acceptance

git grep -n 'src/abi/' -- . ':!data/' | grep -iE 'idris|proof|\.idr|module'

→ 20 hits, every one an ipkg/build reference, past-tense history, or the
src/abi/README.adoc title. No false claim survives.

All seven edited AsciiDoc files re-render clean under
asciidoctor --failure-level=WARN.

Refs #816.

🤖 Generated with Claude Code

https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 9c9be321-e0c1-4fc5-94dd-ecbdf009e1ec

📥 Commits

Reviewing files that changed from the base of the PR and between 1b2e66e and bfb6b80.

📒 Files selected for processing (8)

• docs/EXPLAINME.adoc
• docs/operations/prover-wars-integration.adoc
• docs/proofs/gap-analysis.adoc
• docs/quickstart/llm-warmup-dev.adoc
• docs/quickstart/llm-warmup-user.adoc
• docs/quickstart/user.adoc
• docs/wiki-pages/Architecture.md
• verification/PROOF-STATUS.adoc

 __________________
< I see dead code. >
 ------------------
  \
   \   \
        \ /\
        ( )
      .( o ).

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}