diff --git a/docs/REL2_PLAN.md b/docs/REL2_PLAN.md new file mode 100644 index 0000000..1a75ee6 --- /dev/null +++ b/docs/REL2_PLAN.md @@ -0,0 +1,411 @@ +# 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.*