max/cubical-transport-hott-lean4
1
0
Fork 0
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions
Lean 4 cubical-transport HoTT engine + Rust naga-IR FFI. The backend that powers topolei. Cells-spec implementation; the proof IS the implementation.
12 commits 3 branches 0 tags 2.1 MiB
Find a file
Exact
Maximus Gorog 915b7b3b68
Some checks failed
Lean Action CI / build (push) Has been cancelled
Details
REL2 plan: interval primitive → Bridge → K7 cubical encoding 
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>
2026-04-30 18:36:58 -06:00
.forgejo/workflows Add proprietary LICENSE; move CI to .forgejo/workflows/, run cubical-test 2026-04-27 23:04:16 -06:00
CubicalTransport REL1: typing rules + transp/comp derived theorems for .ind + Rust subst 2026-04-30 18:05:32 -06:00
docs REL2 plan: interval primitive → Bridge → K7 cubical encoding 2026-04-30 18:36:58 -06:00
native/cubical REL1: typing rules + transp/comp derived theorems for .ind + Rust subst 2026-04-30 18:05:32 -06:00
.gitignore Initial commit: topolei — cubical-transport HoTT in Lean 4 + Rust FFI 2026-04-27 20:40:45 -06:00
build.sh Split: engine = cubical-transport HoTT only 2026-04-27 21:35:01 -06:00
CubicalBench.lean Split: engine = cubical-transport HoTT only 2026-04-27 21:35:01 -06:00
CubicalTest.lean Split: engine = cubical-transport HoTT only 2026-04-27 21:35:01 -06:00
CubicalTransport.lean REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46) 2026-04-30 15:15:50 -06:00
lake-manifest.json Regenerate lake-manifest.json: package name cubicalTransport (was stale 'topolei') 2026-04-27 23:00:01 -06:00
lakefile.toml Split: engine = cubical-transport HoTT only 2026-04-27 21:35:01 -06:00
lean-toolchain Initial commit: topolei — cubical-transport HoTT in Lean 4 + Rust FFI 2026-04-27 20:40:45 -06:00
LICENSE Add proprietary LICENSE; move CI to .forgejo/workflows/, run cubical-test 2026-04-27 23:04:16 -06:00
NOTICE Add NOTICE: AI tooling acknowledgement; proprietary rights stand on human-directed whole 2026-04-27 23:10:32 -06:00
README.md Add proprietary LICENSE; move CI to .forgejo/workflows/, run cubical-test 2026-04-27 23:04:16 -06:00

README.md

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:

[[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

(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 — the cells-spec workspace interface, built on this engine. See its docs/cells-spec.md and docs/STATUS.md for the application-side picture.