cubical-transport-hott-lean4/docs/REL2_PLAN.md

# 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 <nominal>` 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 `<hash>`."
- `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.*