Detailed three-phase plan for the next stratum past REL1:
1. CType.interval primitive (1-2d) — the river-bed under every
dim-flowing computation. Promotes .dimExpr from .univ
placeholder to .interval typing.
2. Bridge.lean (Eq ↔ Path interop, 3-5d) — the ferry between
Lean's discrete equality and the embedded cubical Path.
Default CubicalEmbed instances for Bool, Nat, List, Prod;
forward bridge always available, backward restricted to
neutral-free paths in REL2.0 (full Glue NbE deferred to
REL2.1).
3. paideia K7 literal cubical encoding (5-10d) — the carrying
load. Replaces MathPath p₀ p₁ with a CTerm-typed
Path between two embedded MasteryProvenance traces.
Closes engine issue #1 with the originating use case.
Covers acceptance criteria, risk register, sequencing graph
(engine → topolei → paideia, no cycle), Rust ABI bump 2→3,
post-REL2 deferral list (REL2.1 Glue NbE / pointwise dist,
REL3 numerical layer, REL3+ higher cells, REL4 GPU/interaction).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Typing.lean: minimal-viable typing rules for the three new CTerm
constructors (REL1 first cut; REL2 will refine to dependent
formulations).
- HasType.ctor : .ctor S c params args : .ind S params
(no per-arg premises; runtime enforces)
- HasType.indElim : non-dependent form — motive : .pi (.ind …) C,
result : C; branch coherence checked at eval
- HasType.dimExpr : placeholder typing at .univ (real interval-
typing requires a CType.interval primitive,
deferred to REL2)
HasType.weaken_core extended with the three new arms.
TransportLaws.lean: derived theorems for transport over .ind (T1,
T2, stuck), all reducing to existing axioms (eval_transp_top,
eval_transp_const, eval_transp_nonpath + vTransp_stuck). Pointwise
distribution through ctor args is REL1.1 future work.
CompLaws.lean: derived theorems for composition over .ind (C1, C2,
const-line, stuck) — corollaries of the existing eval_comp_*
axioms. Same REL1.1 deferral for pointwise distribution.
native/cubical/src/subst.rs: critical Rust fix. The previous
fallback `_ => mk_term_var(ctor_field(t, 0))` corrupted the new
TERM_DIMEXPR / TERM_CTOR / TERM_INDELIM tags by extracting field 0
(a CTypeSchema for ctor) and wrapping it as a malformed .var,
causing infinite recursion / OOM in subst-driven paths
(eval_comp_top calls substDim). Proper arms for all three new
tags + cterm_subst_dim_list and cterm_subst_dim_branches helpers.
Unknown-tag fallback now safely returns the input unchanged
instead of synthesising a malformed .var.
FFITest.lean: three new smoke arms exercising T1/T2 transport and
C1 composition over .ind natC. Result: 28/28 smoke + 46/46
properties = 74/74.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds schema-based inductive type encoding to the engine, supporting both
plain inductives (Nat, List, Bool) and HITs (S¹, propositional truncation,
suspensions) via a single CTypeSchema/CtorSpec/CTypeArg structure.
New CType constructor:
- .ind (S : CTypeSchema) (params : List CType)
New CTerm constructors:
- .dimExpr (r : DimExpr)
- .ctor (S, ctorName, params, args)
- .indElim (S, params, motive, branches, target)
New CVal constructors:
- .vctor (S, ctorName, params, evaluatedArgs)
- .vdimExpr (DimExpr)
New CNeu constructor:
- .nIndElim (S, params, motive, branches, neuTarget)
Five-way mutual block in Syntax.lean (CType, CTerm, CTypeArg, CtorSpec,
CTypeSchema) with Repr derivation post-hoc. Tag layout per
docs/INDUCTIVE_TYPES.md §6: old tags preserved (no shifting). Existing
62/62 smoke + property tests pass unchanged through Rust.
Substitution / dim-absent / endpoint handling:
Subst.lean — substDim, substDimExpr, equation lemmas,
substDim_eq_substDimExpr (mutual with .params helpers).
DimLine.lean — CTerm.dimAbsent + CType.dimAbsent (mutual w/ helpers
for list / branches / params). Plus all five
auxiliary mutual blocks: substDim_absent_aux,
substDimExpr_absent_aux, dimAbsent_after_substDim_aux,
substDim_comm_aux — for both CTerm and CType.
Eval.lean: ctor → vctor (eval'd args); indElim β-reduces on canonical
vctor target via vApp chain over branch body, otherwise stuck via
.nIndElim; dimExpr → vdimExpr. Path-ctor boundary firing and
recursive-arg IH wiring marked TODO REL1.1 (β-reduction works for
non-recursive ctors today).
Readback.lean: vctor → .ctor, vdimExpr → .dimExpr, nIndElim → .indElim.
FFITest.lean: cvalSummary / ctermSummary extended with new constructor
arms.
Topolei (sibling repo) has not yet been migrated — see
docs/INDUCTIVE_TYPES.md §9.1 for the per-file impact map.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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>
- LICENSE: proprietary, all rights reserved. Public availability of
the repo grants no license; use requires written consent from
mgorog@gmail.com.
- README: "Reusing this engine" → "Consuming the engine (with
permission)" with explicit pointer to LICENSE.
- CI: workflow moved from .github/workflows/ to .forgejo/workflows/
so forgejo's runner picks it up. Workflow now also installs Rust,
builds native/cubical/, and runs cubical-test (62/62 verification)
rather than only running lake build (which would have failed at
link time without libtopolei_cubical.a).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Standard convention: README.md at root, everything else in docs/.
Engine docs/: FFI_DESIGN, FFI_COMPLETENESS, KERNEL_BOUNDARY, NUMERICAL,
PHASE1_HISTORY, ZIGZAG_PORT. README.md links updated to docs/<name>.
Cross-repo reference in NUMERICAL.md (to topolei's STATUS.md) now
includes the relative path `../topolei/docs/STATUS.md`.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- TRANSPORT_PLAN.md → PHASE1_HISTORY.md with archival header.
Path references updated from `Topolei/Cubical/*` to
`CubicalTransport/*` to match the post-split namespace.
Methodology preserved as a template for future formalisation phases.
- ZIGZAG_PORT.md moved here from topolei. This is engine code: the
port lands in `CubicalTransport/Zigzag/`, and an AI shortcut on
normalisation, degeneracy, or signature-typechecking would
cascade-corrupt every higher-cell proof in topolei. Added a
cascade caveat header explaining how engine-level zigzag changes
ripple back into the topolei interface repo. Body updated for
split context.
- KERNEL_BOUNDARY.md: clarified that the planned `Eq ↔ Path` bridge
module is distinct from the existing trace bridge
(`Topolei/Cubical/Trace.lean` in topolei).
- README.md: refreshed Reference section with renames + new docs.
- native/cubical/README.md: path refs updated.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Restructure to engine-only contents. Application code (Topolei.*
namespace, canvas-rs / render Rust crates, Main / ProbeTest, naga IR
pipeline, Selection / Subobject / Trace / Obs.Ctx hypothesis stack,
cells-spec / HYPOTHESES / STATUS / NAGA_IR_PLAN docs) moves to the
sibling repo max/topolei.
What moved:
- `Topolei/Cubical/*.lean` (22 files) → `CubicalTransport/*.lean`
with namespace `Topolei.Cubical.*` renamed to `CubicalTransport.*`.
Fully-qualified test types `TopoleiCubical{FFI,Property}Test` →
`CubicalTransport{FFI,Property}Test` for consistency.
- New root file `CubicalTransport.lean` re-exporting all 22 modules.
- Lakefile: package `cubicalTransport`; lib `CubicalTransport`; only
`cubical-test` and `cubical-bench` exes (no GPU link path).
The split criterion: anything an AI shortcut could break that would
cascade-corrupt downstream proofs lives here. Anything that would
only break the application stays in the topolei interface repo.
cubical-test passes 62/62 (smoke + properties) on the renamed engine.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Implements the cells-spec vision: a computation space that preserves
auditability, correctness, interactivity. Phase 1 (Lean kernel +
naga-IR Rust backend) is closed; foundation hypothesis stack
(Selection H1+H2, Subobject H3, Trace H5, Obs.Ctx C2, Cubical.Trace)
landed.
Highlights:
- Cubical-HoTT syntax + value/eval/readback in Lean
- naga-IR pipeline (no GLSL string crosses FFI; 17/17 probes pass)
- Honesty audit: every non-transport (sealed cells, vertex shader,
Y-flip, presentation conventions) is documented as such
- Polymorphic Trace α as free monoid; Cubical.Trace gives
CTerm → Trace CTerm by structural fold (homomorphism = definition)
- Selection as Huet zipper; Subobject as Boolean algebra over WCell
- All theorems proven; the proof IS the implementation
See STATUS.md for the resume guide.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
