# cubical-transport-hott-lean4

A Lean 4 implementation of cubical-transport homotopy type theory
(CCHM-flavor), with a fast Rust kernel exposed through C ABI.

The Lean side defines the syntax, semantics, and soundness theorems.
The Rust side discharges the per-step β-rules of the evaluator.
Lean axioms are routed through `@[implemented_by]` to Rust functions
that return Lean objects in the same shape Lean would have produced;
the soundness layer (`CubicalTransport/Soundness.lean`) certifies the
backend at the boundary, so the kernel speed of the Rust code
preserves the Lean-level proofs.

## What's here

- `CubicalTransport/` — 22 Lean modules for syntax, substitution,
  dimensional structure, faces, typing, evaluation (eval / value /
  readback), transport, Glue, composition, and the soundness theorems.
- `native/cubical/` — Rust kernel (`#![no_std]`, dual-target native
  staticlib + cdylib, wasm32 cdylib).
- `CubicalTest.lean`, `CubicalBench.lean` — engine smoke + property
  tests (62/62 passing) and microbenchmarks.

## Consuming the engine (with permission)

This Software is **proprietary**.  See `LICENSE` — no use is granted
by virtue of the repository being public.  The instructions below
are for the copyright holder and any party with prior written consent
from `mgorog@gmail.com`.

Add as a Lake dependency from another Lean 4 project:

```toml
[[require]]
name = "cubicalTransport"
path = "../cubical-transport-hott-lean4"   # or git = "..."
```

Then `import CubicalTransport.Syntax`, `import CubicalTransport.Eval`,
etc.  Link against `native/cubical/target/release/libtopolei_cubical.a`
in your own `moreLinkArgs` so the FFI symbols resolve.

## Build

```bash
(cd native/cubical && cargo build --release)
lake build
./.lake/build/bin/cubical-test    # 62/62 tests pass
```

## Reference

- `docs/FFI_DESIGN.md` — C ABI contract between Lean and the Rust kernel.
- `docs/FFI_COMPLETENESS.md` — per-function axiom audit.
- `docs/KERNEL_BOUNDARY.md` — what this delivers in unmodified Lean 4 vs.
  what would need upstream Lean kernel work.
- `docs/NUMERICAL.md` — numerical implementation principles.
- `docs/PHASE1_HISTORY.md` — original transport/composition formalisation
  plan (archived; Phase 1 closed; preserved as methodology template
  for future phases).
- `docs/ZIGZAG_PORT.md` — step-by-step Lean port plan for the n-category
  combinatorial engine (Phase 2+ higher-cell backend).  Lands here
  in the engine.  **Read the cascade caveat at the top before
  editing**: changes in the ported zigzag layer cascade to the
  sibling `topolei` repo.
- `native/cubical/README.md` — Rust crate build + dev guide.
- `native/cubical/WASM.md` — wasm32 ABI integration contract.

## Used by

- [`max/topolei`](../topolei) — the cells-spec workspace interface,
  built on this engine.  See its `docs/cells-spec.md` and
  `docs/STATUS.md` for the application-side picture.