Lean 4 cubical-transport HoTT engine + Rust naga-IR FFI. The backend that powers topolei. Cells-spec implementation; the proof IS the implementation.
5de7d9e7d0
Some checks are pending
Lean Action CI / build (push) Waiting to run
THEORY.md §0.8 — first-class contracts as CType-typed predicates valued
in Ω, with a category of (CType, Contract instance)-pairs forming a topos.
## Architecture
def Contract (ℓ : ULevel) : Type := CType ℓ → CTerm
By convention, the output CTerm inhabits Ω ℓ. Each named contract
genuinely depends on its T input — no fun _ => stub-bodies in
substantive contracts; only the boundary Heyting elements (trivial_,
empty_) legitimately discard T.
## Per-contract structure CTypes (real Σ-towers)
CGroupStructCType T — 7-fold Σ over (mul, one, inv) + 4 group laws
(assoc, one_left, one_right, inv_left) as
Path equations referencing T's bound vars
CActionStructCType G T — Σ over (act : G → T → T) + composition law
CSiteStructCType T — Σ over (cov : T → T → Ω) + identity-cov law
CSheafStructCType _ _ — Σ over (presheaf, restriction coherence)
Every $-prefixed binder name in these towers is bound in its
surrounding sigmaSelf/piSelf enclosure — no free-variable placeholders.
## Named contracts
CubicalSetC ℓ — T is 0-truncated (Truncation.IsNType .zero T)
CGroupC ℓ — T carries a group (propTruncC of structure)
CActionC G_carrier — G acts on T (propTruncC of action structure)
CCoxeterC ℓ — T is a Coxeter system (refines on braid relations
downstream)
CSiteC ℓ — T is a Grothendieck site
CSheafC site value — sheaves on (site, value)
CModalC ℓ — T is the carrier of a modality
Boundary contracts:
Contract.trivial_ ℓ — every CType satisfies it (carrier = unitC)
Contract.empty_ ℓ — no CType satisfies it (carrier = botC ℓ)
Operators:
Contract.and / .or / .implies — pointwise lift of Ω.and / Ω.or / Ω.implies
## Naming reconciliation with Bridge/Set
Bridge.Set.CubicalSetC : Lean Prop existential
(∃ w, HasType [] w (IsNType .zero T))
Contract.CubicalSetC : Contract (CType → CTerm)
(T-dependent Ω-typed pair)
Both are valid forms of the same predicate. Bridge/Set's form is
used by the via_eq_contract tactic (Lean-level dispatch); Contract's
form is the topos-internal version usable inside cubical proofs.
Conversion lemmas connect them at use sites.
## Theorems (real Prop statements)
contracts_heyting (ℓ) — 4-clause conjunction of Path-equality in Ω ℓ
for ∧-idempotence, ∧-commutativity, modus
ponens, implication absorption
(sorry, waits on: Subobject.Ω_internal_logic_sound)
contracts_form_topos (ℓ) — ∃ CCategory ℓ + inclusion functor + non-
degeneracy clause
(sorry, waits on: Subobject.subobject_classifier
+ Category's pullback construction)
Both real Prop statements; no True := trivial, no tautological rfl.
## Discipline summary
· 2 sorries this round, both annotated -- waits on:
· Zero noncomputable / Classical.propDecidable
· Zero stub-bodies (every substantive contract uses T)
· Zero free-variable CTerm placeholders (only $-prefixed binders
declared in the same expression, plus $bogus non-degeneracy
placeholders following the Modality.adjoint_modal_triple pattern)
· No existing file modified
## Verification
lake build Build completed successfully (48 jobs)
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.