REL1: design doc for schema-based inductive + HIT CTypes

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>
2026-04-30 14:57:22 -06:00 · 2026-04-30 14:57:22 -06:00 · f9e79b7b0d
commit f9e79b7b0d
parent 58330df245
1 changed files with 650 additions and 0 deletions
--- a/docs/INDUCTIVE_TYPES.md
+++ b/docs/INDUCTIVE_TYPES.md
@ -0,0 +1,650 @@
+# INDUCTIVE_TYPES.md — Schema-based inductive & higher-inductive CTypes
+
+*REL1 design contract for the schema-driven inductive-type extension to
+the cubical engine.  Targets: full HIT support (point + path
+constructors with arbitrary boundary partial-element systems, multi-
+parameter schemas, recursive constructor arguments).  Filed against
+issue #1 in `max/cubical-transport-hott-lean4` (2026-04-30); requested
+by paideia for K7's literal cubical-Path encoding.*
+
+---
+
+## 0. Status & scope
+
+**Status:** REL1 design — landing on `Dev_REL1`, not `main`, until the
+whole inductive refactor lands.
+
+**In scope (REL1):**
+
+- Plain (point-only) inductives: `Nat`, `Bool`, `List A`, polymorphic
+  parametric inductives, recursive ctor args.
+- HITs: path constructors with `dim`-binders + boundary partial-element
+  system; supports `S¹`, interval `I`, propositional truncation
+  `‖A‖₋₁`, suspension `Σ A`, pushouts.
+- Eliminator (`indElim`) with motive over `.ind S params`, one branch
+  per ctor.  Branches for path ctors carry a coherence obligation
+  matching the boundary system.
+- Transport / hcomp / heterogeneous comp over `.ind S params`.
+- FFI: full Rust dispatch on the new constructor tags.
+
+**Deferred (post-REL1):**
+
+- Indexed inductive families (`Vec n`, `Eq` natively).
+- Mutual / nested inductives in a single schema.
+- Higher path constructors (2-cells / squares / cubes inside a single
+  ctor body — the "boundary system" mechanism *technically* supports
+  arbitrarily many `dim` binders, but only in REL2 will we wire the
+  composition rules end-to-end).
+- Quotient inductive-inductive types (QIITs).
+
+**Breaking changes accepted up-front (REL1 mandate):**
+
+- `CType` and `CTerm` gain new constructors — every Lean module that
+  pattern-matches on these (`Subst`, `DimLine`, `Typing`, `Eval`,
+  `Value`, `Readback`, `Transport`, `TransportLaws`, `CompLaws`,
+  `Glue`, `System`, `Soundness`) gets new arms.
+- All existing axioms keep their statements; new ones added for the
+  new constructors.  The total axiom count grows.  No old axiom is
+  removed.
+- The `CTerm`/`CType` constructor *tags* will shift if we insert new
+  constructors mid-list.  Rust `tags.rs` and any tag-dispatching Rust
+  module pin tags via the Lean order — those need synchronised
+  updates.  We pin REL1 tag layout in §6 of this doc.
+- The Rust ABI version bumps from `1` to `2` (REL1).
+
+---
+
+## 1. The problem
+
+Paideia's K7 (`BootstrapGradient`) is ideologically a literal cubical
+`Path` between two `MasteryProvenance` values.  `MasteryProvenance` is
+a `Trace KnowledgeNode` — a list of records.  Encoding it as a CTerm
+of a `Path`-typed CType requires a `CType` for "list of `KnowledgeNode`
+serialisations."  The engine currently has no inductive types — only
+`univ | pi | path | sigma | glue`.  So `toCTerm : MasteryProvenance →
+CTerm` is undefinable.
+
+The same shape recurs for every downstream consumer that wants to
+embed Lean-inductive data into the cubical universe:
+
+- `Color/Space.lean` (modular color spaces) — was sketched as a HIT.
+- Future cell-graph rendering inputs.
+- Cubical Path-equality on `Bool`, `Nat`, `List` — needed for any
+  serious bridge to discrete-math reasoning.
+
+REL1 unblocks all of these in one move.
+
+---
+
+## 2. Schema model — the data
+
+### 2.1 Argument shape
+
+```lean
+inductive CTypeArg where
+  /-- Non-recursive arg of a fixed CType (may reference schema params
+      via `.param i` inside `A`).  Examples: `cons : A → List A → List A`
+      has its first arg as `.type (CType.ind ListSchema [.param 0])`
+      shadowed via the param mechanism — see §2.4. -/
+  | type   (A : CType)
+  /-- The `i`th schema parameter (zero-indexed against `numParams`). -/
+  | param  (i : Nat)
+  /-- Recursive reference to the inductive being defined.  Distinct
+      from `.type (CType.ind …)` because schemas are open-recursive
+      until they're inhabited — `.self` lets us state the schema
+      without a fixpoint operator. -/
+  | self
+  /-- Dimension binder.  Used in path constructors.  When the ctor is
+      applied with a concrete `DimExpr`, the elimination rule consults
+      the boundary system to decide whether to produce the raw value
+      or fire a clause. -/
+  | dim
+  deriving Repr, BEq
+```
+
+### 2.2 Constructor specification
+
+```lean
+structure CtorSpec where
+  /-- Constructor name.  Must be unique within a schema. -/
+  name     : String
+  /-- Argument list, in order.  The boundary system (below) may refer
+      to args by index; ctor application supplies one CTerm per arg
+      in this order. -/
+  args     : List CTypeArg
+  /-- Boundary partial-element system.  Empty list ≡ point ctor.
+      Non-empty list ≡ path ctor: each clause says "on this face of
+      the dim args, this ctor reduces to this value (a CTerm in scope
+      where the args are bound)."
+
+      Coherence obligations on the clauses (enforced at
+      schema-validation time, not by the type of `boundary`):
+
+      1. Every face mentioned in the clause refers only to `.dim`
+         args of this ctor.
+      2. Clause faces are pairwise compatible — overlapping faces
+         agree on the overlap.
+      3. The collection of clause faces, taken as a join, equals the
+         outer boundary of the cube formed by the dim args (i.e. for
+         `k` dim args there are `2k` faces and every dimension's
+         endpoints must be specified, possibly via `.top`-faced
+         clauses if the boundary is constant).
+  -/
+  boundary : List (FaceFormula × CTerm)
+  deriving Repr
+```
+
+### 2.3 Schema
+
+```lean
+structure CTypeSchema where
+  name      : String
+  numParams : Nat
+  ctors     : List CtorSpec
+  deriving Repr
+```
+
+Equality on schemas is *structural by schema name + numParams + ctor
+list*.  The engine doesn't intern schemas; two schemas with the same
+name in different modules are distinct values.
+
+### 2.4 Embedding into `CType` / `CTerm`
+
+```lean
+inductive CType where
+  | univ
+  | pi    (A B : CType)
+  | path  (A : CType) (a b : CTerm)
+  | sigma (A B : CType)
+  | glue  (φ : FaceFormula) (T : CType)
+          (f fInv sec ret coh : CTerm) (A : CType)
+  /-- NEW: an instance of a schema-defined inductive type at given
+      parameters.  `params.length = S.numParams` is a typing-side
+      condition. -/
+  | ind   (S : CTypeSchema) (params : List CType)
+
+inductive CTerm where
+  | var, lam, app, plam, papp, transp, comp, compN
+  | glueIn, unglue
+  | pair, fst, snd
+  /-- NEW: constructor application.  `ctorName` selects the clause
+      from `S.ctors`; `params` matches the schema parameters; `args`
+      supplies one CTerm per `CtorSpec.args` entry, with the
+      same arity ordering. -/
+  | ctor    (S : CTypeSchema) (ctorName : String)
+            (params : List CType) (args : List CTerm)
+  /-- NEW: induction principle / eliminator.  `motive` is a CTerm
+      defining `λ x : .ind S params. Type` — i.e. a function whose
+      body is a CType expression with the bound name in scope.
+      `branches` lists `(ctorName, body)` pairs in *schema-declaration
+      order*; each branch's `body` is a CTerm taking the ctor's args
+      *and one extra arg per recursive `.self` arg* (the recursive
+      hypothesis, i.e. the result of the eliminator on the recursive
+      sub-value).  `target` is the inductive-typed term being
+      eliminated. -/
+  | indElim (S : CTypeSchema) (params : List CType)
+            (motive : CTerm)
+            (branches : List (String × CTerm))
+            (target : CTerm)
+```
+
+A constructor's `args` carries its *full* arg list, including dim
+args.  When typing `.ctor S "loop" params [d]`, we know from `S.ctors`
+that `loop` has `[.dim]`, so `d` must be a `CTerm` interpreted as a
+`DimExpr` (we lift via `CTerm.var`-of-the-dim's name; or via a new
+`CTerm.dimExpr (r : DimExpr) : CTerm` constructor — see §2.5).
+
+### 2.5 Dim args at the term level
+
+Path-ctor application crosses the term/dim boundary.  Two options:
+
+**Option A — borrow `.var x`:** The dim-arg position in
+`CTerm.ctor`'s `args` carries a `CTerm.var "i"` whose name happens to
+be a `DimVar` name.  Subst, eval, and dispatch all special-case "this
+position is a dim arg" and read the name as a `DimVar`, looking it up
+in a dim environment that the cubical evaluator maintains in parallel.
+
+Pros: no new CTerm constructor.  Cons: punny & ambiguous; substituting
+a non-var DimExpr (like `.meet i j`) is impossible without re-encoding.
+
+**Option B — new `CTerm.dimExpr (r : DimExpr) : CTerm`:** A first-
+class CTerm carrying a dim expression.  Only legal in dim-arg
+positions; ill-typed elsewhere.
+
+Pros: fully general; `meet`/`join`/`inv` of dim args are expressible.
+Cons: one more CTerm constructor; one more substitution arm; one more
+eval / readback / typing rule.
+
+**Decision: Option B.**  The user mandate is "no shortcuts."  Path
+constructors may want `.meet i j`-shaped boundary applications later
+(e.g., for higher cubes), so we pay the constructor cost now.  REL1
+ships `CTerm.dimExpr`.
+
+---
+
+## 3. Worked examples
+
+### 3.1 `Nat`
+
+```
+schema Nat:
+  numParams = 0
+  ctors:
+    .point "zero" []
+    .point "succ" [.self]
+```
+
+```
+CType:    .ind NatSchema []
+zero  ::= .ctor NatSchema "zero" [] []
+succ n::= .ctor NatSchema "succ" [] [n]
+```
+
+### 3.2 `List A`
+
+```
+schema List:
+  numParams = 1
+  ctors:
+    .point "nil"  []
+    .point "cons" [.param 0, .self]
+```
+
+```
+CType:    .ind ListSchema [A]
+nil   ::= .ctor ListSchema "nil"  [A] []
+cons x::= λxs. .ctor ListSchema "cons" [A] [x, xs]
+```
+
+### 3.3 `Bool`
+
+```
+schema Bool:
+  numParams = 0
+  ctors:
+    .point "false" []
+    .point "true"  []
+```
+
+### 3.4 `S¹`
+
+```
+schema S¹:
+  numParams = 0
+  ctors:
+    .point "base" []
+    .path  "loop" [.dim "i"]   -- one dim binder, named for boundary refs
+           boundary:
+             [(.eq0 i, base()), (.eq1 i, base())]
+```
+
+Note: `.dim` carries no name in `CTypeArg` — boundary clauses
+reference dim args positionally (the *kth* `.dim` in `args` becomes
+`DimVar.mk "$d_k"` at typing time).
+
+### 3.5 Propositional truncation `‖A‖₋₁`
+
+```
+schema PropTrunc:
+  numParams = 1     -- A
+  ctors:
+    .point "in"     [.param 0]
+    .path  "squash" [.self, .self, .dim]
+           boundary:
+             [(.eq0 d, /-arg 0-/), (.eq1 d, /-arg 1-/)]
+```
+
+(Boundary clause bodies use a positional `argRef`-encoding inside
+their CTerm — see §4.)
+
+### 3.6 Suspension `Σ A`
+
+```
+schema Susp:
+  numParams = 1
+  ctors:
+    .point "north" []
+    .point "south" []
+    .path  "merid" [.param 0, .dim]
+           boundary:
+             [(.eq0 d, north()), (.eq1 d, south())]
+```
+
+---
+
+## 4. Boundary system semantics
+
+The `boundary : List (FaceFormula × CTerm)` field has body CTerms in a
+specific scope: the ctor's args are *all* in scope, addressed by
+`CTerm.var "$arg_k"` where `k` is the arg index.  The face formulae
+range over the dim args, addressed by `DimVar.mk "$d_k"` where `k` is
+the *dim*-arg index (counted only among `.dim` args).
+
+When `eval` encounters `.ctor S c params args`:
+
+1. Resolve the ctor spec: `cs := S.ctors.find name == c`.
+2. Build a dim-evaluation environment from the dim args of `args`:
+   `dimEnv := λ d. eval-as-DimExpr (args.nth idxOfDim_d)`.
+3. Evaluate each boundary clause's face: `φ.eval dimEnv`.
+4. If any clause's face evaluates to `true` (canonical), substitute
+   the clause body (with arg references resolved) and evaluate that
+   instead.
+5. Otherwise, the ctor application is canonical — produce
+   `CVal.vctor`.
+
+A path ctor with all-`.bot` boundary faces is canonical at every
+generic dim — it acts like a free higher-dimensional generator.
+
+---
+
+## 5. Eliminator (`indElim`)
+
+```
+indElim S params motive [(c₁, b₁), (c₂, b₂), …] target : CTerm
+```
+
+Typing rule sketch:
+
+1. `target : .ind S params`.
+2. `motive : .pi (.ind S params) .univ` (depending on whether we
+   model the motive as a function or a closed `CType`-valued term —
+   REL1 ships the `pi`-valued form).
+3. For each ctor `cᵢ`:
+   - The branch `bᵢ` has type
+     `args.foldr (λa rest. matchArg a rest) (.app motive (rebuilt-ctor))`
+   - `matchArg`:
+     - `.type A` → `.pi A rest`
+     - `.param j` → `.pi (params.nth j) rest`
+     - `.self` → `.pi (.ind S params) (.pi (.app motive bvar) rest)`
+       — i.e. take the recursive arg *and* the recursive hypothesis.
+     - `.dim` → `.path … …` — the dim is universally quantified
+       over the interval (modelled as a closed plam).
+4. For path ctors, the branch must satisfy boundary coherence: at
+   each `(φ, body)` of the ctor's boundary, the branch evaluated at
+   the corresponding face equals the appropriate substitution into
+   the corresponding ctor (recursively eliminated).  This is a
+   typing-level side condition mirroring `.comp`'s compatibility
+   condition.
+
+Reduction rule (β):
+
+```
+indElim S params M [(c₁,b₁), …] (ctor S cᵢ params [a₁,…,aₘ])
+  ⟶ bᵢ a₁ … aₘ ih₁ … ihₖ
+```
+
+where `ihⱼ` is the `indElim`-result of each `.self`-typed argument.
+
+---
+
+## 6. Constructor tag layout (REL1 freeze)
+
+Lean's `inductive` assigns tags in declaration order.  Rust dispatch
+relies on this order.  REL1 freeze:
+
+**`CType` tags (REL1):**
+
+| Tag | Constructor | Notes |
+|-----|-------------|-------|
+| 0 | `.univ`     | unchanged from REL0 |
+| 1 | `.pi`       | unchanged |
+| 2 | `.path`     | unchanged |
+| 3 | `.sigma`    | unchanged |
+| 4 | `.glue`     | unchanged |
+| 5 | `.ind`      | **NEW** |
+
+**`CTerm` tags (REL1):**
+
+| Tag | Constructor |
+|-----|-------------|
+| 0 | `.var` |
+| 1 | `.lam` |
+| 2 | `.app` |
+| 3 | `.plam` |
+| 4 | `.papp` |
+| 5 | `.transp` |
+| 6 | `.comp` |
+| 7 | `.compN` |
+| 8 | `.glueIn` |
+| 9 | `.unglue` |
+| 10 | `.pair` |
+| 11 | `.fst` |
+| 12 | `.snd` |
+| 13 | `.dimExpr` | **NEW** |
+| 14 | `.ctor`    | **NEW** |
+| 15 | `.indElim` | **NEW** |
+
+**`CVal` tags (REL1):**
+
+| Tag | Constructor |
+|-----|-------------|
+| 0 | `.vlam` |
+| 1 | `.vplam` |
+| 2 | `.vneu` |
+| 3 | `.vTranspFun` |
+| 4 | `.vHCompFun` |
+| 5 | `.vTubeApp` |
+| 6 | `.vCompFun` |
+| 7 | `.vPathTransp` |
+| 8 | `.vpair` |
+| 9 | `.vctor`     | **NEW** — fully-applied schema constructor |
+
+**`CNeu` tags (REL1):**
+
+| Tag | Constructor |
+|-----|-------------|
+| 0 | `.nvar` |
+| 1 | `.napp` |
+| 2 | `.npapp` |
+| 3 | `.ntransp` |
+| 4 | `.ncomp` |
+| 5 | `.nhcomp` |
+| 6 | `.ncompN` |
+| 7 | `.nglueIn` |
+| 8 | `.nunglue` |
+| 9 | `.nfst` |
+| 10 | `.nsnd` |
+| 11 | `.nIndElim` | **NEW** — stuck eliminator |
+
+**Rust ABI version bump:** `TOPOLEI_FFI_ABI_VERSION 1 → 2`.
+
+---
+
+## 7. Reductions (axiom catalogue)
+
+### 7.1 `eval` arms
+
+- `eval_ctor` — `eval env (.ctor S c params args) = .vctor S c params (args.map (eval env))` for point ctors.
+- `eval_ctor_path_face_fires` — for path ctors, when one of the
+  boundary clauses' face evaluates to `true` under the dim-env from
+  the supplied args, eval substitutes that clause body and
+  re-evaluates.
+- `eval_indElim_ctor` — β-reduction of the eliminator on a
+  fully-applied constructor.
+- `eval_indElim_stuck` — produces `.vneu (.nIndElim …)` when target
+  is neutral.
+- `eval_dimExpr` — `eval env (.dimExpr r) = .vdimExpr r` (or routes
+  through a `vdim` neutral; design pending — placeholder pinned at
+  REL1 implementation time).
+
+### 7.2 Transport
+
+- `eval_transp_ind_const` — when every parameter is dim-absent from
+  the binder, transport over `.ind S params` is identity (T2).
+- `eval_transp_ind_pointwise` — transport over a varying-parameter
+  inductive applied to a `.vctor` distributes pointwise: each
+  non-recursive arg is transported via its CType's transport rule;
+  each `.self` arg is transported via the same outer-`.ind`
+  transport recursively.
+- `eval_transp_ind_path_ctor` — for path ctors, transport must
+  respect the boundary system; CCHM gives the explicit formula via
+  `comp`-shaped fillers.
+- `eval_transp_ind_stuck` — `.vneu (.ntransp …)` for non-canonical
+  targets.
+
+### 7.3 Composition
+
+- `eval_comp_ind_const`, `eval_comp_ind_pointwise`,
+  `eval_comp_ind_path_ctor`, `eval_comp_ind_stuck` — analogous to
+  `pi` rules in the existing `CompLaws.lean`.
+
+### 7.4 Readback
+
+- `readback_vctor` — `vctor S c params vargs ⟶ .ctor S c params (vargs.map readback)`
+- `readbackNeu_nIndElim` — straightforward.
+
+---
+
+## 8. FFI surface (REL1)
+
+Add to `native/cubical/include/topolei_cubical.h`:
+
+```c
+lean_obj_res topolei_cubical_vIndElim(
+    b_lean_obj_arg env, b_lean_obj_arg S, b_lean_obj_arg params,
+    b_lean_obj_arg motive, b_lean_obj_arg branches,
+    b_lean_obj_arg target);
+
+lean_obj_res topolei_cubical_vCtor(
+    b_lean_obj_arg S, b_lean_obj_arg name,
+    b_lean_obj_arg params, b_lean_obj_arg args);
+```
+
+`eval` / `readback` / `subst` / `dim_absent` — extend tag-dispatch
+arms in Rust to cover `CTerm.{dimExpr, ctor, indElim}`,
+`CType.ind`, `CVal.vctor`, `CNeu.nIndElim`.
+
+Substitution of `.var`-named dim args inside `CTerm.dimExpr` follows
+the same path as `DimExpr.subst` already does — Rust `subst.rs` gains
+a single arm.
+
+---
+
+## 9. Migration notes (downstream consumers)
+
+### 9.1 `topolei` (sibling repo) — concrete impact
+
+Surveyed against `topolei` HEAD (2026-04-30).  Six files import
+`CubicalTransport.*` and pattern-match on engine types; the breakage
+is well-bounded — every match is structural recursion that mirrors
+the existing `compN`/`pair`/`unglue` shape, so new constructors slot
+in cleanly.
+
+| File | Match shape | New arms required |
+|------|-------------|-------------------|
+| `Topolei/Cubical/DecEq.lean`     | exhaustive `CTerm.beq` (13 arms), `CType.beq` (5 arms), reflexivity proofs | +1 `CType` arm (`.ind`); +3 `CTerm` arms (`.dimExpr`, `.ctor`, `.indElim`) |
+| `Topolei/Cubical/Trace.lean`     | exhaustive `CTerm.traceOf` recursing into every sub-CTerm | +3 `CTerm` arms; structural — recurse via `Trace.union` over `args` / `branches` / `target` |
+| `Topolei/Cubical/TraceAt.lean`   | exhaustive `CTerm.traceOfAt`; **13 per-constructor `subTrace_*` lifting lemmas** | +3 arms in `traceOfAt`; +3 new lifting lemmas (`subTrace_dimExpr`, `subTrace_ctor`, `subTrace_indElim`) |
+| `Topolei/Cubical/FluxR.lean`     | exhaustive `CTerm.fluxAtAcc` (Float-weighted face propagation) | +3 arms; flux weight = `min` over sub-CTerms (same pattern as `compN`) |
+| `Topolei/EML/Path.lean`          | none on `CType`/`CTerm` — uses `DimLine` as a black box | none |
+| `Topolei/EML/Cubical.lean`       | partial `CTerm.evalEML` with `_ => 0.0` fallback (intentional) | none — fallback handles new shapes |
+
+**Schema/CtorSpec/CTypeArg/dimExpr design choice — why it fits topolei:**
+the new `CTerm.{dimExpr, ctor, indElim}` constructors all have either
+no sub-CTerms (`dimExpr`) or a flat `List CTerm` of sub-terms (`args`,
+`branches.map .2`, `motive`, `target`).  Topolei's recursors all
+already handle the "list of sub-CTerms" shape (see `compN`'s clauses
+arm in `Trace.lean:107`).  No new recursion machinery is needed — the
+new arms are mechanical.
+
+**`CTypeSchema` is opaque to topolei.**  The schema is part of the
+mutual inductive block at the engine level, but topolei never
+pattern-matches on `CTypeSchema` / `CtorSpec` / `CTypeArg` directly —
+it only sees them as opaque payloads inside `CType.ind` / `CTerm.ctor` /
+`CTerm.indElim`.  Schema-internal CTerms (boundary clause bodies)
+are static schema-level data, not part of any user term's trace.
+
+**Migration plan for topolei (post-engine REL1 merge):**
+
+1. Extend `DecEq.lean`: add ind-arm to `CType.beq`; add three arms to
+   `CTerm.beq` plus refl proofs.  Decision: equality on `CTypeSchema`
+   inside `CType.ind` reduces to schema *name* equality plus `params`
+   equality (REL1 does not intern schemas; structural equality on
+   the full schema struct is provided as a separate decision
+   procedure — see §11.2).
+2. Extend `Trace.lean`'s `traceOf` and the helper clause recursor.
+3. Extend `TraceAt.lean`'s `traceOfAt`, `traceOfAt.clauses`, plus
+   add the three new lifting lemmas matching the existing 13.
+4. Extend `FluxR.lean`'s `fluxAtAcc` (and its clause helper).
+5. `Path.lean`, `EML/Cubical.lean` — no changes needed.
+
+Estimated topolei migration: ~150–250 lines across the four files,
+mostly mechanical recursion arms.
+
+### 9.2 `paideia` and other downstream
+
+Paideia is the *driver* of this refactor — its K7 work depends on it.
+Migration sequence in §9.3 of the original issue body.  Other
+downstream consumers (any project depending on `topolei` rather than
+the engine directly) get the breakage indirectly through topolei's
+`Trace`/`TraceAt`/`FluxR` API surface, which is preserved by name
+(only the new arms are added).
+
+### 9.3 Rust kernel
+
+`native/cubical/src/{tags.rs, value.rs, eval.rs, readback.rs,
+subst.rs, dim_absent.rs}` all switch on Lean constructor tags.  REL1
+freezes the new tag layout in §6 above; Rust modules update in
+lockstep.  ABI version bumps to `2`.
+
+### 9.2 `paideia`
+
+- `Paideia/Foundation/K7Cubical.lean` retires `MathPath` in favour of
+  `CTerm`-typed values of `Path (.ind ListSchema [KNodeCType])`.
+- New module `Paideia/Foundation/MasteryEncoding.lean` defines
+  `KnowledgeNode.toCTerm`, `MasteryProvenance.toCTerm` (using
+  `ListSchema`), and the inverse parser.
+- K7's external API (`init`, `step`, `lift`) keeps its types; only
+  the under-the-hood representation moves to engine-grounded paths.
+
+---
+
+## 10. Test plan
+
+### 10.1 Plain inductives
+
+- `nat_zero_succ_eval` — eval `succ (succ zero)` to `vctor … "succ" [vctor … "succ" [vctor … "zero" []]]`.
+- `list_cons_nil_eval` — same shape, parameterised.
+- `nat_indElim_plus` — define `plus : Nat → Nat → Nat` via indElim;
+  eval `plus 2 3 = 5` (engine-side).
+- `transp_const_list_id` — transport over a constant `List Nat` line
+  is identity.
+
+### 10.2 HITs
+
+- `s1_loop_endpoints` — `loop @ 0 = base`, `loop @ 1 = base`.
+- `prop_trunc_squash` — any two `‖A‖₋₁` values are connected by a path.
+- `susp_merid_endpoints` — `merid a @ 0 = north`, `merid a @ 1 = south`.
+- `transp_s1_const` — transport over a constant S¹ line is identity.
+
+### 10.3 Cross-cutting
+
+- Property tests: schemas with N constructors and M dim args, random
+  ctor application; check that boundary firing is consistent with
+  manual reduction.
+- Differential fuzz against Rust impl: post-Phase-D regression suite.
+
+---
+
+## 11. Open questions (REL1 implementation)
+
+1. **Schema interning.**  We don't intern schemas in REL1 (every
+   `.ind` carries the schema by value).  This means schemas are
+   structurally compared.  If schemas grow large, switch to a global
+   registry keyed by `name`.  Defer until profiling justifies.
+2. **Equality on schemas.**  Lean's `deriving BEq`/`DecidableEq`
+   over `CTypeSchema` is non-trivial because `CtorSpec.boundary`
+   contains `CTerm`s, which mutually recurse with `CType`.  We
+   deliberately don't derive `BEq` — equality is structural per
+   the inductive definition; any `BEq` instance is provided by a
+   bespoke decision procedure (REL1.1, post-merge).
+3. **Soundness chapter.**  The transport-over-HIT chapter
+   (cells-spec §14, "HIT transport") becomes a real deliverable in
+   REL1 alongside the new axioms.  Statement and proof obligations
+   listed in §11 of `Soundness.lean` after the refactor.
+
+---
+
+*End of INDUCTIVE_TYPES.md.  This document is the contract between
+the engine refactor and downstream consumers.  Update on every API
+shape change before the change lands.*