Detailed three-phase plan for the next stratum past REL1:
1. CType.interval primitive (1-2d) — the river-bed under every
dim-flowing computation. Promotes .dimExpr from .univ
placeholder to .interval typing.
2. Bridge.lean (Eq ↔ Path interop, 3-5d) — the ferry between
Lean's discrete equality and the embedded cubical Path.
Default CubicalEmbed instances for Bool, Nat, List, Prod;
forward bridge always available, backward restricted to
neutral-free paths in REL2.0 (full Glue NbE deferred to
REL2.1).
3. paideia K7 literal cubical encoding (5-10d) — the carrying
load. Replaces MathPath p₀ p₁ with a CTerm-typed
Path between two embedded MasteryProvenance traces.
Closes engine issue #1 with the originating use case.
Covers acceptance criteria, risk register, sequencing graph
(engine → topolei → paideia, no cycle), Rust ABI bump 2→3,
post-REL2 deferral list (REL2.1 Glue NbE / pointwise dist,
REL3 numerical layer, REL3+ higher cells, REL4 GPU/interaction).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Filed against issue #1 (paideia K7 cubical-Path encoding blocker).
Generalised scope: full HIT support — point + path constructors with
boundary partial-element systems, multi-param schemas, recursive ctor
args. CTypeSchema/CtorSpec/CTypeArg embedded in the mutual inductive
block alongside CType/CTerm. New constructors: CType.ind,
CTerm.{dimExpr, ctor, indElim}, CVal.vctor, CNeu.nIndElim.
Tag layout frozen for REL1; Rust ABI bumps 1→2. Topolei migration
surveyed and documented (§9.1) — ~150–250 lines across DecEq, Trace,
TraceAt, FluxR; Path.lean and EML/Cubical.lean unaffected.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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/<name>.
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) <noreply@anthropic.com>
