diff --git a/README.md b/README.md
index a3d34cb..5b21ac8 100644
--- a/README.md
+++ b/README.md
@@ -45,15 +45,15 @@ lake build
 
 ## Reference
 
-- `FFI_DESIGN.md` — C ABI contract between Lean and the Rust kernel.
-- `FFI_COMPLETENESS.md` — per-function axiom audit.
-- `KERNEL_BOUNDARY.md` — what this delivers in unmodified Lean 4 vs.
+- `docs/FFI_DESIGN.md` — C ABI contract between Lean and the Rust kernel.
+- `docs/FFI_COMPLETENESS.md` — per-function axiom audit.
+- `docs/KERNEL_BOUNDARY.md` — what this delivers in unmodified Lean 4 vs.
   what would need upstream Lean kernel work.
-- `NUMERICAL.md` — numerical implementation principles.
-- `PHASE1_HISTORY.md` — original transport/composition formalisation
+- `docs/NUMERICAL.md` — numerical implementation principles.
+- `docs/PHASE1_HISTORY.md` — original transport/composition formalisation
   plan (archived; Phase 1 closed; preserved as methodology template
   for future phases).
-- `ZIGZAG_PORT.md` — step-by-step Lean port plan for the n-category
+- `docs/ZIGZAG_PORT.md` — step-by-step Lean port plan for the n-category
   combinatorial engine (Phase 2+ higher-cell backend).  Lands here
   in the engine.  **Read the cascade caveat at the top before
   editing**: changes in the ported zigzag layer cascade to the
@@ -64,5 +64,5 @@ lake build
 ## Used by
 
 - [`max/topolei`](../topolei) — the cells-spec workspace interface,
-  built on this engine.  See its `cells-spec.md` and `STATUS.md` for
-  the application-side picture.
+  built on this engine.  See its `docs/cells-spec.md` and
+  `docs/STATUS.md` for the application-side picture.
diff --git a/FFI_COMPLETENESS.md b/docs/FFI_COMPLETENESS.md
similarity index 100%
rename from FFI_COMPLETENESS.md
rename to docs/FFI_COMPLETENESS.md
diff --git a/FFI_DESIGN.md b/docs/FFI_DESIGN.md
similarity index 100%
rename from FFI_DESIGN.md
rename to docs/FFI_DESIGN.md
diff --git a/KERNEL_BOUNDARY.md b/docs/KERNEL_BOUNDARY.md
similarity index 100%
rename from KERNEL_BOUNDARY.md
rename to docs/KERNEL_BOUNDARY.md
diff --git a/NUMERICAL.md b/docs/NUMERICAL.md
similarity index 98%
rename from NUMERICAL.md
rename to docs/NUMERICAL.md
index 4daeec6..d72e6b0 100644
--- a/NUMERICAL.md
+++ b/docs/NUMERICAL.md
@@ -109,10 +109,11 @@ enforces three properties:
    implementations for axiom-stated behaviors
    (`@[extern "topolei_cubical_eval"] opaque cubicalEval : CEnv → CTerm → CVal`).
    Each Rust function's behavior is specified by a Lean axiom it
-   must satisfy (e.g., `eval_var` / `eval_lam` / … in `Cubical/Eval.lean`,
-   or `readback_vneu` / … in `Cubical/Readback.lean`).  Step-level
-   axioms are derived from the eval/readback contract via the Week 7
-   bridge — see `STATUS.md`.
+   must satisfy (e.g., `eval_var` / `eval_lam` / … in
+   `CubicalTransport/Eval.lean`, or `readback_vneu` / … in
+   `CubicalTransport/Readback.lean`).  Step-level axioms are derived
+   from the eval/readback contract via the Week 7 bridge — see
+   `STATUS.md` in the topolei repo (`../topolei/docs/STATUS.md`).
 
 3. **IO tagging.** Any effect (GPU dispatch, memory allocation,
    timing, parallelism) is wrapped in `IO` so it cannot leak into
diff --git a/PHASE1_HISTORY.md b/docs/PHASE1_HISTORY.md
similarity index 100%
rename from PHASE1_HISTORY.md
rename to docs/PHASE1_HISTORY.md
diff --git a/ZIGZAG_PORT.md b/docs/ZIGZAG_PORT.md
similarity index 100%
rename from ZIGZAG_PORT.md
rename to docs/ZIGZAG_PORT.md