docs: correct Idris2 region-linearity theorem names (#115)

The recent README/ROADMAP/EXPLAINME rewrite used
`regionSafetyTheorem`/`noGCTheorem` for two theorems in `src/formal/`,
but the actual names are `regionSafetyExtract`/`noGCExtract` (in
`Ephapax/Formal/RegionLinear.idr` at lines 139 and 151 respectively).
EXPLAINME also cited non-existent paths (`NoEscape.idr`,
`RegionSafety.idr`, `NoGC.idr`, `Orthogonality.idr`) — all four theorems
actually live in `RegionLinear.idr`.

Fixed in README.adoc, ROADMAP.adoc, EXPLAINME.adoc.

Companion wiki fix (Home.md, Region-calculus.md, Proof-status.md) pushed
separately to the wiki repo.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

EXPLAINME.adoc

@@ -245,16 +245,16 @@ properties of the region-linear calculus:
 | Theorem | Where
 
 | `noEscapeTheorem`
-| `src/formal/Ephapax/Formal/NoEscape.idr`
+| `src/formal/Ephapax/Formal/RegionLinear.idr:129`
 
-| `regionSafetyTheorem`
-| `src/formal/Ephapax/Formal/RegionSafety.idr`
+| `regionSafetyExtract`
+| `src/formal/Ephapax/Formal/RegionLinear.idr:139`
 
-| `noGCTheorem`
-| `src/formal/Ephapax/Formal/NoGC.idr`
+| `noGCExtract`
+| `src/formal/Ephapax/Formal/RegionLinear.idr:151`
 
 | `orthogonalityLemma`
-| `src/formal/Ephapax/Formal/Orthogonality.idr`
+| `src/formal/Ephapax/Formal/RegionLinear.idr:164`
 
 | `splitLinearCoverage`
 | `src/formal/Ephapax/Formal/Qualifier.idr` (PR #85, 2026-05-19) —

README.adoc

@@ -239,7 +239,7 @@ Two Idris2 developments:
   markers retained for documented Idris2 0.8.0 SCT limits.
 
 * **`src/formal/`** — region-linearity theorems on the type side:
-  `noEscapeTheorem`, `regionSafetyTheorem`, `noGCTheorem`,
+  `noEscapeTheorem`, `regionSafetyExtract`, `noGCExtract`,
   `orthogonalityLemma`, plus `splitLinearCoverage` generalising
   the non-diminishment property (PR #85). All four headline theorems
   complete with **zero unsafe patterns**.

ROADMAP.adoc

@@ -123,8 +123,8 @@ Separate Idris2 development proving structural properties of the
 region-linear calculus:
 
 * `noEscapeTheorem` — region references cannot leak past their scope
-* `regionSafetyTheorem` — typed expressions don't dereference freed regions
-* `noGCTheorem` — bulk deallocation at region exit is sound
+* `regionSafetyExtract` — typed expressions don't dereference freed regions
+* `noGCExtract` — bulk deallocation at region exit is sound
 * `orthogonalityLemma` — the linear / region disciplines compose
 * `splitLinearCoverage` (PR #85, 2026-05-19) — generalises
   `nonDiminishment` from head-position to all linear bindings