REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46)

Inductive.lean (new module): schema combinators (mkSchema, mkCtor,
mkPath) and canonical schema instances:
  - Plain inductives: natSchema, boolSchema, listSchema
  - HITs: s1Schema, intervalSchema, propTruncSchema
Plus type-level helpers (CType.natC, listC, s1C, …) and term-level
ergonomic builders (zeroC, succC, nilC, consC, baseC, loopC, …,
natLit, natElim, boolElim, listElim).

Rust kernel (native/cubical/src/):
  · tags.rs       — TY_IND, TERM_DIMEXPR/CTOR/INDELIM, VAL_VCTOR/VDIMEXPR,
                    NEU_NINDELIM tag constants per docs/INDUCTIVE_TYPES.md §6.
  · value.rs      — mk_vctor, mk_vdimexpr, mk_nindelim builders.
  · eval.rs       — TERM_DIMEXPR / TERM_CTOR / TERM_INDELIM dispatch
                    arms; full β-reduction on canonical vctor target
                    (find matching branch by name, vapp chain over
                    ctor args); stuck nIndElim build for vneu target;
                    eval_term_list / eval_branches / find_branch_body
                    helpers (recursive list walking).
  · readback.rs   — VAL_VCTOR / VAL_VDIMEXPR readback arms;
                    readback_val_list, map_readback_branches helpers;
                    NEU_NINDELIM neutral readback; mk_term_dimexpr,
                    mk_term_ctor, mk_term_indelim builders.

Tests (CubicalTransport/FFITest.lean): nine new smoke arms exercising
canonical-form eval (zero, succ-of-succ, false, cons-true-nil, base,
loop@r), readback round-trip on succ zero, and indElim β on Bool with
both branch directions.  Result: 25/25 smoke + 46/46 properties =
71/71 passing.

Existing tests untouched (constructor tags preserved per REL1 freeze).
Rust ABI version is now de facto v2 (new tags); update the
TOPOLEI_FFI_ABI_VERSION constant in a follow-up commit.

Remaining REL1 work (per task list):
  - #4  HasType arms for ctor / indElim
  - #8  transport over .ind axioms
  - #9  composition over .ind axioms
  - Path-ctor boundary firing (REL1.1)
  - Recursive-arg IH wiring in indElim β (REL1.1)
  - Topolei migration (sibling repo) per docs/INDUCTIVE_TYPES.md §9.1

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

CubicalTransport.lean

@@ -19,4 +19,5 @@ import CubicalTransport.TransportLaws
 import CubicalTransport.System
 import CubicalTransport.CompLaws
 import CubicalTransport.Soundness
+import CubicalTransport.Inductive
 import CubicalTransport.PropertyTest

CubicalTransport/FFITest.lean

@@ -20,6 +20,10 @@
 
 import CubicalTransport.Readback
 import CubicalTransport.FFI
+import CubicalTransport.Inductive
+
+open CubicalTransport.Inductive
+open CubicalTransport.Inductive.CTerm
 
 namespace CubicalTransportFFITest
 
@@ -139,7 +143,37 @@ def tests : List (String × String × String) :=
      cvalSummary (vPApp
        (.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
        (.var ⟨"r"⟩)),
-     "vneu ncompN") ]
+     "vneu ncompN"),
+    -- ── REL1 inductive-type smoke tests ─────────────────────────────────────
+    ("eval (zero : Nat) ⇓ vctor zero",
+     cvalSummary (eval .nil zeroC),
+     "vctor zero ..."),
+    ("eval (succ (succ zero) : Nat) ⇓ vctor succ",
+     cvalSummary (eval .nil (succC (succC zeroC))),
+     "vctor succ ..."),
+    ("eval (false : Bool) ⇓ vctor false",
+     cvalSummary (eval .nil falseC),
+     "vctor false ..."),
+    ("eval (cons true nil : List Bool) ⇓ vctor cons",
+     cvalSummary (eval .nil (consC CType.boolC trueC (nilC CType.boolC))),
+     "vctor cons ..."),
+    ("readback ∘ eval (succ zero : Nat) ≡ ctor succ",
+     ctermSummary (readback (eval .nil (succC zeroC))),
+     "ctor succ ..."),
+    ("eval (base : S¹) ⇓ vctor base",
+     cvalSummary (eval .nil baseC),
+     "vctor base ..."),
+    ("eval (loop @ r : S¹) ⇓ vctor loop",
+     cvalSummary (eval .nil (loopC (.var ⟨"r"⟩))),
+     "vctor loop ..."),
+    ("indElim Bool false-case (true → \"yes\") on true ⇓ \"yes\"",
+     cvalSummary (eval .nil
+       (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") trueC)),
+     "vneu nvar yes"),
+    ("indElim Bool true-case on false ⇓ \"no\"",
+     cvalSummary (eval .nil
+       (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") falseC)),
+     "vneu nvar no") ]
 
 /-- Run every smoke test, print its actual vs expected.  Returns the
     number of failures. -/

CubicalTransport/Inductive.lean

@@ -0,0 +1,265 @@
+/-
+  CubicalTransport.Inductive
+  ==========================
+  Helper combinators and canonical schema instances for the REL1
+  schema-based inductive (and higher-inductive) type system.
+
+  This module sits *on top of* `Syntax.lean` — it doesn't add new
+  primitives, only ergonomic builders.  Every value here is a plain
+  CTypeSchema / CType / CTerm; nothing is opaque.  Downstream
+  consumers should prefer these helpers over hand-spelling
+  CTypeSchema literals so the canonical encodings are maintained
+  in one place.
+
+  ## Sections
+
+  · §1  Argument-shape helpers
+  · §2  Schema constructors (mkSchema, mkCtor, mkPath)
+  · §3  Type-level helpers (CType.list, CType.nat, …, CType.s1, …)
+  · §4  Term-level helpers (zeroC, succC, nilC, consC, baseC, loopC, …)
+  · §5  Eliminator builders (natElim, listElim, …)
+
+  ## Design notes
+
+  · Boundary clauses inside HIT path constructors reference *dim args*
+    via `DimVar.mk "$d_k"` (zero-indexed among `.dim` args) and
+    *non-dim args* via `CTerm.var "$arg_k"` (zero-indexed in the full
+    arg list).  See INDUCTIVE_TYPES.md §4 for the discipline.
+
+  · The schemas here are concrete values, not `def`s under a
+    `noncomputable` veil — `Nat`, `Bool`, etc. are first-class data
+    that downstream code can pattern-match on or use as parameters.
+-/
+
+import CubicalTransport.Syntax
+
+namespace CubicalTransport.Inductive
+
+-- ── §1. Argument-shape helpers ─────────────────────────────────────────────
+
+/-- A non-recursive argument of a closed CType. -/
+@[inline] def argType (A : CType) : CTypeArg := .type A
+
+/-- A reference to the schema's `i`th type parameter. -/
+@[inline] def argParam (i : Nat) : CTypeArg := .param i
+
+/-- A recursive argument of the inductive being defined. -/
+@[inline] def argSelf : CTypeArg := .self
+
+/-- A dimension argument (path-constructor binder). -/
+@[inline] def argDim : CTypeArg := .dim
+
+-- ── §2. Schema constructors ────────────────────────────────────────────────
+
+/-- A point constructor (no boundary system, empty boundary list). -/
+@[inline] def mkCtor (name : String) (args : List CTypeArg) : CtorSpec :=
+  .mk name args []
+
+/-- A path constructor: a constructor whose argument list contains at
+    least one `.dim` arg, and whose boundary system specifies the
+    canonical reduction on the corresponding cube faces. -/
+@[inline] def mkPath (name : String) (args : List CTypeArg)
+    (boundary : List (FaceFormula × CTerm)) : CtorSpec :=
+  .mk name args boundary
+
+/-- Build a schema from name, parameter count, and constructor list. -/
+@[inline] def mkSchema (name : String) (numParams : Nat)
+    (ctors : List CtorSpec) : CTypeSchema :=
+  .mk name numParams ctors
+
+-- ── §3. Canonical plain inductive schemas ──────────────────────────────────
+
+/-- The natural numbers as a schema.
+
+    `Nat` has two point constructors:
+    - `zero : Nat`
+    - `succ : Nat → Nat` (recursive arg: `.self`)
+-/
+def natSchema : CTypeSchema :=
+  mkSchema "Nat" 0
+    [ mkCtor "zero" []
+    , mkCtor "succ" [.self] ]
+
+/-- The booleans as a schema. -/
+def boolSchema : CTypeSchema :=
+  mkSchema "Bool" 0
+    [ mkCtor "false" []
+    , mkCtor "true"  [] ]
+
+/-- Polymorphic lists as a schema, parameterised by the element type. -/
+def listSchema : CTypeSchema :=
+  mkSchema "List" 1
+    [ mkCtor "nil"  []
+    , mkCtor "cons" [.param 0, .self] ]
+
+-- ── §4. Canonical HIT schemas ──────────────────────────────────────────────
+
+/-- The circle `S¹` as a HIT.
+
+    Constructors:
+    - `base : S¹`                       (point)
+    - `loop : (i : I) → S¹`             (path: `loop @ 0 = base = loop @ 1`)
+
+    Boundary: at `i=0` and `i=1`, `loop` returns `base`.
+
+    The `loop` boundary references `base` via the schema's own
+    `.ctor` constructor at the same schema (recursive self-reference
+    inside the schema's body).  We construct it inline here. -/
+def s1Schema : CTypeSchema :=
+  -- Build a self-referential schema: `loop`'s boundary uses
+  -- `.ctor s1Schema "base" [] []` which in turn references `s1Schema`.
+  -- Since the recursion is structural through the schema's data
+  -- (not through a Lean-level fixpoint), we define `s1Schema` via
+  -- Lean's well-founded recursion through structural data; the
+  -- result is a finite, well-formed `CTypeSchema` value — but Lean
+  -- won't accept a literal self-recursive `def` like this.
+  --
+  -- Workaround: take the schema *name* + a fresh local schema that
+  -- refers to itself via a placeholder.  At construction time we
+  -- patch the placeholder.  This is implemented as a small fix-up
+  -- below.
+  let baseAt (s : CTypeSchema) : CTerm := .ctor s "base" [] []
+  -- We need `s1Schema = mkSchema "S¹" 0 [base, loop]` where
+  -- `loop` carries a boundary that references `s1Schema`.
+  -- Lean's `let rec` doesn't handle this for `CTypeSchema` the
+  -- way it would for a function — but we can use a `where`-style
+  -- two-step build: first build a "stub" schema, then build the
+  -- final `loop` referring to it.  Both schemas have the same
+  -- structural shape, so `s1Schema` is well-defined.
+  let stub : CTypeSchema :=
+    mkSchema "S¹" 0
+      [ mkCtor "base" []
+      , mkPath "loop" [.dim] [] ]
+  let d : DimVar := ⟨"$d_0"⟩
+  mkSchema "S¹" 0
+    [ mkCtor "base" []
+    , mkPath "loop" [.dim]
+        [ (.eq0 d, baseAt stub)
+        , (.eq1 d, baseAt stub) ] ]
+
+/-- The interval as a HIT.
+
+    Constructors:
+    - `zero : I`
+    - `one  : I`
+    - `seg  : (i : I) → I` with `seg @ 0 = zero`, `seg @ 1 = one`. -/
+def intervalSchema : CTypeSchema :=
+  let stub : CTypeSchema :=
+    mkSchema "I" 0
+      [ mkCtor "zero" []
+      , mkCtor "one"  []
+      , mkPath "seg" [.dim] [] ]
+  let zeroAt (s : CTypeSchema) : CTerm := .ctor s "zero" [] []
+  let oneAt  (s : CTypeSchema) : CTerm := .ctor s "one"  [] []
+  let d : DimVar := ⟨"$d_0"⟩
+  mkSchema "I" 0
+    [ mkCtor "zero" []
+    , mkCtor "one"  []
+    , mkPath "seg" [.dim]
+        [ (.eq0 d, zeroAt stub)
+        , (.eq1 d, oneAt  stub) ] ]
+
+/-- Propositional truncation `‖A‖₋₁` as a HIT.
+
+    Constructors:
+    - `inT  : A → ‖A‖₋₁`           (point)
+    - `squash : (x y : ‖A‖₋₁) → (i : I) → ‖A‖₋₁`
+        with `squash x y @ 0 = x`, `squash x y @ 1 = y`. -/
+def propTruncSchema : CTypeSchema :=
+  let d : DimVar := ⟨"$d_0"⟩
+  -- arg index: 0 = first .self ("$arg_0"), 1 = second .self ("$arg_1"),
+  -- 2 = .dim ($d_0).  Boundary references positional arg names.
+  mkSchema "‖_‖₋₁" 1
+    [ mkCtor "inT"    [.param 0]
+    , mkPath "squash" [.self, .self, .dim]
+        [ (.eq0 d, .var "$arg_0")
+        , (.eq1 d, .var "$arg_1") ] ]
+
+-- ── §5. Type-level helpers ─────────────────────────────────────────────────
+
+/-- The `CType` for natural numbers. -/
+@[inline] def CType.natC : CType := .ind natSchema []
+
+/-- The `CType` for booleans. -/
+@[inline] def CType.boolC : CType := .ind boolSchema []
+
+/-- The `CType` for lists with element type `A`. -/
+@[inline] def CType.listC (A : CType) : CType := .ind listSchema [A]
+
+/-- The `CType` for the circle. -/
+@[inline] def CType.s1C : CType := .ind s1Schema []
+
+/-- The `CType` for the interval. -/
+@[inline] def CType.intervalC : CType := .ind intervalSchema []
+
+/-- The `CType` for propositional truncation `‖A‖₋₁`. -/
+@[inline] def CType.propTruncC (A : CType) : CType :=
+  .ind propTruncSchema [A]
+
+-- ── §6. Term-level helpers ─────────────────────────────────────────────────
+
+namespace CTerm
+
+/-- The `CTerm` `zero : Nat`. -/
+@[inline] def zeroC : CTerm := .ctor natSchema "zero" [] []
+
+/-- The `CTerm` `succ n` for a given `n : Nat`. -/
+@[inline] def succC (n : CTerm) : CTerm := .ctor natSchema "succ" [] [n]
+
+/-- The `CTerm` `false : Bool`. -/
+@[inline] def falseC : CTerm := .ctor boolSchema "false" [] []
+
+/-- The `CTerm` `true : Bool`. -/
+@[inline] def trueC  : CTerm := .ctor boolSchema "true"  [] []
+
+/-- The `CTerm` `nil : List A`.  Carries the element type as parameter. -/
+@[inline] def nilC (A : CType) : CTerm := .ctor listSchema "nil" [A] []
+
+/-- The `CTerm` `cons x xs : List A`. -/
+@[inline] def consC (A : CType) (x xs : CTerm) : CTerm :=
+  .ctor listSchema "cons" [A] [x, xs]
+
+/-- The `CTerm` `base : S¹`. -/
+@[inline] def baseC : CTerm := .ctor s1Schema "base" [] []
+
+/-- The `CTerm` `loop @ r : S¹` where `r : DimExpr`. -/
+@[inline] def loopC (r : DimExpr) : CTerm :=
+  .ctor s1Schema "loop" [] [.dimExpr r]
+
+/-- The `CTerm` `inT a : ‖A‖₋₁`. -/
+@[inline] def inTC (A : CType) (a : CTerm) : CTerm :=
+  .ctor propTruncSchema "inT" [A] [a]
+
+/-- The `CTerm` `squash x y @ r : ‖A‖₋₁`. -/
+@[inline] def squashC (A : CType) (x y : CTerm) (r : DimExpr) : CTerm :=
+  .ctor propTruncSchema "squash" [A] [x, y, .dimExpr r]
+
+/-- Build a Nat literal `n` as a tower of `succ`s on `zero`. -/
+def natLit : Nat → CTerm
+  | 0     => zeroC
+  | n + 1 => succC (natLit n)
+
+end CTerm
+
+-- ── §7. Eliminator builders ────────────────────────────────────────────────
+
+/-- Build an `indElim` for `Nat`.  `motive` is the result type-former,
+    `caseZero` the body for `zero`, `caseSucc` the body for `succ`
+    (curried as `λ pred ih. body`).  `target` is the natural being
+    eliminated. -/
+def natElim (motive caseZero caseSucc target : CTerm) : CTerm :=
+  .indElim natSchema [] motive
+    [("zero", caseZero), ("succ", caseSucc)] target
+
+/-- Build an `indElim` for `Bool`. -/
+def boolElim (motive caseFalse caseTrue target : CTerm) : CTerm :=
+  .indElim boolSchema [] motive
+    [("false", caseFalse), ("true", caseTrue)] target
+
+/-- Build an `indElim` for `List A`.  `caseCons` is curried as
+    `λ head tail ih. body`. -/
+def listElim (A : CType) (motive caseNil caseCons target : CTerm) : CTerm :=
+  .indElim listSchema [A] motive
+    [("nil", caseNil), ("cons", caseCons)] target
+
+end CubicalTransport.Inductive

native/cubical/src/eval.rs

@@ -205,10 +205,135 @@ pub fn eval(env: LeanObj, t: LeanObj) -> LeanObjMut {
                 }
             }
         }
+        TERM_DIMEXPR => {
+            // .dimExpr r — lift to .vdimExpr r.
+            let r = ctor_field(t, 0);
+            retain(r);
+            mk_vdimexpr(r)
+        }
+        TERM_CTOR => {
+            // .ctor S c params args — produce canonical .vctor with each
+            // arg evaluated.  Path-ctor boundary firing is REL1.1 work.
+            let schema = ctor_field(t, 0);
+            let name = ctor_field(t, 1);
+            let params = ctor_field(t, 2);
+            let args_term = ctor_field(t, 3);
+            retain(schema); retain(name); retain(params);
+            let args_val = eval_term_list(env, args_term);
+            mk_vctor(schema, name, params, args_val as LeanObj)
+        }
+        TERM_INDELIM => {
+            // .indElim S params motive branches target — β-reduce on a
+            // canonical vctor target; otherwise build .nIndElim stuck.
+            let schema = ctor_field(t, 0);
+            let params = ctor_field(t, 1);
+            let motive = ctor_field(t, 2);
+            let branches = ctor_field(t, 3);
+            let target = ctor_field(t, 4);
+            let target_val = eval(env, target);
+            let target_tag = ctor_tag(target_val as LeanObj);
+            if target_tag == VAL_VCTOR {
+                // Canonical β: find branch matching the ctor's name,
+                // apply branch body to each ctor arg via vapp chain.
+                let ctor_name = ctor_field(target_val as LeanObj, 1);
+                let ctor_args = ctor_field(target_val as LeanObj, 3);
+                match find_branch_body(branches, ctor_name) {
+                    Some(body) => {
+                        retain(body);
+                        let mut acc = eval(env, body);
+                        let mut cur = ctor_args;
+                        while ctor_tag(cur) == 1 {
+                            let head = ctor_field(cur, 0);
+                            retain(head);
+                            acc = vapp(acc, head as LeanObjMut);
+                            cur = ctor_field(cur, 1);
+                        }
+                        release(target_val as LeanObj);
+                        acc
+                    }
+                    None => {
+                        release(target_val as LeanObj);
+                        stuck_marker(b"<indElim: no matching branch>\0")
+                    }
+                }
+            } else if target_tag == VAL_VNEU {
+                // Stuck: extract inner neutral, build .nIndElim with
+                // env-evaluated motive and branches.
+                let inner_neu = ctor_field(target_val as LeanObj, 0);
+                retain(inner_neu);
+                let motive_val = eval(env, motive);
+                let branches_val = eval_branches(env, branches);
+                retain(schema); retain(params);
+                release(target_val as LeanObj);
+                let nelim = mk_nindelim(schema, params, motive_val as LeanObj,
+                                         branches_val as LeanObj, inner_neu);
+                mk_vneu(nelim as LeanObj)
+            } else {
+                release(target_val as LeanObj);
+                stuck_marker(b"<indElim: target not canonical>\0")
+            }
+        }
         _ => stuck_marker(b"<eval: unknown CTerm tag>\0"),
     }
 }
 
+/// Walk a Lean `List CTerm`, eval each element, return a new
+/// `List CVal`.  Cons-list shape: tag 0 = nil, tag 1 = cons (head, tail).
+fn eval_term_list(env: LeanObj, terms: LeanObj) -> LeanObjMut {
+    if ctor_tag(terms) == 0 {
+        retain(terms);
+        terms as LeanObjMut
+    } else {
+        let head = ctor_field(terms, 0);
+        let tail = ctor_field(terms, 1);
+        let head_val = eval(env, head);
+        let tail_vals = eval_term_list(env, tail);
+        let cons = alloc_ctor(1, 2);
+        ctor_set_field(cons, 0, head_val as LeanObj);
+        ctor_set_field(cons, 1, tail_vals as LeanObj);
+        cons
+    }
+}
+
+/// Walk a Lean `List (String × CTerm)`, eval each body, return
+/// `List (String × CVal)`.
+fn eval_branches(env: LeanObj, brs: LeanObj) -> LeanObjMut {
+    if ctor_tag(brs) == 0 {
+        retain(brs);
+        brs as LeanObjMut
+    } else {
+        let head = ctor_field(brs, 0);
+        let tail = ctor_field(brs, 1);
+        let name = ctor_field(head, 0);
+        let body = ctor_field(head, 1);
+        let body_val = eval(env, body);
+        retain(name);
+        let new_pair = alloc_ctor(0, 2);  // Prod.mk
+        ctor_set_field(new_pair, 0, name);
+        ctor_set_field(new_pair, 1, body_val as LeanObj);
+        let tail_vals = eval_branches(env, tail);
+        let cons = alloc_ctor(1, 2);
+        ctor_set_field(cons, 0, new_pair as LeanObj);
+        ctor_set_field(cons, 1, tail_vals as LeanObj);
+        cons
+    }
+}
+
+/// Look up a branch body in a `List (String × CTerm)` by ctor name.
+/// Returns the borrowed CTerm body if found.
+fn find_branch_body(brs: LeanObj, target_name: LeanObj) -> Option<LeanObj> {
+    let mut cur = brs;
+    while ctor_tag(cur) == 1 {
+        let head = ctor_field(cur, 0);
+        let name = ctor_field(head, 0);
+        if unsafe { lean_string_eq(name, target_name) } {
+            return Some(ctor_field(head, 1));
+        }
+        cur = ctor_field(cur, 1);
+    }
+    None
+}
+
 // ── vApp ────────────────────────────────────────────────────────────────────
 
 /// `vApp : CVal → CVal → CVal` — function application.

native/cubical/src/readback.rs

@@ -196,6 +196,42 @@ pub(crate) fn mk_term_snd(inner: LeanObj) -> LeanObjMut {
     ctor
 }
 
+/// `.dimExpr r` — REL1.
+#[inline]
+pub(crate) fn mk_term_dimexpr(r: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(TERM_DIMEXPR, 1);
+    ctor_set_field(ctor, 0, r);
+    ctor
+}
+
+/// `.ctor S c params args` — REL1 schema constructor application.
+#[inline]
+pub(crate) fn mk_term_ctor(
+    schema: LeanObj, name: LeanObj, params: LeanObj, args: LeanObj,
+) -> LeanObjMut {
+    let ctor = alloc_ctor(TERM_CTOR, 4);
+    ctor_set_field(ctor, 0, schema);
+    ctor_set_field(ctor, 1, name);
+    ctor_set_field(ctor, 2, params);
+    ctor_set_field(ctor, 3, args);
+    ctor
+}
+
+/// `.indElim S params motive branches target` — REL1.
+#[inline]
+pub(crate) fn mk_term_indelim(
+    schema: LeanObj, params: LeanObj, motive: LeanObj,
+    branches: LeanObj, target: LeanObj,
+) -> LeanObjMut {
+    let ctor = alloc_ctor(TERM_INDELIM, 5);
+    ctor_set_field(ctor, 0, schema);
+    ctor_set_field(ctor, 1, params);
+    ctor_set_field(ctor, 2, motive);
+    ctor_set_field(ctor, 3, branches);
+    ctor_set_field(ctor, 4, target);
+    ctor
+}
+
 /// CType `.univ` — nullary scalar.
 #[inline]
 pub(crate) fn mk_ty_univ() -> LeanObjMut { lean_box_mut(TY_UNIV as usize) }
@@ -477,6 +513,21 @@ pub fn readback(v: LeanObj) -> LeanObjMut {
             let bt = readback(b);
             mk_term_pair(at as LeanObj, bt as LeanObj)
         }
+        VAL_VCTOR => {
+            // `.vctor S c params args` — readback each arg, rebuild .ctor.
+            let schema = ctor_field(v, 0);
+            let name = ctor_field(v, 1);
+            let params = ctor_field(v, 2);
+            let args_val = ctor_field(v, 3);
+            retain(schema); retain(name); retain(params);
+            let args_term = readback_val_list(args_val);
+            mk_term_ctor(schema, name, params, args_term as LeanObj)
+        }
+        VAL_VDIMEXPR => {
+            let r = ctor_field(v, 0);
+            retain(r);
+            mk_term_dimexpr(r)
+        }
         _ => {
             // Malformed — return a marker var.
             let msg = unsafe {
@@ -582,6 +633,21 @@ pub fn readback_neu(n: LeanObj) -> LeanObjMut {
             let inner_term = readback_neu(inner);
             mk_term_snd(inner_term as LeanObj)
         }
+        NEU_NINDELIM => {
+            // .nIndElim S params motive branches target — readback to
+            // .indElim with each branch body read back.
+            let schema = ctor_field(n, 0);
+            let params = ctor_field(n, 1);
+            let motive = ctor_field(n, 2);
+            let branches = ctor_field(n, 3);
+            let target = ctor_field(n, 4);
+            retain(schema); retain(params);
+            let motive_term = readback(motive);
+            let branches_term = map_readback_branches(branches);
+            let target_term = readback_neu(target);
+            mk_term_indelim(schema, params, motive_term as LeanObj,
+                            branches_term as LeanObj, target_term as LeanObj)
+        }
         _ => {
             let msg = unsafe {
                 lean_mk_string(b"<readbackNeu: unknown CNeu>\0".as_ptr() as *const core::ffi::c_char)
@@ -591,6 +657,52 @@ pub fn readback_neu(n: LeanObj) -> LeanObjMut {
     }
 }
 
+/// Map `readback` over a `List CVal`, producing a `List CTerm` —
+/// used to read back the args of a `.vctor`.
+fn readback_val_list(vals: LeanObj) -> LeanObjMut {
+    match ctor_tag(vals) {
+        LIST_NIL => lean_box_mut(LIST_NIL as usize),
+        LIST_CONS => {
+            let head = ctor_field(vals, 0);
+            let tail = ctor_field(vals, 1);
+            let head_term = readback(head);
+            let tail_term = readback_val_list(tail);
+            let cons = alloc_ctor(LIST_CONS, 2);
+            ctor_set_field(cons, 0, head_term as LeanObj);
+            ctor_set_field(cons, 1, tail_term as LeanObj);
+            cons
+        }
+        _ => lean_box_mut(LIST_NIL as usize),
+    }
+}
+
+/// Map `readback` over a `List (String × CVal)`, producing a
+/// `List (String × CTerm)` — used by the `nIndElim` readback arm.
+fn map_readback_branches(brs: LeanObj) -> LeanObjMut {
+    match ctor_tag(brs) {
+        LIST_NIL => lean_box_mut(LIST_NIL as usize),
+        LIST_CONS => {
+            let head = ctor_field(brs, 0);
+            let name = ctor_field(head, 0);
+            let body_val = ctor_field(head, 1);
+            let tail = ctor_field(brs, 1);
+
+            retain(name);
+            let body_term = readback(body_val);
+            let new_pair = alloc_ctor(PROD_MK, 2);
+            ctor_set_field(new_pair, 0, name);
+            ctor_set_field(new_pair, 1, body_term as LeanObj);
+
+            let new_tail = map_readback_branches(tail);
+            let new_cons = alloc_ctor(LIST_CONS, 2);
+            ctor_set_field(new_cons, 0, new_pair as LeanObj);
+            ctor_set_field(new_cons, 1, new_tail as LeanObj);
+            new_cons
+        }
+        _ => lean_box_mut(LIST_NIL as usize),
+    }
+}
+
 /// Map `readback` over a `List (FaceFormula × CVal)`, producing a
 /// `List (FaceFormula × CTerm)` for use in a `.compN`.
 fn map_readback_clauses(clauses: LeanObj) -> LeanObjMut {

native/cubical/src/tags.rs

@@ -31,6 +31,7 @@ pub const TY_PI:    u32 = 1;
 pub const TY_PATH:  u32 = 2;
 pub const TY_SIGMA: u32 = 3;
 pub const TY_GLUE:  u32 = 4;
+pub const TY_IND:   u32 = 5;  // REL1: schema-based inductive type
 
 // ── CTerm (Cubical/Syntax.lean) ────────────────────────────────────────────
 
@@ -47,6 +48,9 @@ pub const TERM_UNGLUE:  u32 = 9;
 pub const TERM_PAIR:    u32 = 10;
 pub const TERM_FST:     u32 = 11;
 pub const TERM_SND:     u32 = 12;
+pub const TERM_DIMEXPR: u32 = 13;  // REL1: dim expression lifted to CTerm
+pub const TERM_CTOR:    u32 = 14;  // REL1: schema constructor application
+pub const TERM_INDELIM: u32 = 15;  // REL1: inductive eliminator
 
 // ── CEnv (Cubical/Value.lean) ──────────────────────────────────────────────
 
@@ -64,17 +68,20 @@ pub const VAL_VTUBEAPP:    u32 = 5;
 pub const VAL_VCOMPFUN:    u32 = 6;
 pub const VAL_VPATHTRANSP: u32 = 7;
 pub const VAL_VPAIR:       u32 = 8;
+pub const VAL_VCTOR:       u32 = 9;   // REL1: canonical schema-ctor value
+pub const VAL_VDIMEXPR:    u32 = 10;  // REL1: lifted dim-expression value
 
 // ── CNeu (Cubical/Value.lean) ──────────────────────────────────────────────
 
-pub const NEU_NVAR:    u32 = 0;
+pub const NEU_NVAR:     u32 = 0;
-pub const NEU_NAPP:    u32 = 1;
+pub const NEU_NAPP:     u32 = 1;
-pub const NEU_NPAPP:   u32 = 2;
+pub const NEU_NPAPP:    u32 = 2;
-pub const NEU_NTRANSP: u32 = 3;
+pub const NEU_NTRANSP:  u32 = 3;
-pub const NEU_NCOMP:   u32 = 4;
+pub const NEU_NCOMP:    u32 = 4;
-pub const NEU_NHCOMP:  u32 = 5;
+pub const NEU_NHCOMP:   u32 = 5;
-pub const NEU_NCOMPN:  u32 = 6;
+pub const NEU_NCOMPN:   u32 = 6;
-pub const NEU_NGLUEIN: u32 = 7;
+pub const NEU_NGLUEIN:  u32 = 7;
-pub const NEU_NUNGLUE: u32 = 8;
+pub const NEU_NUNGLUE:  u32 = 8;
-pub const NEU_NFST:    u32 = 9;
+pub const NEU_NFST:     u32 = 9;
-pub const NEU_NSND:    u32 = 10;
+pub const NEU_NSND:     u32 = 10;
+pub const NEU_NINDELIM: u32 = 11;  // REL1: stuck inductive eliminator

native/cubical/src/value.rs

@@ -214,6 +214,44 @@ pub(crate) fn mk_nsnd(n: LeanObj) -> LeanObjMut {
     ctor
 }
 
+/// `.vctor S c params args` — canonical schema-constructor value (REL1).
+/// Takes ownership of all four field handles.
+#[inline]
+pub(crate) fn mk_vctor(
+    schema: LeanObj, name: LeanObj, params: LeanObj, args: LeanObj,
+) -> LeanObjMut {
+    let ctor = alloc_ctor(VAL_VCTOR, 4);
+    ctor_set_field(ctor, 0, schema);
+    ctor_set_field(ctor, 1, name);
+    ctor_set_field(ctor, 2, params);
+    ctor_set_field(ctor, 3, args);
+    ctor
+}
+
+/// `.vdimExpr r` — dim-expression lifted to the value level (REL1).
+#[inline]
+pub(crate) fn mk_vdimexpr(r: LeanObj) -> LeanObjMut {
+    let ctor = alloc_ctor(VAL_VDIMEXPR, 1);
+    ctor_set_field(ctor, 0, r);
+    ctor
+}
+
+/// `.nIndElim S params motive branches target` — stuck eliminator
+/// neutral.  Five fields per the Lean definition.
+#[inline]
+pub(crate) fn mk_nindelim(
+    schema: LeanObj, params: LeanObj, motive: LeanObj,
+    branches: LeanObj, target: LeanObj,
+) -> LeanObjMut {
+    let ctor = alloc_ctor(NEU_NINDELIM, 5);
+    ctor_set_field(ctor, 0, schema);
+    ctor_set_field(ctor, 1, params);
+    ctor_set_field(ctor, 2, motive);
+    ctor_set_field(ctor, 3, branches);
+    ctor_set_field(ctor, 4, target);
+    ctor
+}
+
 // ── Environment operations ─────────────────────────────────────────────────
 
 /// `CEnv.cons name val rest` — extend env with a new binding.