Lean 4 cubical-transport HoTT engine + Rust naga-IR FFI. The backend that powers topolei. Cells-spec implementation; the proof IS the implementation.
391a048dcf
Some checks failed
Lean Action CI / build (push) Has been cancelled
Adds substantive content to Modal.lean §2a/§2b without discharging
the §3 adjoint theorems (which wait on FS-H18, see paired topolei
commit).
§2a — Unit/counit underlying CTerm constructions (substantive):
· flatSharpUnit : λ$a. modalIntro .sharp (modalIntro .flat $a)
— A → ♯(♭ A)
· flatSharpCounit: λ$x. modalElim .flat (λ$y. modalElim .sharp
(λ$z. $z) $y) $x
— ♭(♯ A) → A
· shapeFlatUnit : λ$a. modalIntro .flat (modalIntro .shape $a)
— A → ♭(ʃ A)
· shapeFlatCounit: λ$x. modalElim .shape (λ$y. modalElim .flat
(λ$z. $z) $y) $x
— ʃ(♭ A) → A
Reserved binders modalUnitVar / modalCounitVar / modalCounitInner /
modalCounitCore. Real CTerm bodies using actual modal constructors
(Phase 2 unification); no placeholders.
§2b — Constructive partial discharges (no FS-H18 needed, REAL proofs):
· 4 @[simp] rfl-lemmas: flatSharpUnit_eq / flatSharpCounit_eq /
shapeFlatUnit_eq / shapeFlatCounit_eq pinning each body.
· 4 typed-correctness theorems: flatSharpUnit_typed /
flatSharpCounit_typed / shapeFlatUnit_typed / shapeFlatCounit_typed
discharge HasType obligations via HasType.lam +
HasType.modalIntro (units) or chained HasType.modalElim with
explicit (var, A, C, k) annotations (counits).
· 4 non-vacuity / non-degeneracy theorems:
flatSharpUnit_ne_Counit, shapeFlatUnit_ne_Counit,
flatSharpUnit_ne_shapeFlatUnit, flatSharpCounit_ne_shapeFlatCounit
— distinct binder names / kind heads make the constructions
genuinely distinct (rules out vacuous defs).
§3 — Adjoint theorem annotations updated:
· flat_sharp_adjoint / shape_flat_adjoint / cohesive_triple sorry'd
with sharper FS-H18 attribution. Each annotation names the
§2a/§2b constructive partial discharges that ARE landed and
explains exactly what FS-H18 unlocks (CAdjoint instance via
triangle identities = Path-form of the modal β-rules).
· 3 sorries in proof positions (lines 880, 909, 985) — same count
as before, sharper attribution.
The CTerm un-indexed-by-universe nature of Syntax.lean §3 means
flatSharpUnit etc.'s (ℓ, A) arguments are formally unused in the
body; explicit `let _ := ℓ; let _ := A` makes this intentional and
keeps the signature aligned with the typed-correctness theorems.
Build: lake build (48 jobs) + lake build CubicalTransport (43 jobs)
PASS. Runtime: 49/49 + 46/46 = 95/95.
ZERO new sorries (the §2b theorems are all REAL proofs). ZERO
new noncomputable / Classical / axiom.
Modal.lean: 598 → 1026 lines (+428).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
||
|---|---|---|
| .forgejo/workflows | ||
| CubicalTransport | ||
| docs | ||
| native/cubical | ||
| .gitignore | ||
| build.sh | ||
| CubicalBench.lean | ||
| CubicalTest.lean | ||
| CubicalTransport.lean | ||
| lake-manifest.json | ||
| lakefile.toml | ||
| lean-toolchain | ||
| LICENSE | ||
| NOTICE | ||
| 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/libcubical_transport.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 siblingtopoleirepo.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 itsdocs/cells-spec.mdanddocs/STATUS.mdfor the application-side picture.