diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc
index 43e63e5a..45cdcaec 100644
--- a/docs/EXPLAINME.adoc
+++ b/docs/EXPLAINME.adoc
@@ -73,7 +73,7 @@ This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), a
 | Technology | Role in Hypatia | Also Used In
 
 | *Idris2 ABI* (hyperpolymath standard)
-| `src/abi/` — formal specs for GraphQL, gRPC, REST with dependent type proofs; `ffiReturnsApiResponse` proof in `FFI.idr`
+| `src/Hypatia/ABI/` — formal specs for GraphQL, gRPC, REST with dependent type proofs; `ffiReturnsApiResponse` proof in `FFI.idr`
 | gossamer (`gossamer/src/interface/abi/`), burble (`burble/src/Burble/ABI/`), verisimdb, proven, typed-wasm — every repo with an FFI layer
 
 | *Zig FFI* (hyperpolymath standard)
@@ -116,7 +116,7 @@ This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), a
 | `lib/self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery
 | `lib/neural/` | 5 networks (graph-of-trust, moe, lsm, esn, rbf) + coordinator
 | `lib/vcl/` | VCL client, file executor, query functions
-| `src/abi/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI)
+| `src/Hypatia/ABI/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI, RuleEngine, Gen)
 | `ffi/zig/src/` | 7 C-compatible exported functions
 | `adapters/ cli/ data/ fixer/ integration/` | Rust workspace (root crates)
 | `proofs/agda/` | Formal verification of safety triangle correctness
diff --git a/docs/operations/prover-wars-integration.adoc b/docs/operations/prover-wars-integration.adoc
index 82dfc9cd..5e9bcb3c 100644
--- a/docs/operations/prover-wars-integration.adoc
+++ b/docs/operations/prover-wars-integration.adoc
@@ -36,7 +36,7 @@ the head-to-head statistics from each prover's results corpus.
     `data/prover-wars/{challenge,result,winner}/*.jsonl` (proposed
     layout — needs confirmation with the VeriSimDB owner).
 
-  * *ABI* — Idris2 ABI definitions in `src/abi/` already export
+  * *ABI* — Idris2 ABI definitions in `src/Hypatia/ABI/` already export
     `ProofObligation` types. Prover Wars integration adds
     `ProofChallenge` + `ProofResult` to the ABI so cross-language
     consumers see consistent shapes.
diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc
index eab72e3e..dddf4b28 100644
--- a/docs/proofs/gap-analysis.adoc
+++ b/docs/proofs/gap-analysis.adoc
@@ -76,7 +76,7 @@ CI invocation does not.
 This is the one proof currently gated on every push to main and on a
 weekly Monday 04:00 UTC schedule. Pattern to replicate.
 
-==== Idris 2 type library (not proofs) — `+src/abi/+`, `+verify/src/+`
+==== Idris 2 type library (not proofs) — `+src/Hypatia/ABI/+`, `+verify/src/+`
 
 `+Types.idr+`, `+RuleEngine.idr+`, `+PipelineState.idr+` —
 dependent-type library code used by the ABI. Type-checked locally; not
diff --git a/docs/quickstart/llm-warmup-dev.adoc b/docs/quickstart/llm-warmup-dev.adoc
index 49adccac..4af9f66d 100644
--- a/docs/quickstart/llm-warmup-dev.adoc
+++ b/docs/quickstart/llm-warmup-dev.adoc
@@ -114,9 +114,10 @@ revert
 |`+tools/cii-registrar+` |CII Best Practices registration
 |===
 
-==== Idris2 ABI (src/abi/)
+==== Idris2 ABI (src/Hypatia/ABI/)
 
-5 modules with dependent type proofs:
+7 modules with dependent type proofs. The `+.ipkg+` files that build them
+live in `+src/abi/+` and set `+sourcedir = ".."+`:
 
 [width="100%",cols="40%,60%",options="header",]
 |===
@@ -132,7 +133,11 @@ health)
 
 |`+FFI.idr+` |GADT constructors for C ABI functions
 
-|`+hypatia-abi.ipkg+` |Package definition
+|`+RuleEngine.idr+` |Rule-evaluation types, safety triangle, dispatch proofs
+
+|`+Gen.idr+` |Wire-enum generator for the Zig and Rust connector enums
+
+|`+src/abi/hypatia-abi.ipkg+` |Package definition
 |===
 
 ==== Zig FFI (ffi/zig/)
diff --git a/docs/quickstart/llm-warmup-user.adoc b/docs/quickstart/llm-warmup-user.adoc
index f4fa2c03..677e255f 100644
--- a/docs/quickstart/llm-warmup-user.adoc
+++ b/docs/quickstart/llm-warmup-user.adoc
@@ -44,7 +44,7 @@ OutcomeTracker (Bayesian feedback loop)
 |`+lib/safety/+` |Rate limiter, quarantine, batch rollback
 |`+adapters/+` |Rust adapter crate
 |`+cli/+` |Rust CLI crate
-|`+src/abi/+` |Idris2 ABI definitions
+|`+src/Hypatia/ABI/+` |Idris2 ABI definitions (built by `+src/abi/*.ipkg+`)
 |`+ffi/zig/+` |Zig FFI bridge (7 functions)
 |`+mix.exs+` |Elixir project config
 |`+Cargo.toml+` |Rust workspace config
diff --git a/docs/quickstart/user.adoc b/docs/quickstart/user.adoc
index 1035eeb4..4d228d03 100644
--- a/docs/quickstart/user.adoc
+++ b/docs/quickstart/user.adoc
@@ -40,7 +40,7 @@ toc::[]
 
 Optional (for ABI/FFI layers):
 
-* Idris2 >= 0.7.0 (for ABI definitions in `src/abi/`)
+* Idris2 >= 0.7.0 (for the ABI definitions in `src/Hypatia/ABI/`)
 * Zig >= 0.13.0 (for FFI bridge in `ffi/zig/`)
 
 == Clone and build
diff --git a/docs/wiki-pages/Architecture.md b/docs/wiki-pages/Architecture.md
index f9db4efb..3ca7424b 100644
--- a/docs/wiki-pages/Architecture.md
+++ b/docs/wiki-pages/Architecture.md
@@ -99,7 +99,7 @@ All `/api/*` endpoints are loopback-only by default; set `HYPATIA_API_BEARER_TOK
 
 Foreign callers reach Hypatia through:
 
-- **Idris2 ABI** (`src/abi/`) — `Types.idr`, `GraphQL.idr`, `GRPC.idr`, `REST.idr`, `FFI.idr` (with dependent-type proofs)
+- **Idris2 ABI** (`src/Hypatia/ABI/`) — `Types.idr`, `GraphQL.idr`, `GRPC.idr`, `REST.idr`, `FFI.idr`, `RuleEngine.idr` (with dependent-type proofs)
 - **Zig FFI** (`ffi/zig/`) — 7 exported C functions (`hypatia_health_check`, `hypatia_scan_repo`, `hypatia_dispatch`, `hypatia_record_outcome`, `hypatia_force_learning_cycle`, `hypatia_get_confidence`, `hypatia_dispatch_strategy`)
 
 ## Component table
diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index 3604b0d5..e99e2e47 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -18,8 +18,10 @@ convenient
 ==== Existing Proofs (pre-2026-04-04)
 
 NOTE: These tables deliberately carry no line-count column. Hand-maintained LOC
-figures drift silently, nothing consumes them, and every one of the twenty
-previously recorded here had gone wrong. Use `+wc -l+` on the paths below.
+figures drift silently, nothing consumes them, and sixteen of the twenty
+previously recorded here were wrong — some by more than double. Use `+wc -l+`
+on the paths below. (The four that were right were all tilde-approximations
+that happened to land within two lines; the column was still not worth keeping.)
 
 [width="100%",cols="28%,14%,42%,16%",options="header",]
 |===