From d9f952fa6c3b4e3e0bf5d6bbcabcb893e402fa26 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Mon, 27 Apr 2026 22:57:10 -0600 Subject: [PATCH] Reorganize: move non-README docs into docs/ subfolder Standard convention: README.md at root, everything else in docs/. Engine docs/: FFI_DESIGN, FFI_COMPLETENESS, KERNEL_BOUNDARY, NUMERICAL, PHASE1_HISTORY, ZIGZAG_PORT. README.md links updated to docs/. Cross-repo reference in NUMERICAL.md (to topolei's STATUS.md) now includes the relative path `../topolei/docs/STATUS.md`. Co-Authored-By: Claude Opus 4.7 (1M context) --- README.md | 16 ++++++++-------- FFI_COMPLETENESS.md => docs/FFI_COMPLETENESS.md | 0 FFI_DESIGN.md => docs/FFI_DESIGN.md | 0 KERNEL_BOUNDARY.md => docs/KERNEL_BOUNDARY.md | 0 NUMERICAL.md => docs/NUMERICAL.md | 9 +++++---- PHASE1_HISTORY.md => docs/PHASE1_HISTORY.md | 0 ZIGZAG_PORT.md => docs/ZIGZAG_PORT.md | 0 7 files changed, 13 insertions(+), 12 deletions(-) rename FFI_COMPLETENESS.md => docs/FFI_COMPLETENESS.md (100%) rename FFI_DESIGN.md => docs/FFI_DESIGN.md (100%) rename KERNEL_BOUNDARY.md => docs/KERNEL_BOUNDARY.md (100%) rename NUMERICAL.md => docs/NUMERICAL.md (98%) rename PHASE1_HISTORY.md => docs/PHASE1_HISTORY.md (100%) rename ZIGZAG_PORT.md => docs/ZIGZAG_PORT.md (100%) 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