# REL2_PLAN.md — Interval, Bridge, K7 Cubical Encoding *Drafted 2026-04-30, on `Dev_REL1`. The detailed engineering plan for advancing both the implementation and the project's Eulerian abstractions one stratum past REL1. Three coordinated phases across three repos (`cubical-transport-hott-lean4`, `topolei`, `paideia`), sequenced to land in a single merge train.* --- ## 0. Eulerian framing (why this trio) Three poetic-and-applicable abstractions converge on this work: - **River bed** — the **interval** `𝕀` as a first-class type. Today `.dimExpr r` types as the placeholder `.univ`; promoting interval to a CType primitive gives every dim-flowing computation real semantic ground. Without a river bed, paths flow over an unspecified medium. - **Ferry** — the **`Eq ↔ Path` bridge**. Lean's discrete-equality river and the embedded cubical-path river run in parallel. The ferry lets payload (Mathlib lemmas, decidable-equality witnesses) cross between them in either direction. - **Carrying load** — **paideia K7** as a literal cubical `Path` between two `MasteryProvenance` traces. The originating issue (#1) filed against this repo. REL1 gave us inductive types in the cubical universe; REL2 makes K7 an actual passenger on the ferry. Each phase advances both registers simultaneously: the metaphor lands *because* the implementation lands. --- ## 1. Phase 1 — `CType.interval` primitive **Repo:** `cubical-transport-hott-lean4` (+ topolei follow-up). **Estimated effort:** 1–2 days. **Branch:** continue on `Dev_REL1`. ### 1.1 Goal Promote the cubical interval to a first-class CType. After this phase, `.dimExpr r : .interval` is a real typing judgement, not a `.univ` placeholder. ### 1.2 Engine changes | File | Change | |------|--------| | `CubicalTransport/Syntax.lean` | Add `\| interval : CType` to the mutual block (tag 6, after `.ind`). Bump tag-layout doc in §6 of `INDUCTIVE_TYPES.md`. | | `CubicalTransport/Subst.lean` | `.interval` arms in `CType.substDim` / `substDimExpr` (no recursion). Reduction lemmas `substDim_interval`, `substDimExpr_interval` (both `rfl`). | | `CubicalTransport/DimLine.lean` | `.interval` arms in `CType.dimAbsent` (always `true`); `CType.substDim_absent_aux`; `CType.substDimExpr_absent_aux`; `CType.dimAbsent_after_substDim_aux`; `CType.substDim_comm_aux`. All trivial. | | `CubicalTransport/Typing.lean` | Replace `HasType.dimExpr : HasType Γ (.dimExpr r) .univ` with `… .interval`. Update `HasType.weaken_core`'s `\| dimExpr` arm. | | `CubicalTransport/Inductive.lean` | Add ergonomic alias `CType.intervalC : CType := .interval`. | | `CubicalTransport/TransportLaws.lean` | Optional: `eval_transp_interval_const : eval env (.transp i .interval φ t) = eval env t` — derived corollary of `eval_transp_const` since `.interval` is dim-absent. | ### 1.3 Rust kernel changes (`native/cubical/src/`) | File | Change | |------|--------| | `tags.rs` | `pub const TY_INTERVAL: u32 = 6;` | | `subst.rs` | `TY_INTERVAL` arm in `ctype_subst_dim` and `ctype_subst_dim_expr` — return self with `retain`. | | `dim_absent.rs` | `TY_INTERVAL` arm in `ctype_absent` — return `true`. | | `include/topolei_cubical.h` | Bump `TOPOLEI_FFI_ABI_VERSION` 2 → 3. | ### 1.4 Topolei follow-up `Topolei/Cubical/DecEq.lean`'s `CType.beq` is exhaustive — add an `.interval` arm: ```lean \| .interval, .interval => true ``` Plus `\| .interval => by simp [CType.beq]` in `CType.beq_refl`. Commit on topolei `Dev_REL1`. ### 1.5 Tests - `CubicalTransport/FFITest.lean`: smoke test `cvalSummary (eval .nil (.dimExpr (.var ⟨"i"⟩)))` ≡ `"vdimExpr ..."` (existing test, still passes). - New `EvalTest.lean` arm: `HasType.dimExpr` constructs a witness at `.interval`. - All existing 74/74 tests must still pass. ### 1.6 Acceptance criteria - `lake build` clean across all 30+ jobs. - `./.lake/build/bin/cubical-test` reports 74/74 + new arm = 75/75. - Engine builds on its own; topolei `Dev_REL1` rebuilds with the one-line `DecEq.lean` patch. - `INDUCTIVE_TYPES.md` §6 tag table updated; doc note in §11.4 marks the dimExpr-typing approximation as resolved. --- ## 2. Phase 2 — `Bridge.lean` (`Eq ↔ Path` interop) **Repo:** `cubical-transport-hott-lean4`. **Estimated effort:** 3–5 days. **Branch:** `Dev_REL1` (continues from Phase 1). **Blocked by:** Phase 1 (instances need interval-typed dim args for path constructors). ### 2.1 Goal Provide a typeclass-mediated bridge between Lean's `Eq` and embedded cubical `Path`, with default instances for canonical types (`Bool`, `Nat`, `List`, products), plus the two principal bridge directions. ### 2.2 The `CubicalEmbed` typeclass ```lean class CubicalEmbed (α : Type) where ctype : CType toCTerm : α → CTerm fromCTerm : CTerm → Option α roundtrip : ∀ a, fromCTerm (toCTerm a) = some a toCTerm_typed : ∀ a, HasType .nil (toCTerm a) ctype ``` Per-instance bookkeeping: `roundtrip` is by structural recursion; `toCTerm_typed` follows from `HasType.ctor`'s minimal-viable rule (REL1) — no per-arg coherence needed at this level. ### 2.3 Default instances | Type | Schema | Notes | |------|--------|-------| | `Bool` | `boolSchema` | `toCTerm true = trueC`, `false = falseC`. | | `Nat` | `natSchema` | `toCTerm n = natLit n` (tower of `succC`s). | | `List α [CubicalEmbed α]` | `listSchema [α.ctype]` | folds via `consC`/`nilC`. | | `α × β [CubicalEmbed α] [CubicalEmbed β]` | (uses Σ via `CType.sigma`) | `toCTerm (a,b) = .pair (toCTerm a) (toCTerm b)`. | | `Option α [CubicalEmbed α]` | (encode as `α + Unit` schema, REL2.1) | deferred. | ### 2.4 Bridge directions **Forward (always available):** ```lean def Eq.toPath {α} [CubicalEmbed α] {a b : α} (h : a = b) : CTerm := .plam (DimVar.mk "$eq2path") (CubicalEmbed.toCTerm a) -- Constant path; b reduces to a by h, so endpoints match. theorem Eq.toPath_typed {α} [CubicalEmbed α] {a b : α} (h : a = b) : HasType .nil (Eq.toPath h) (.path (CubicalEmbed.ctype α) (CubicalEmbed.toCTerm a) (CubicalEmbed.toCTerm b)) ``` **Backward (decidable types):** ```lean theorem Path.toEq {α} [CubicalEmbed α] [DecidableEq α] {a b : α} (p : CTerm) (hp : HasType .nil p (.path (CubicalEmbed.ctype α) (CubicalEmbed.toCTerm a) (CubicalEmbed.toCTerm b))) : a = b ``` **Proof sketch:** by `decEq a b` case analysis. In the negative case, derive `False` from path-endpoint coherence: a path between two `toCTerm`-distinct constructor values cannot exist, by readback + `CTerm.noConfusion`. **Restriction in REL2.0:** Backward bridge is restricted to *neutral- free* paths in the first cut. A non-canonical path produced by Glue or transport may not directly close `Path.toEq`; defer to REL2.1 once the Glue NbE story is fully discharged (sibling open work). Document the restriction in the docstring. **Prop-level coincidence:** ```lean theorem Path_iff_Eq_of_Prop {P : Prop} (a b : P) : a = b ↔ True := ⟨fun _ => trivial, fun _ => proof_irrel a b⟩ -- Trivial bijection via proof irrelevance. ``` ### 2.5 Module layout `CubicalTransport/Bridge.lean` (new): - §1 `CubicalEmbed` class + universe-polymorphic instances skeleton. - §2 Default instances (`Bool`, `Nat`, `List`, `Prod`). - §3 Forward bridge (`Eq.toPath` + typing). - §4 Backward bridge (`Path.toEq` for decidable types). - §5 Prop-level coincidence. - §6 Round-trip lemmas + composition theorems. Re-export from `CubicalTransport.lean`. ### 2.6 Tests `BridgeTest.lean` (new): - `Eq.toPath rfl |> readback` round-trips through a constant `.plam`. - `Path.toEq` on the constant path returns `rfl`. - `roundtrip` per-instance for Bool/Nat/List Bool/(Nat × Bool). - A property-style test: 100 random `Bool`/`Nat` values, all round-trips succeed. ### 2.7 Doc updates - `KERNEL_BOUNDARY.md §2.6` from "planned" to "landed in `Bridge.lean`". - New `docs/EULERIAN.md` (optional but recommended): the river-bed / ferry / carrying-load metaphor with concrete Lean counterparts. Keep under 200 lines; this is the project's poetic record. ### 2.8 Acceptance criteria - All instances compile and `roundtrip`/`toCTerm_typed` proofs go through. - `Path.toEq` proven for `Bool`, `Nat`, `List Bool`, `Nat × Bool`. - `BridgeTest.lean` reports new arms passing alongside the existing smoke + property suites. - `KERNEL_BOUNDARY.md` updated. --- ## 3. Phase 3 — paideia K7 literal cubical encoding **Repo:** `paideia` (separate repo; depends on engine + topolei). **Estimated effort:** 5–10 days. **Branch:** new `Dev_REL1` on paideia. **Blocked by:** Phase 1 (interval), Phase 2 (Bridge), engine `Dev_REL1` merged or available as a path-require. ### 3.1 Goal Replace the discrete-shadow `MathPath p₀ p₁` with a `CTerm`-typed `Path (embed MasteryProvenance) (embed p₀) (embed p₁)`. Closes issue #1 in `max/cubical-transport-hott-lean4`. ### 3.2 Survey day (1 day) Read paideia's existing `Foundation/K7Cubical.lean`, the locations of `KnowledgeNode` and `MasteryProvenance`, and every consumer of `MathPath`. Catalogue: - `KnowledgeNode`'s record fields (CubicalEmbed instance shape). - `MasteryProvenance`'s exact definition (likely `Trace KnowledgeNode` ≡ list). - All `MathPath` call sites (the migration surface). - K7's external API (`init`, `step`, `lift`, anything else). ### 3.3 New module: `Paideia/Foundation/MasteryEncoding.lean` ```lean import CubicalTransport.Bridge import CubicalTransport.Inductive instance : CubicalEmbed KnowledgeNode := { ... } -- via a paideia-local schema for the record (or via composition -- of more primitive instances if KnowledgeNode is structured). instance : CubicalEmbed MasteryProvenance := { ctype := .ind listSchema [CubicalEmbed.ctype KnowledgeNode] toCTerm := fun mp => mp.foldr (fun n acc => consC _ (CubicalEmbed.toCTerm n) acc) (nilC _) fromCTerm := … roundtrip := by structural induction on the trace toCTerm_typed := by structural induction + HasType.ctor } ``` If `KnowledgeNode` carries `Float` fields, encode `Float` opaquely as `.var ` for the first cut; flag it in a TODO; revisit if numerical reasoning at the cubical level becomes necessary (REL3+). ### 3.4 K7 rewrite: `Paideia/Foundation/K7Cubical.lean` ```lean def CubicalGradient (p₀ p₁ : MasteryProvenance) : Type := { p : CTerm // HasType .nil p (.path (CubicalEmbed.ctype MasteryProvenance) (CubicalEmbed.toCTerm p₀) (CubicalEmbed.toCTerm p₁)) } namespace K7 /-- Constant gradient — the "do nothing" learning trajectory. -/ def init (p : MasteryProvenance) : CubicalGradient p p := ⟨Eq.toPath rfl, Eq.toPath_typed rfl⟩ /-- Compose two adjacent learning trajectories. Implementation uses cubical `.comp`. REL2.0 produces a stuck `ncomp` neutral that reads back as a syntactic `.comp` term — semantically correct (the path exists, paideia's downstream uses are type-driven). REL2.1 polishes to genuine reduction once pointwise-distribution-over-`.ind` lands in the engine. -/ def step {p₀ p₁ p₂ : MasteryProvenance} (γ : CubicalGradient p₀ p₁) (δ : CubicalGradient p₁ p₂) : CubicalGradient p₀ p₂ := … def lift {…} : … := … -- depends on what lift currently does end K7 ``` ### 3.5 Migration Per the user's "no compat shims" mandate, retire `MathPath` outright. Update every call site to use `CubicalGradient`. Keep the external API of `K7.init` / `step` / `lift` *type-identical*; only the underlying representation changes. ### 3.6 Tests Port any existing K7 tests to the new representation. Add: - `K7.init p`'s readback equals a constant `.plam` of `(toCTerm p)`. - `K7.step` of two distinct gradients produces a `Path`-typed CTerm (even if its readback is a syntactic `.comp` for now). - Round-trip: `MasteryProvenance.toCTerm ∘ fromCTerm = some` on a populated trace. ### 3.7 Acceptance criteria - paideia builds clean. - All previously-passing K7 tests pass with the new encoding. - New round-trip and type-coherence tests pass. - `MathPath` is fully retired (no remaining references). - A short note in `Paideia/README.md` records "K7 now ships on the cubical engine; see `Foundation/K7Cubical.lean` and `Bridge.lean` in the engine repo." - Engine issue #1 is commented with the closing reference. --- ## 4. Sequencing graph ``` cubical-engine `Dev_REL1` (already pushed) │ ▼ Phase 1 — interval (1–2d) (cubical engine + topolei follow-up) │ ▼ Phase 2 — Bridge.lean (3–5d) (cubical engine only) │ ▼ Phase 3 — paideia K7 cubical encoding (5–10d) (paideia, depends on engine + topolei) │ ▼ Coordinated merge train: engine `Dev_REL1` → main, topolei `Dev_REL1` → main, paideia `Dev_REL1` → main. Engine issue #1 closes with the K7 commit reference. ``` **Total: 9–17 working days.** Three repos. One coordinated merge. --- ## 5. Risks & mitigations | Risk | Likelihood | Mitigation | |------|-----------|------------| | Interval's introduction surfaces a hidden axiom that pattern-matches `CType` exhaustively. | Low | Build cleanly already after each phase 1 commit; existing topolei `DecEq.lean` is the only known consumer (already covered in 1.4). | | `Path.toEq` proof needs Glue NbE that isn't yet discharged. | Medium | Restrict REL2.0 backward bridge to neutral-free paths; document; defer full Glue interop to REL2.1. | | `KnowledgeNode`'s record shape requires a custom paideia schema (more work than expected). | Medium | Survey day in 3.2 catches this; budget contingency in 5–10d window. | | paideia has many `MathPath` call sites scattered across modules. | Low–Medium | Survey day catalogues them; migration is mechanical once the new type is in place. | | Rust ABI bump 2→3 breaks any out-of-tree consumers. | Low | Only `cubical-test` and `cubical-bench` link the .a; both are in-tree. Forgejo CI catches any drift. | | Coordinated merge train: paideia depends on engine which depends on topolei (cyclically via `Trace.lean` modifications). | Low | Engine has no topolei dep; the dependency is paideia → engine and paideia → topolei. No cycle. Land engine first, topolei second, paideia third. | --- ## 6. Definition of done (whole arc) - `eval .nil (CubicalEmbed.toCTerm mp)` round-trips to `mp` for every paideia-relevant `MasteryProvenance`. - `K7.init p` and `K7.step γ δ` produce well-typed CubicalGradients. - Issue #1 in `max/cubical-transport-hott-lean4` closes with a comment "K7 now ships as a literal cubical Path; see paideia `Dev_REL1` commit ``." - `KERNEL_BOUNDARY.md §2.6` records the bridge as landed. - `INDUCTIVE_TYPES.md` §11.4 records `dimExpr` typing as resolved (interval is the answer). - *(Optional, recommended)*: `docs/EULERIAN.md` writes up the river-bed / ferry / carrying-load metaphors next to their concrete Lean counterparts. The project's poetic record. --- ## 7. After REL2 — what comes next Items still deferred at end-of-arc, in rough priority: - **REL2.1 — Glue NbE completion + full backward bridge.** Removes the neutral-free restriction on `Path.toEq`. - **REL2.2 — Pointwise transport / composition distribution over `.ind`.** Makes `K7.step` reduce definitionally instead of staying as a stuck neutral. - **REL3 — Numerical layer.** `docs/NUMERICAL.md`'s vision lands; `Float`-CType primitive; `KnowledgeNode`'s float fields encode natively rather than opaquely. - **REL3+ — Higher cells (cells-spec §8).** 2-cells / n-cells build atop the HIT layer. Mostly Lean-native; small amount of engine support. - **REL4 — Cell layer / GPU shaders / interaction (cells-spec §6–§10).** Application surface; depends on most of the above. Each future item gets its own `docs/RELn_PLAN.md` when scoped. --- *End of REL2_PLAN.md. Companion to `INDUCTIVE_TYPES.md` (REL1 design) and `KERNEL_BOUNDARY.md` (long-horizon scope contract). Update as the arc progresses or as the user redirects.*