915b7b3b68
Some checks failed
Lean Action CI / build (push) Has been cancelled
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>
|
||
|---|---|---|
| .. | ||
| FFI_COMPLETENESS.md | ||
| FFI_DESIGN.md | ||
| INDUCTIVE_TYPES.md | ||
| KERNEL_BOUNDARY.md | ||
| NUMERICAL.md | ||
| PHASE1_HISTORY.md | ||
| REL2_PLAN.md | ||
| ZIGZAG_PORT.md | ||