c2e3ecb3e3
Some checks are pending
Lean Action CI / build (push) Waiting to run
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>
1163 lines
69 KiB
Markdown
1163 lines
69 KiB
Markdown
# Topolei — Formal Status
|
||
|
||
*Last updated: 2026-04-24 (Phase 1 closed; Stages 1–4 delivered;
|
||
Rust backend Phases A–D all shipped. Rust cubical evaluator is
|
||
live in both native and wasm32 builds, wired via @[implemented_by],
|
||
verified by 55/55 smoke+property tests and baseline benchmarks.)*
|
||
|
||
---
|
||
|
||
## Resume guide (start here on a new session)
|
||
|
||
This document combines architecture, axiom inventory, historical logs, and
|
||
the next-action menu. For resuming work, read in this order:
|
||
|
||
1. **Architecture at a glance** (immediately below) — the Lean-as-host /
|
||
Rust-as-FFI-backend framing. Skip if already familiar.
|
||
2. **What is done** (jump to `## What is done` heading) — current module
|
||
inventory.
|
||
3. **Axiom discharge obligations** (`## Axiom discharge obligations`) —
|
||
the live list of what Rust must compute.
|
||
4. **Priority order** (`## Priority order`) — the menu of next-action
|
||
entry points across Streams A/B/C, with ✅ marks on completed items.
|
||
5. **Concrete "next session" suggestions** (last section) — curated
|
||
single/multi-session candidates.
|
||
|
||
Skip the per-week historical logs (the long block of "Phase 1 Week N"
|
||
sub-sections) unless tracing a specific past decision.
|
||
|
||
**Process discipline (do not violate):**
|
||
- Lean-first, Rust-second: every Rust-implemented behavior is *first*
|
||
stated in Lean as an axiom, *then* discharged. Adding eval/readback
|
||
axioms in Lean is the right move; writing Rust ahead of the spec is not.
|
||
- Face-disjoint axiom partitions: when extending a sub-case (e.g. Glue
|
||
transport), add new axioms with a precondition disjoint from existing
|
||
ones rather than rewriting the existing axiom. This keeps `transp_ua`
|
||
and similar consumers stable.
|
||
- NbE-first reductions: prefer eval-level + readback-level axioms over
|
||
step-level. After Stage 2.3 (subject reduction), **T3 and C4 are
|
||
theorems**, not step-level axioms; only T4 (`transp_plam_is_plam`)
|
||
remains as a syntactic fallback — all other step-level axioms are gone.
|
||
- **Axiom provenance discipline (Stage 3):** every axiom carries one of
|
||
three provenance tags — *Rust-discharge* (evaluator implementation),
|
||
*Lean-discharge* (future Lean proof from inductive definition), or
|
||
*IEEE/external* (Float / GPU spec). See "Axiom provenance spectrum"
|
||
section below.
|
||
|
||
---
|
||
|
||
## Architecture at a glance
|
||
|
||
**Topolei is a Lean 4 extension that adds cubical-transport HoTT to Lean 4
|
||
via a Rust FFI module.** The process discipline is:
|
||
|
||
1. **Formalize in Lean first.** Every layer that will eventually be
|
||
implemented in Rust — the cubical evaluator's reduction rules, the GPU
|
||
runtime's IO behavior, numerical kernels' input-output specs — is
|
||
*first* stated in Lean as axioms and data structures. No Rust is
|
||
written until the Lean-side axiom set is stable.
|
||
2. **Discharge via FFI later.** Rust functions, exposed through a C ABI,
|
||
are linked back into Lean via `@[extern]` + `@[implemented_by]`. Each
|
||
axiom becomes a kernel-trusted computation.
|
||
3. **Phase 1 (Cubical Core) is closed in Lean.** The six-week cubical
|
||
specification (Interval, Face, Syntax, Subst, DimLine, Typing, Value,
|
||
Eval, Transport, Comp, Equiv, Glue, Soundness, plus the EML and
|
||
GPU/Spec bridges) is complete with zero Rust dependency. Its axiom
|
||
set is the contract the Rust FFI will eventually satisfy.
|
||
4. **Many Lean-side phases don't need Rust.** Phase 2 (Cells), Phase 3a
|
||
(Reactive), Phase 3b (Color), Phase 4 Shader IR/emit, Phase 5b
|
||
Boundary/Security models, and Phase 6 Meta can all proceed as more
|
||
Lean — extending the axiom base. The Rust FFI unblocks *execution*
|
||
(GPU, window, OS), not *formalization*.
|
||
|
||
**The one Rust component has two distinct surfaces within it:**
|
||
|
||
- **(a) Cubical evaluator backend** — Rust implements `step`, `eval`,
|
||
`vApp`, `vPApp`, `vTransp`, `vHCompValue`, `vCompAtTerm`, `vCompNAtTerm`
|
||
+ the face-disjoint reduction rules for transp/comp/glue. Gives Lean's
|
||
kernel the ability to *reduce* cubical terms to values. **This is the
|
||
defining purpose of topolei's Rust FFI** — it exists to extend Lean 4
|
||
with computational cubical-transport HoTT.
|
||
- **(b) GPU / effectful runtime** — wgpu-backed GPU context, shader
|
||
upload/dispatch, window/input, OS primitives. Hosted in the same
|
||
Rust crate for build convenience; distinct FFI surface. Specs live
|
||
in `GPU/Spec.lean` + Phase 5 Runtime modules.
|
||
|
||
**Zigzag engine — Lean, not Rust.** The combinatorial n-category
|
||
engine (normalisation, degeneracy theory, type-checking against
|
||
signatures) is being ported into Lean. The Rust reference at
|
||
`zigzag-engine/` is a port-from template, not a dependency. See
|
||
`ZIGZAG_PORT.md` for the full 10-step plan. This preserves the
|
||
Lean-as-host discipline: reasoning inside Lean about n-categorical
|
||
normalisation requires structural access, which FFI hides.
|
||
|
||
**Numerical scheme discipline:** see `NUMERICAL.md` for the
|
||
context-from-content separation principle applied to numerical
|
||
implementations. Every scheme is a pair (mathematical content ×
|
||
execution context); they must not leak into each other, and §10
|
||
defines the minimum contract for first-class registry status.
|
||
|
||
---
|
||
|
||
## Audit summary
|
||
|
||
Post-review pass addressed a kernel-level soundness issue and cleaned up
|
||
abstractions across Phase 1. Changes:
|
||
|
||
- **Soundness:** `CTerm.step` is now `opaque` (was a concrete `def` with an
|
||
identity wildcard arm). Every axiom of the form `step (.transp …) = …` or
|
||
`step (.comp …) = …` was silently inconsistent with `CTerm.noConfusion`
|
||
under the old definition; opacity restores consistency. The path β-rule
|
||
is stated as an explicit axiom `step_papp_plam`.
|
||
- **CCHM alignment:** dropped the non-CCHM axiom `transp_as_comp` (T3) and
|
||
the misleading `transp_id_from_comp` derived theorem. `comp_top_const_id`
|
||
now requires `CTerm.dimAbsent i t = true` and is reproved via `comp_full` +
|
||
`substDimBool_of_absent`, with no appeal to T3.
|
||
- **Dead code:** collapsed identical `if j = i` branches in
|
||
`CTerm.substDim` (Syntax) and `CTerm.dimAbsent` (DimLine). Removed
|
||
tautology theorems `substDim_false_is_at0`/`substDim_true_is_at1`.
|
||
- **Abstraction:** removed useless hypotheses on `comp_full`
|
||
(`(φ : FaceFormula) (hφ : φ = .top)`) and `comp_empty`
|
||
(`Entails .bot .bot`). `comp_full_typed` now *actually* uses `comp_full`
|
||
(states typing for `substDimBool L.binder true u`, not for `step`).
|
||
`path_at_face_zero`/`one` removed (they took unused face hypotheses;
|
||
the unconditional `CTerm.step_papp_zero`/`one` in Syntax already
|
||
capture the content). `typing_plam_boundaries` renamed to
|
||
`plam_boundaries` and stripped of its unused typing hypothesis.
|
||
`System.typed_bot_vacuous` renamed to `System.typed_bot`.
|
||
|
||
### GPU bridge pass
|
||
|
||
- **Soundness (GPU side):** the old `compile_correct` axiom universally
|
||
quantified over both `expr` and `h`, so instantiating with two different
|
||
exprs at a shared `h` forced `expr₁.toColor = expr₂.toColor`. Replaced with
|
||
an abstract compile function `compileEML : EMLExpr → ShaderHandle` and a
|
||
per-handle correctness axiom `compileEML_correct`.
|
||
- **Rendering bridge:** added `EMLPath.evalAt_body_eq_at1` (scalar),
|
||
`EMLPath.toColor_body_eq_at1_toColor` (color), and `render_eq_at1`
|
||
(end-to-end). These close the cubical → Float → color → pixel chain.
|
||
- **Plot paths:** added `PlotConfig.dimName` and `PlotConfig.toEMLPath` in
|
||
EML/Path.lean. `plotExp` and `plotLn` are proved *constant paths* (their
|
||
bodies don't mention `"t"`); a genuinely parametric `plotExpT` demo was
|
||
added with proved endpoint values.
|
||
- **Last sorry discharged:** `evalAt_expOf` now closes against three IEEE 754
|
||
Float axioms (`Float.log_one`, `Float.max_one_ge_eps`, `Float.sub_zero`).
|
||
|
||
### Phase 1 Week 2: evaluator (cells-spec §5.4)
|
||
|
||
- **`Cubical/Value.lean`:** mutual `CEnv` / `CVal` / `CNeu` inductives
|
||
(named-variable adaptation of the spec's de-Bruijn `Env`/`Val`/`Neutral`).
|
||
`CVal` covers `vlam` closures, `vplam` dim-closures, and embedded `CNeu`;
|
||
`CNeu` covers free variables, stuck (p)apps, and stuck transport/comp.
|
||
- **`Cubical/Eval.lean`:** mutual `partial def` `eval` / `vApp` / `vPApp`
|
||
covering the λ-calculus fragment plus dimension application (β-reduces
|
||
via `CTerm.substDim`). Transport and composition produce `vneu` stuck
|
||
values (real reduction rules are Phase 1 Weeks 3–4). Eleven axiom
|
||
equations mirror the match arms so theorems can reduce through `eval`
|
||
without relying on `partial def`'s opaque kernel form — same pattern as
|
||
`opaque CTerm.step` + `step_papp_plam`.
|
||
- **`Cubical/EvalTest.lean`:** eight roundtrip tests — free variable,
|
||
identity β, constant-function β, K combinator (two β-reductions), stuck
|
||
application, path-abstraction closure, path β via `substDim`, transport
|
||
and composition neutralisation. All proved from the axiom equations.
|
||
|
||
### Phase 1 Week 3: transport at eval level (cells-spec §5.5)
|
||
|
||
**Full CCHM Π transport is implemented** — both constant-domain and
|
||
varying-domain cases. Delivers the "transport along refl = id" test
|
||
target (§13 Week 3) and the per-type-former Π rule.
|
||
|
||
#### Prerequisite: CType substitution by general DimExpr
|
||
|
||
- **`Cubical/Subst.lean`:** added `CType.substDimExpr : DimVar → DimExpr → CType → CType`
|
||
— generalises the existing Bool-only `CType.substDim` to arbitrary
|
||
`DimExpr`. Needed to build the reversed line `A[i := inv i]` for
|
||
inverse transport. Reduction lemmas `substDimExpr_univ/pi/path` and the
|
||
bridge `substDim_eq_substDimExpr` relating the two.
|
||
- **`Cubical/DimLine.lean`:** generalised `CTerm.substDim_of_absent` to
|
||
arbitrary `DimExpr` (the proof is the same as the old Bool case); added
|
||
`CType.substDimExpr_of_absent`. The old `substDimBool_of_absent` is now
|
||
a corollary.
|
||
|
||
#### Value-level machinery
|
||
|
||
- **`Cubical/Value.lean`:** `CVal.vTranspFun` now carries *both* domain
|
||
and codomain: `vTranspFun : DimVar → CType → CType → FaceFormula →
|
||
CVal → CVal`. A single uniform constructor handles the full CCHM Π
|
||
rule; the constant-domain specialisation falls out automatically from
|
||
`vTranspInv_const`.
|
||
- **`Cubical/Transport.lean`:**
|
||
- `vTransp i A φ v` dispatches in four priority-ordered arms:
|
||
1. `φ = .top` → `v` (T1).
|
||
2. `CType.dimAbsent i A = true` → `v` (T2).
|
||
3. `A = pi domA codA` → `vTranspFun i domA codA φ v` (**unified
|
||
full CCHM Π rule** — no longer gated by `dimAbsent i domA`).
|
||
4. Otherwise → stuck `vneu (.ntransp i A φ v)`.
|
||
- `vTranspInv i A φ v := vTransp i (A.substDimExpr i (.inv (.var i))) φ v`
|
||
— inverse transport as forward transport along the reversed line.
|
||
- Theorem `vTranspInv_const`: when `CType.dimAbsent i A = true`, the
|
||
reversed line equals the original (by `substDimExpr_of_absent`), so
|
||
`vTranspInv` reduces to `v` via T2.
|
||
- Theorem `vTranspInv_top`: `vTranspInv i A .top v = v`.
|
||
- Four axioms: `vTransp_top`, `vTransp_const`, `vTransp_pi` (new;
|
||
replaces the earlier `vTransp_pi_dom_const`), `vTransp_stuck`
|
||
(simplified precondition: "A is not a pi" replaces the earlier
|
||
"not a pi-with-constant-domain").
|
||
|
||
#### CCHM Π β-rule at the value level
|
||
|
||
- **`Cubical/Eval.lean`:** `vApp` on a transported function now performs
|
||
the full three-step CCHM reduction:
|
||
```
|
||
vApp (.vTranspFun i domA codA φ f) arg =
|
||
vTransp i codA φ (vApp f (vTranspInv i domA φ arg))
|
||
```
|
||
i.e. inverse-transport through the domain, apply the function,
|
||
forward-transport through the codomain. The axiom `vApp_vTranspFun`
|
||
is updated to match. Derived theorem `eval_transp_pi` replaces the
|
||
earlier `eval_transp_pi_dom_const`.
|
||
|
||
#### Tests
|
||
|
||
- `eval_transp_top_id`, `eval_transp_const_univ`, `eval_transp_const_pi`
|
||
— Week 3 "transport along refl = id".
|
||
- `eval_transp_pi_const_dom_example` — const-domain Π transport produces
|
||
`vTranspFun i .univ codA φ f`.
|
||
- `vApp_vTranspFun_const_dom_reduces` — applying it reduces through
|
||
`vTranspInv_const` (identity) + outer `vTransp_stuck`.
|
||
- `eval_transp_pi_varying_dom` — **varying-domain** Π transport also
|
||
produces `vTranspFun` (same constructor, no special case).
|
||
- `vApp_vTranspFun_varying_dom_reduces` — applying it cascades three
|
||
stuck neutrals: the inverse transport through the varying domain, the
|
||
stuck application, and the stuck forward transport through the
|
||
varying codomain.
|
||
|
||
### Correctness audit
|
||
|
||
The axiom set is provably disjoint by preconditions (top / const / pi /
|
||
stuck-non-pi), so no two axioms can fire with contradictory conclusions
|
||
on the same input. The unified `vTranspFun` constructor is
|
||
semantically well-behaved at every edge case:
|
||
|
||
- **Fully constant line** (caught by arm 2): `vTranspFun` isn't produced;
|
||
if manually constructed, `vApp` reduces it to `vApp f y` via the
|
||
two-sided `vTransp_const`/`vTranspInv_const` collapse.
|
||
- **Constant domain, varying codomain**: `vTranspInv` reduces to
|
||
identity, recovering the simpler formula `vTransp i codA φ (vApp f arg)`.
|
||
- **Varying domain**: the full CCHM three-step reduction runs; when
|
||
pieces stall, they stall consistently into nested `ntransp`/`napp`
|
||
neutrals.
|
||
- **Under `φ = .top`** (if manually constructed): reduces to `vApp f y`
|
||
via `vTransp_top` + `vTranspInv_top` — correct, since identity
|
||
transport of a function is the function.
|
||
|
||
### Phase 1 Week 4: composition at eval level
|
||
|
||
Heterogeneous composition at eval level plus homogeneous composition on
|
||
Π types — CCHM §5.6 delivered with working reductions for the cases that
|
||
don't require Glue.
|
||
|
||
#### Value-level machinery
|
||
|
||
- **`Cubical/Value.lean`:** two new `CVal` constructors + one `CNeu`:
|
||
- `vHCompFun : CType → FaceFormula → CVal → CVal → CVal` — result of
|
||
`hcomp (pi A B) φ tube base` at the value level. No domain stored
|
||
(homogeneous comp doesn't transport through the domain).
|
||
- `vTubeApp : CVal → CVal → CVal` — represents `λj. (tube @ j) arg`
|
||
as a dim-abstraction value. Needed to thread the outer hcomp's
|
||
tube into the inner hcomp on the codomain.
|
||
- `CNeu.nhcomp : CType → FaceFormula → CVal → CVal → CNeu` — stuck
|
||
hcomp (separate from `ncomp` because the type is fixed, not a line).
|
||
|
||
#### Evaluator extensions
|
||
|
||
- **`Cubical/Eval.lean`:** mutual block extended with two partial defs:
|
||
- `vHCompValue A φ tube base` — homogeneous composition on a fixed
|
||
type. Three disjoint arms: `.top → vPApp tube .one`, `.pi → vHCompFun`,
|
||
stuck otherwise.
|
||
- `vCompAtTerm env i A φ u t` — heterogeneous composition at the *term
|
||
level*. Takes `u` and `t` as `CTerm`s so that the `comp_full` case
|
||
can substitute `i := 1` before evaluating (this is genuinely different
|
||
from `vPApp`-ing the evaluated `u`). Four disjoint arms:
|
||
`.top → eval env (u[i := 1])` (C1), `.bot → eval env (.transp i A .bot t)` (C2),
|
||
`dimAbsent i A → vHCompValue A φ (vplam env i u) (eval env t)`
|
||
(hetero-comp ≡ hcomp on constant lines), stuck otherwise.
|
||
- `eval`'s `.comp` arm now routes through `vCompAtTerm`.
|
||
- `vApp` gains a `vHCompFun` case unfolding per the CCHM Π hcomp rule:
|
||
`vApp (.vHCompFun codA φ tube base) arg = vHCompValue codA φ (.vTubeApp tube arg) (vApp base arg)`.
|
||
- `vPApp` gains a `vTubeApp` case: `vPApp (.vTubeApp tube arg) r = vApp (vPApp tube r) arg`.
|
||
- Exhaustiveness cases for `vApp` on `vTubeApp` (type error) and
|
||
`vPApp` on `vHCompFun` (type error).
|
||
|
||
#### Axioms (all disjoint by precondition)
|
||
|
||
Old coarse `eval_comp` axiom replaced by four disjoint case-axioms:
|
||
- `eval_comp_top` — C1: `eval env (u.substDim i .one)`.
|
||
- `eval_comp_bot` — C2: `eval env (.transp i A .bot t)`.
|
||
- `eval_comp_const` — `dimAbsent i A → vHCompValue A φ (vplam env i u) (eval env t)`.
|
||
- `eval_comp_stuck` — fallback.
|
||
|
||
Three `vHCompValue_*`: `vHCompValue_top`, `vHCompValue_pi`, `vHCompValue_stuck`.
|
||
One each for `vApp` on `vHCompFun` (`vApp_vHCompFun`) and `vPApp` on
|
||
`vTubeApp` (`vPApp_vTubeApp`).
|
||
|
||
#### Tests
|
||
|
||
- `eval_comp_top_example` — C1 with a body with no dim dep → stripped to neutral.
|
||
- `eval_comp_top_dim_subst` — C1 with body `papp (var "p") i`; the `i := 1`
|
||
substitution hits `DimExpr.subst (var i)` which collapses to `DimExpr.one`,
|
||
yielding `npapp (nvar "p") .one`. **Exercises real dim substitution.**
|
||
- `eval_comp_bot_univ` — C2 chained with T2: `comp i .univ .bot u t` → `eval t`.
|
||
- `eval_comp_const_line` — constant-line comp reduces to hcomp; on `.univ`
|
||
the hcomp stalls into `nhcomp`.
|
||
- `eval_comp_neu` — stuck comp form (free vars, non-const non-endpoint face).
|
||
- `vHCompValue_top_reduces` — `hcomp .top` on a vplam tube returns the
|
||
tube-body at dim 1.
|
||
- `vApp_vHCompFun_reduces` — **CCHM Π hcomp β-rule** runs with neutral
|
||
tube/base/argument; cascades cleanly into `nhcomp` + `napp` neutrals.
|
||
- `vPApp_vTubeApp_reduces` — `(λj. tube@j arg) @ r` reduces to
|
||
`(tube@r) arg` using a vplam tube.
|
||
|
||
### C1 / C2 now discharged at eval level
|
||
|
||
`eval_comp_top` and `eval_comp_bot` are the eval-level analogues of the
|
||
step-level axioms `comp_full` (C1) and `comp_empty` (C2). Once a
|
||
`step ↔ eval` bridge is built, the step-level axioms can be derived from
|
||
these — one less foundational axiom each.
|
||
|
||
### Phase 1 Week 4+: Path transport (cells-spec §5.5 Path case)
|
||
|
||
Path transport of a path element `p : Path A(0) a(0) b(0)` along a line
|
||
`i. Path A(i) a(i) b(i)` produces an element of `Path A(1) a(1) b(1)`.
|
||
CCHM's rule uses a 3-clause heterogeneous comp with the system
|
||
`[φ ↦ p@j, j=0 ↦ a(i), j=1 ↦ b(i)]`. Full multi-clause comp is an
|
||
involved refactor; this pass delivers the **endpoint-accurate
|
||
reductions** (which cover the common case of evaluating paths at their
|
||
boundaries) and a **structured stuck form** for generic-dim applications
|
||
that preserves the transport data for possible future unsticking.
|
||
|
||
#### Value-level machinery
|
||
|
||
- **`Cubical/Value.lean`:**
|
||
- `CVal.vPathTransp : CEnv → DimVar → CType → CTerm → CTerm → FaceFormula → CVal → CVal`
|
||
— value-level representation of `transp^i (Path A(i) a(i) b(i)) φ p`.
|
||
Stores env (for later substDim on `a`, `b`), binder, base type,
|
||
endpoint CTerms, face, and the already-evaluated path value.
|
||
- `CNeu.npathTranspApp : ... → DimExpr → CNeu` — generic-dim stall,
|
||
structurally preserves the full transport data.
|
||
|
||
#### Evaluator refactor
|
||
|
||
- **`Cubical/Eval.lean`:** eval's `.transp` arm now dispatches in four
|
||
priority-ordered arms:
|
||
1. `φ = .top` → `eval env t` (T1, unconditional).
|
||
2. `CType.dimAbsent i A = true` → `eval env t` (T2, covers constant
|
||
lines of *any* head — univ, pi, path, sigma-when-we-have-it).
|
||
3. `A = .path A₀ a b` (line varies) → `vPathTransp` closure.
|
||
4. Otherwise → value-level `vTransp` (which handles `.pi` via
|
||
`vTranspFun`).
|
||
`vPApp` gains three new arms for `vPathTransp`:
|
||
· At `.zero` → `eval env (a.substDim i .one)` (= a(1) from CCHM
|
||
(j=0) clause).
|
||
· At `.one` → `eval env (b.substDim i .one)` (= b(1) from (j=1)).
|
||
· At generic DimExpr → `vneu (.npathTranspApp …)`.
|
||
`vApp` gains a `vPathTransp` case (type error — path values aren't
|
||
functions).
|
||
|
||
#### Axioms (all disjoint by precondition)
|
||
|
||
Old coarse `eval_transp` axiom replaced by four disjoint case-axioms:
|
||
- `eval_transp_top` (φ = .top).
|
||
- `eval_transp_const` (φ ≠ .top ∧ dimAbsent i A).
|
||
- `eval_transp_path` (φ ≠ .top ∧ path-line varies).
|
||
- `eval_transp_nonpath` (φ ≠ .top ∧ non-constant non-path).
|
||
|
||
Three axioms for `vPApp` on `vPathTransp`: `vPApp_vPathTransp_zero`,
|
||
`vPApp_vPathTransp_one`, `vPApp_vPathTransp_stuck` (r ≠ .zero ∧ r ≠ .one).
|
||
|
||
#### Tests
|
||
|
||
- `eval_transp_path_example` — transport along a varying path line
|
||
`path univ (var "a_line") (papp (var "b_pt") i)` produces the
|
||
expected `vPathTransp` closure.
|
||
- `vPApp_vPathTransp_zero_reduces` — endpoint at `.zero` yields `a(1)`.
|
||
Exercises `substDim i .one` on a constant endpoint term.
|
||
- `vPApp_vPathTransp_one_reduces` — endpoint at `.one` yields `b(1)`.
|
||
The `.papp (.var "b_pt") (DimExpr.var i)` endpoint has its `i` replaced
|
||
with `.one`, producing `npapp (nvar "b_pt") .one` — **real CCHM
|
||
endpoint correction firing through multiple layers**.
|
||
- `vPApp_vPathTransp_stuck_reduces` — at a fresh dim var, stalls at
|
||
`npathTranspApp` preserving all transport data.
|
||
- `eval_transp_constant_path` — when the path line is fully constant,
|
||
T2 fires and the transport is identity (no `vPathTransp` produced).
|
||
|
||
### Correctness audit for path transport
|
||
|
||
- **Axiom disjointness** — eval's four `.transp` axioms have preconditions
|
||
that partition the input space: `.top` / (non-top ∧ const) / (non-top
|
||
∧ non-const ∧ path) / (non-top ∧ non-const ∧ non-path). Similarly the
|
||
three `vPApp vPathTransp` axioms partition by `.zero`/`.one`/else.
|
||
- **Endpoint correctness** — the CCHM `(j=0)` clause specifies the value
|
||
at `j=0` to be `a(i)`; at the lid `i=1`, this is `a(1)`. Not
|
||
`transp^i(a(0))`, which is what a naïve approach would compute. Our
|
||
axiom directly gives the CCHM-correct value `eval env (a.substDim i .one)`.
|
||
- **Constant-line short-circuit** — when `dimAbsent i A = true` for
|
||
`A = .path A₀ a b`, CCHM transport is identity (T2). Our eval checks
|
||
this before the path routing, so no `vPathTransp` is constructed and
|
||
the result is plainly `eval env t`. Avoids producing a `vPathTransp`
|
||
that would need additional reduction machinery to recognize as identity.
|
||
- **φ = .top short-circuit** — similarly, the top face is caught before
|
||
path routing, so transport under `.top` is identity (T1) for path
|
||
types as for any other type. No `vPathTransp` is produced.
|
||
- **Stall preservation** — at generic dims, the `npathTranspApp` neutral
|
||
stores env, binder, types, endpoints, face, and path value. A later
|
||
substitution of a fresh dim with an endpoint can be propagated through
|
||
this neutral via the endpoint axioms — no data is lost.
|
||
|
||
### Phase 1 Week 4++: Multi-clause comp + full path transport
|
||
|
||
The **full CCHM machinery** for path transport is now in place — generic-dim
|
||
applications no longer stall blindly but produce a multi-clause `compN` that
|
||
genuinely unsticks when any clause face resolves to `.top` (via the new
|
||
`FaceFormula.dimExprEq0/1` helpers).
|
||
|
||
#### New machinery
|
||
|
||
**`Cubical/Face.lean`**:
|
||
- `FaceFormula.dimAbsent` (moved up from DimLine so it's visible at Face level).
|
||
- `FaceFormula.dimExprEq0 / dimExprEq1 : DimExpr → FaceFormula` — encoding
|
||
"r = 0" and "r = 1" as face formulas for composite DimExprs. Mutual
|
||
recursion (inv swaps them; meet/join de Morgan-dualise).
|
||
`_eval` theorems prove semantic correctness.
|
||
- `FaceFormula.substDim : DimVar → DimExpr → FaceFormula → FaceFormula` —
|
||
general substitution. Uses `dimExprEq0/1` for `eq0 j[j:=r]`/`eq1 j[j:=r]`.
|
||
- Supporting theorems: `substDim_zero/substDim_one` (agree with `restrict`),
|
||
`substDim_of_absent`, `substDim_comm`, `dimExprEq0_dimAbsent`/`dimExprEq1_dimAbsent`,
|
||
`dimExprEq0_substDim_of_absent`/`dimExprEq1_substDim_of_absent`,
|
||
`dimAbsent_after_substDim`.
|
||
|
||
**`Cubical/Interval.lean`**: `DimExpr.dimAbsent` relocated here.
|
||
|
||
**`Cubical/Syntax.lean`**:
|
||
- New CTerm constructor `compN : DimVar → CType → List (FaceFormula × CTerm) → CTerm → CTerm`.
|
||
- `CTerm.substDim` extended for `compN` via a mutual helper
|
||
`substDim.clauses` (so Lean can see structural termination through the
|
||
clause list).
|
||
- `transp` and `comp` now substitute into `FaceFormula` too (were previously
|
||
no-ops on `φ` — an approximation that could produce subtle bugs with
|
||
nested dim substitutions).
|
||
|
||
**`Cubical/DimLine.lean`**:
|
||
- `CTerm.dimAbsent` extended for `compN`, mutual helper `dimAbsent.clauses`.
|
||
- `CTerm.substDim_absent_aux`, `CTerm.dimAbsent_after_substDim_aux`,
|
||
`CTerm.substDim_comm_aux` all extended to handle `compN` via mutual
|
||
helpers for the clause-list case.
|
||
- Transp/comp proofs updated for the new face-formula substitution.
|
||
|
||
**`Cubical/Value.lean`**:
|
||
- `CNeu.ncompN` — stuck multi-clause comp neutral.
|
||
- `CVal.vPathTransp` changed to store the path as a `CTerm` (not CVal) —
|
||
needed so `.papp p r` terms can be constructed for the multi-clause
|
||
reduction.
|
||
- `CNeu.npathTranspApp` removed (no longer produced — path transport now
|
||
always reduces to `vCompNAtTerm`, which handles the stuck case itself).
|
||
|
||
**`Cubical/Eval.lean`**:
|
||
- Mutual block now has **six** partial defs: `eval`, `vApp`, `vPApp`,
|
||
`vHCompValue`, `vCompAtTerm`, `vCompNAtTerm`.
|
||
- `eval`'s `.compN` arm delegates to `vCompNAtTerm`.
|
||
- `vPApp` on `vPathTransp` at a generic DimExpr now routes through
|
||
`vCompNAtTerm` with the CCHM 3-clause system
|
||
`[(φ, p@r), (dimExprEq0 r, a), (dimExprEq1 r, b)]` and base `p@r`.
|
||
**This is the genuine CCHM path transport reduction, not a stall.**
|
||
- `vCompNAtTerm` priority-order arms:
|
||
· forcing `.top` clause anywhere in list → fires (substDim i .one in body).
|
||
· empty list → reduces to plain transport (C2).
|
||
· single live clause → delegates to `vCompAtTerm`.
|
||
· else → stuck `ncompN`.
|
||
- New axioms: `eval_compN`, `vCompNAtTerm_def` (compound axiom exposing
|
||
the full case analysis — users pattern-match on clause list).
|
||
- `vPApp_vPathTransp_general` replaces the old `vPApp_vPathTransp_stuck`
|
||
(now uses `vCompNAtTerm` reduction).
|
||
|
||
#### New tests
|
||
|
||
- `eval_compN_empty` — empty system compN reduces to transport.
|
||
- `eval_compN_top_fires` — top-clause at head fires (C1-like).
|
||
- `eval_compN_top_later` — top-clause deeper in list still fires
|
||
(`find?` scans past non-top clauses).
|
||
- `vPApp_vPathTransp_inv_zero` — **key correctness test**: applying path
|
||
transport at the composite DimExpr `.inv .zero` (semantically = 1)
|
||
exercises:
|
||
1. `dimExprEq0 (inv 0)` computes via the de Morgan case to
|
||
`dimExprEq1 .zero = .bot`.
|
||
2. `dimExprEq1 (inv 0)` computes to `dimExprEq0 .zero = .top`.
|
||
3. compN system `[(φ, _), (.bot, a), (.top, b)]` scanned by `find?`.
|
||
4. `.top`-faced clause fires → returns `b(1)` = `b.substDim i .one`.
|
||
5. `pathLine_b.substDim i_dim .one` = `papp (var "b_pt") .one`.
|
||
6. Evaluates to `vneu (npapp (nvar "b_pt") .one)`.
|
||
This is real CCHM reduction chaining through every new piece.
|
||
|
||
### Correctness audit for this pass
|
||
|
||
- **`FaceFormula.substDim` preserves semantic equality with `restrict`
|
||
at endpoints** — `substDim_zero/one = restrict false/true`. Full
|
||
semantic correctness proven via `dimExprEq0_eval` / `dimExprEq1_eval`
|
||
theorems (`dimExprEq0 r` evaluates to true iff `r` evaluates to false).
|
||
- **compN clause-list substitution commutes with disjoint dim vars** —
|
||
via `CTerm.substDim.clauses_comm_aux` (mutual with the CTerm case).
|
||
- **`.compN` dim-absence preserved by substitution** — via
|
||
`CTerm.dimAbsent.clauses_after_substDim` (mutual).
|
||
- **Face formulas now substituted in `.transp` and `.comp`** — closes a
|
||
prior gap where `transp i A φ t`'s dim-substitution left `φ` unchanged
|
||
even when `φ` mentioned the substituted var.
|
||
- **Path transport at endpoints still via specific axioms**
|
||
(`vPApp_vPathTransp_zero/one`) — semantic-equivalent shortcut to the
|
||
general compN reduction, skipping list-scan overhead.
|
||
|
||
### Phase 1 Week 5: Equivalences and Glue (cells-spec §5.7–§5.8)
|
||
|
||
**Equiv** (`Cubical/Equiv.lean`):
|
||
|
||
- `EquivData` — half-adjoint equivalence structure (HoTT §4.2) carrying
|
||
`f`, `fInv`, `sec`, `ret`, `coh` as raw `CTerm`s rather than a Σ-type
|
||
(sigma types aren't in `CType` yet; `fiberTy` / contractibility-of-fibers
|
||
deferred).
|
||
- `idEquiv : CType → EquivData` — trivial equivalence on any type;
|
||
uses reserved hygienic names `"$x"`, `⟨"$e"⟩`, `⟨"$eo"⟩`, `⟨"$ei"⟩`
|
||
for its bound vars (consistent with `"$y"`/`⟨"$fj"⟩` in `vApp vCompFun`).
|
||
- Five typing theorems proving `idEquiv` components are well-typed in any
|
||
context at their *propositionally-reduced* types (e.g. `sec : A → Path A x x`
|
||
rather than `A → Path A (f (fInv x)) x`). Same compromise as the
|
||
non-dependent Π restriction — β-equivalence isn't part of `HasType`.
|
||
|
||
**Glue** (`Cubical/Glue.lean` + extensions):
|
||
|
||
- New `CType` constructor `.glue (φ : FaceFormula) (T : CType)
|
||
(f fInv sec ret coh : CTerm) (A : CType)` — equivalence's five CTerms
|
||
inlined directly so the `CType`/`CTerm` mutual block remains closed
|
||
(not dependent on `EquivData`).
|
||
- New `CTerm` constructors `.glueIn (φ t a)` and `.unglue (φ f g)`.
|
||
- Threaded through the full pipeline: `CTerm.substDim` extended for both
|
||
new term constructors; `CType.substDim` / `CType.substDimExpr` / all
|
||
four `_aux` mutual defs in `DimLine.lean` extended for `.glue` on the
|
||
CType side and `.glueIn`/`.unglue` on the CTerm side.
|
||
- Two new `CNeu` constructors: `nglueIn` and `nunglue` — structured stuck
|
||
forms preserving both face-on and face-off evaluated sub-values, so
|
||
later dim substitution into `φ` can unstick them.
|
||
- `eval` on `.glueIn` / `.unglue` dispatches by face priority (top/bot/
|
||
stuck), mirrored by six face-disjoint axioms:
|
||
- `eval_glueIn_top` — `.glueIn .top t a → eval t`.
|
||
- `eval_glueIn_bot` — `.glueIn .bot t a → eval a`.
|
||
- `eval_glueIn_stuck` — non-top-non-bot produces `nglueIn`.
|
||
- `eval_unglue_top` — `.unglue .top f g → vApp f g` (forward map).
|
||
- `eval_unglue_bot` — `.unglue .bot f g → eval g` (identity).
|
||
- `eval_unglue_stuck` — non-top-non-bot produces `nunglue`.
|
||
- `EquivData.toGlueType (φ T e A)` — ergonomic wrapper inlining `e`'s
|
||
five CTerms into the `.glue` constructor.
|
||
- `uaLine e A B : DimExpr → CType` — single-face CCHM univalence line
|
||
`Glue [dimExprEq0 r ↦ (A, e)] B`. At `r = .zero`, `dimExprEq0 .zero = .top`,
|
||
so the glue is `A` via `e`; at `r = .one`, `dimExprEq0 .one = .bot`, so
|
||
the glue is `B`. Not a two-face symmetric ua (`Glue [i=0 ↦ (A, e),
|
||
i=1 ↦ (B, idEquiv)] B`); semantically equivalent but simpler.
|
||
- Endpoint rfl-lemmas `uaLine_zero / one / var`, plus computational
|
||
content theorems `uaLine_zero/one_glueIn/unglue_reduces` that derive
|
||
A-behaviour at `r=0` and B-behaviour at `r=1` from the face-disjoint
|
||
axioms.
|
||
|
||
### Correctness audit for Week 5
|
||
|
||
- **Axiom disjointness** — glueIn's three axioms partition by `.top` /
|
||
`.bot` / (non-top ∧ non-bot); unglue's three axioms similarly. No two
|
||
axioms for the same head can fire together.
|
||
- **Structured stucks** — `nglueIn` / `nunglue` preserve sub-values as
|
||
`CVal`s (not erased to neutrals). When dim substitution resolves the
|
||
stored `φ` to `.top` or `.bot`, a later pass can unstick by re-evaluating
|
||
through the endpoint axioms.
|
||
- **`CType.glue` in substitution machinery** — extended for `substDim`,
|
||
`substDimExpr`, `substDim_of_absent`, `substDimExpr_of_absent`,
|
||
`dimAbsent_after_substDim`, and `substDim_comm_aux`. All five threads
|
||
uniformly descend into the 5 inlined CTerms + T + A + φ.
|
||
- **Partial: Glue transport** — a restricted-form axiom
|
||
`eval_transp_glue_const_at_bot` (in `Glue.lean`) covers the case of an
|
||
empty outer face, constant-in-i fiber/base/equivalence components, and
|
||
inner glue face collapsing to `.bot` at `i := 1`. This discharges
|
||
`transp_ua` as a *theorem* (not axiom). The generalisation to varying
|
||
equivalences, varying base type, and non-`.bot` outer faces remains
|
||
Week 6+ work — extending this one axiom into a full CCHM §6.2 rule is
|
||
the first step toward a complete Glue reduction system.
|
||
- **Deferred: multi-face Glue** — a `.glueN` with a list of `(φ_k, T_k, e_k)`
|
||
clauses would let us write the full two-face CCHM ua. Single-face is
|
||
semantically equivalent and enough for Phase 1.
|
||
|
||
### Phase 1 Week 6 (2026-04-23): Glue transport — constant-component fragment
|
||
|
||
**`transp_ua` is now a theorem.** Glue transport is closed for the
|
||
"constant-non-φ-components" case — equivalences supplied from outside the
|
||
transport binder — modulo a single future-work gap (the `φ[i:=1] = .top`
|
||
sub-case, which needs the equivalence's half-adjoint hcomp construction).
|
||
|
||
Changes:
|
||
|
||
- **Eval.lean — `.transp` dispatch on `.glue`.** The `eval` partial def's
|
||
`.transp` arm now has a dedicated `.glue` case that produces a stuck
|
||
neutral as a runtime placeholder (the same shape `vTransp` would have
|
||
produced for glue). This separates `.glue` from the `_ => vTransp`
|
||
fallback so the new Glue-specific axioms don't collide with
|
||
`eval_transp_nonpath`.
|
||
- **Eval.lean — `eval_transp_nonpath` restricted.** Added an `h_not_glue`
|
||
precondition excluding `.glue` type heads. Without this, the new Glue
|
||
axioms would directly contradict `eval_transp_nonpath` + `vTransp_stuck`
|
||
on the `.glue` case. Downstream theorems `eval_transp_pi`,
|
||
`eval_transp_stuck`, and `EvalTest.eval_transp_neu` all propagate the
|
||
precondition.
|
||
- **Glue.lean — `eval_transp_glue_const_at_bot`.** When all non-φ
|
||
components are dim-absent from `i`, the outer face `ψ ≠ .top`, and the
|
||
inner face restricted to `i := 1` collapses to `.bot`, glue transport
|
||
reduces to `transp i A ψ (unglue (φ[i:=0]) f t)`. In the `uaLine`
|
||
setting (constant `A`, constant equivalence, `φ = eq0 i`), this chains
|
||
through `eval_transp_const` (T2) and `eval_unglue_top` to yield `e.f t`.
|
||
- **Glue.lean — `eval_transp_glue_const_stuck`.** When the inner face
|
||
restricted to `i := 1` is neither `.top` nor `.bot` (so the glueIn at
|
||
`i = 1` has a non-trivial face and the reduction can't collapse), the
|
||
result is a structured stuck neutral preserving the full glue data,
|
||
matching the partial def's runtime behavior. Disjoint from
|
||
`_at_bot` by the `φ[i:=1] ≠ .bot` precondition.
|
||
|
||
**Case-analysis status for constant non-φ components:**
|
||
|
||
| `φ.substDim i .one` | status | axiom / mechanism |
|
||
|---------------------|-------------|----------------------------------------------|
|
||
| `.bot` | ✅ covered | `eval_transp_glue_const_at_bot` |
|
||
| `.top` | ✅ covered | `eval_transp_glue_const_at_top` (Stream B #1a, 2026-04-23) |
|
||
| otherwise | ✅ covered | `eval_transp_glue_const_stuck` (stuck form) |
|
||
|
||
**Constant-component fragment is closed.** All three sub-cases of
|
||
`φ.substDim i .one` are face-disjoint axioms with documented discharge
|
||
obligations on the Rust backend. `transp_ua` and the new
|
||
`transp_ua_inverse` (Soundness.lean) demonstrate the `_at_bot` and
|
||
`_at_top` axioms firing through the canonical univalence-line shapes.
|
||
|
||
**New proof obligation on the Rust backend:** the full CCHM §6.2 Glue
|
||
transport formula, whose restriction to each covered sub-case must
|
||
produce the stated RHS. In particular the `_at_top` axiom states the
|
||
T-side witness as the *naïve* `app fInv (transp i A ψ (unglue …))`; the
|
||
full CCHM formula adds an hcomp-in-T correction using `sec` to enforce
|
||
ψ-boundary agreement, which trivialises under the constant-component
|
||
hypothesis up to the equivalence's propositional coherence (a
|
||
well-typedness obligation the caller already discharges).
|
||
|
||
**Remaining Glue-transport generalisations** (require more machinery):
|
||
- Varying base type `A`: replace the outer transport with a genuine
|
||
comp/fill through the base line (CCHM §6.2's first fill).
|
||
- Varying equivalence components `f(i)`, `fInv(i)`, etc.: use
|
||
`transp^i T` to transport witnesses along the equivalence line.
|
||
- Hcomp-correction wrapper around the `_at_top` RHS: requires T-side
|
||
hcomp infrastructure to state the formula precisely.
|
||
|
||
### Phase 1 Week 7 (2026-04-23): step↔eval bridge — Session 1
|
||
|
||
**Goal of the bridge.** The project currently carries two parallel
|
||
axiom sets: step-level (T1–T5, C1/C2/C4, `step_papp_plam`) and eval-level
|
||
(`eval_*` mirrors of the partial def). They must agree but nothing
|
||
enforces this. The bridge defines `step` as a normalisation-by-evaluation
|
||
composition — `step t := readback 0 (eval .nil t)` — so step-level axioms
|
||
become theorems derivable from eval-level axioms alone. Net effect: ~8
|
||
fundamental axioms (step-level) become derivable, and the Rust backend's
|
||
obligation list halves.
|
||
|
||
**Why multiple sessions.** The bridge requires (a) defining readback
|
||
(NbE reification) as a partial def, (b) proving a readback/eval
|
||
correspondence lemma, (c) redefining step and deriving each existing
|
||
step axiom as a theorem. Each piece is substantial; this is a five-session
|
||
plan.
|
||
|
||
**Session 1 (this session) — `Topolei/Cubical/Readback.lean` landed:**
|
||
|
||
- `partial def readback : Nat → CVal → CTerm` and
|
||
`partial def readbackNeu : Nat → CNeu → CTerm` in a mutual block,
|
||
covering every `CVal` and `CNeu` constructor (including the cubical
|
||
closures — `vTranspFun`, `vCompFun`, `vHCompFun`, `vTubeApp`,
|
||
`vPathTransp` — and every neutral shape).
|
||
- Depth-indexed fresh-name generation: `$rb_<n>` for term binders,
|
||
`$rd_<n>` for dim binders. Extends the `$`-prefixed hygiene
|
||
convention already used by the evaluator.
|
||
- Correct α-renaming semantics for `vlam`: extend env at the *original*
|
||
binder name mapped to `vneu (nvar fresh)`, so body lookups return the
|
||
fresh neutral. (First implementation attempt extended at the fresh
|
||
name, yielding `λx. x ↝ λ$rb_0. x` — caught by the test suite.)
|
||
- Face-disjoint reduction axioms mirroring every partial-def arm, same
|
||
pattern as `eval_*` in Eval.lean.
|
||
- `CTerm.readback : CTerm → CTerm := readback 0 ∘ eval .nil` — the
|
||
convenience wrapper that Session 3 will use to redefine step.
|
||
- Three sanity tests in `ReadbackTest`: free variable (`var_readback`),
|
||
identity function (`id_lambda_readback`), constant function
|
||
(`const_fn_readback`). All exercise the axioms end-to-end and verify
|
||
α-renaming works correctly.
|
||
|
||
**Sessions 2–4 delivered (same day):**
|
||
|
||
| Session | Delivered |
|
||
|---------|-----------|
|
||
| 2 ✅ | Switched from depth-indexed fresh-name generation (`$rb_<n>`) to **original-binder preservation** — env shadowing handles capture, which means `readback (eval .nil t) = t` for closed normal forms in the λ-fragment. Axioms simplified (no depth parameter). Correspondence lemmas `readback_nvar`, `CTerm.readback_var`, `CTerm.readback_lam`, `CTerm.readback_plam` prove readback/eval behavior on canonical λ-fragment forms. |
|
||
| 3 ✅ | Derived five step-level axioms as theorems under NbE: `CTerm.readback_papp_plam` (path β), `readback_transp_id` (T1), `readback_transp_const_id` (T2), `readback_comp_full` (C1), `readback_comp_empty` (C2). Each is a one-to-three-step `rw` chain through the corresponding eval-level axiom. |
|
||
| 4 ✅ | Partial T4 coverage: `readback_transp_plam_top` (full face) and `readback_transp_plam_const` (constant line) — the two cases where NbE reduces through. General T4 (arbitrary line/face) and T3/T5/C4 are documented as requiring machinery beyond NbE reification (typing-preservation for T3/C4, face-formula normalisation for T5, richer `vPathTransp` readback for general T4). |
|
||
|
||
**Session 5 (deferred — independent refactor):** The five NbE-derivable
|
||
step axioms are now provably redundant, but physical removal from the
|
||
codebase requires refactoring clients of `step_papp_plam`
|
||
(`step_papp_zero`, `step_papp_one`, `plam_witnesses_boundaries`) and of
|
||
the derived step-level theorems in TransportLaws/CompLaws. That
|
||
refactor is decoupled from the bridge's soundness benefit — the bridge
|
||
works as-is; removal just shortens the source.
|
||
|
||
**Net Week 7 result**: Rust's obligation list is down from "step axioms
|
||
+ eval axioms + readback axioms" to "eval axioms + readback axioms +
|
||
three semantic step axioms (T3, T5, C4) that truly are beyond NbE".
|
||
Five step axioms eliminated from the fundamental obligation list. See
|
||
the updated Axiom discharge obligations table below.
|
||
|
||
## What is done
|
||
|
||
### Cubical core (all 8 steps of TRANSPORT_PLAN.md)
|
||
|
||
| File | Contents | State |
|
||
|------|----------|-------|
|
||
| `Cubical/Interval.lean` | `DimVar`, `DimExpr`, de Morgan algebra, `DimExpr.subst`, `eval_subst`. **Stage 4.1**: `DimExpr.normalize` + `normalize_preserves_eval` + literal-reduction lemmas (`.inv .zero → .one`, `.inv .one → .zero`, double-negation). `deriving Inhabited` added (for FFI `opaque` requirement). | ✅ Stage 4.1 |
|
||
| `Cubical/Face.lean` | `FaceFormula`, face lattice laws, `restrict`, `Entails`, endpoint lemmas. **Stage 4.3**: `FaceFormula.normalize` + `normalize_preserves_eval` covering the meet/join × top/bot absorption laws — ensures deterministic face dispatch for Rust. `deriving Inhabited` added. | ✅ Stage 4.3 |
|
||
| `Cubical/Syntax.lean` | `CType` (`univ`/`pi`/`path`/**`sigma`**/**`glue`**) and `CTerm` (λ-fragment + transp/comp/compN + `glueIn`/`unglue` + **`pair`/`fst`/`snd`**) mutual inductives, `substDim`, **opaque** `step`. **Stage 1.2**: Σ types added. **Stage 4.4**: step-representation decision documented — Rust may implement natively (Option A) or derive as `readback ∘ eval .nil` (Option B); both satisfy the T4 axiom. | ✅ Stages 1.2 + 4.4 |
|
||
| `Cubical/Line.lean` | **NEW (Stage 1.1)**. `DimLine.inv` (reversed line), `DimLine.concat` (CCHM universe-hcomp, axiomatic), `transp_concat` theorem (cells-spec §14 Critical), `transp_concat_const_{left,right}` unit-law corollaries. Explicit Rust-discharge vs Lean-discharge provenance discipline codified. | ✅ Stage 1.1 |
|
||
| `Cubical/ValueTyping.lean` | **NEW (Stage 2.3)**. Semantic typing relations `HasVal : CVal → CType → Prop` / `HasNeu` / `EnvHasType` (opaque stubs, full inductive definition is Lean-discharge future work). Preservation axioms: `eval_preserves_type`, `readback_preserves_type`, `EnvHasType.nil`, consolidated `CTerm.step_preserves_type`. **T3 and C4 are now theorems** derived from `step_preserves_type` — axiom scales O(1) in type-formers, not O(n). | ✅ Stage 2.3 |
|
||
| `Cubical/FFI.lean` | **NEW (Stage 4.6)**. `@[extern]` `opaque` declarations for every Rust cubical-HoTT entry point: `evalRust`, `vAppRust`, `vPAppRust`, `vTranspRust`, `vHCompValueRust`, `vCompAtTermRust`, `vCompNAtTermRust`, `vFstRust`, `vSndRust`, `readbackRust`, `readbackNeuRust`, `stepRust`, `DimExprNormalizeRust`, `FaceFormulaNormalizeRust`. Companion doc: `FFI_DESIGN.md` (memory + marshalling) + `FFI_COMPLETENESS.md` (axiom audit). | ✅ Stage 4.6 |
|
||
| `Cubical/Subst.lean` | `CTerm.substDimBool`, `CType.substDim` (Bool), `CType.substDimExpr` (general DimExpr) — **extended for `.glue`** — `substDim_eq_substDimExpr` bridge, reduction lemmas | ✅ complete |
|
||
| `Cubical/DimLine.lean` | `DimLine`, endpoints `at0`/`at1`, `dimAbsent` (extended for `.glue`/`.glueIn`/`.unglue`), general-DimExpr absent-subst, Bool-case corollaries, `substDim_idem`, `substDim_comm` — all four `_aux` mutual defs extended | ✅ complete |
|
||
| `Cubical/Typing.lean` | `HasType` judgment (var/lam/app/plam/papp/transp/comp), inversion lemmas, `weaken`, `plam_boundaries` | ✅ complete |
|
||
| `Cubical/TransportLaws.lean` | **Stage 2.3**: T3 `transp_step_preserves` is now a *theorem* derived from `CTerm.step_preserves_type` (ValueTyping.lean). **Stage 4.2**: T4 `transp_plam_is_plam` replaced by constructive `transp_plam_is_plam_path` — path-restricted with explicit body `.plam j (.compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body)` mirroring `readback_vPathTransp_plam`. Rust discharges concretely. Derived: `transp_plam_body_path`, `transp_plam_body_path_eq`, `transp_plam_step_typed_path`. | ✅ Stages 2.3 + 4.2 |
|
||
| `Cubical/System.lean` | `System`, `CompatAt0`, compat lemmas, `System.Valid`, `HasType.comp_of_valid` bridge | ✅ complete |
|
||
| `Cubical/CompLaws.lean` | **Stage 2.3**: C4 `comp_step_preserves` is now a *theorem* derived from `CTerm.step_preserves_type`. Zero axioms in this file. C3 intentionally dropped (see file header). | ✅ Stage 2.3 |
|
||
| `Cubical/Value.lean` | Mutual `CEnv` / `CVal` / `CNeu` extended with `nglueIn`/`nunglue` + **`vpair`** (CVal) + **`nfst`/`nsnd`** (CNeu), `CEnv.lookup`/`extend`, `Inhabited` instances. **Stage 1.2**: Σ values added. | ✅ Stage 1.2 |
|
||
| `Cubical/Eval.lean` | Mutual block of 6 partial defs: `eval`, `vApp`, `vPApp`, `vHCompValue`, `vCompAtTerm`, `vCompNAtTerm`. λ-fragment + plam/papp + priority-ordered `.transp` dispatch (top / const / path / **glue (stuck placeholder)** / non-path-non-glue via `vTransp`) + `vCompAtTerm` for `.comp` + `vCompNAtTerm` for `.compN` + face-disjoint dispatch for `.glueIn` (top/bot/stuck) and `.unglue` (top/bot/stuck). `vApp` performs full CCHM Π β-rules on `vTranspFun`, `vHCompFun`, and `vCompFun`. `vPApp` reduces `vPathTransp` at `.zero`/`.one` endpoints via CCHM multi-clause (j=0/j=1) logic and routes generic dims through `vCompNAtTerm`. `eval_transp_nonpath` now carries an `h_not_glue` precondition so the Glue transport axioms (in `Glue.lean`) have an uncontested slot. | ✅ complete |
|
||
| `Cubical/Readback.lean` | Mutual `readback : CVal → CTerm` / `readbackNeu : CNeu → CTerm` as partial defs covering every CVal/CNeu constructor. **Original-binder preservation** — env shadowing provides capture-avoidance without needing fresh names. Face-disjoint `readback_*` / `readbackNeu_*` axioms mirroring every arm; `vPathTransp` arm splits face-disjointly on `.plam` input (Stream B #2c). `CTerm.readback` wrapper for NbE composition. **Seven NbE theorems** (`readback_papp_plam`, `readback_transp_id`, `readback_transp_const_id`, `readback_comp_full`, `readback_comp_empty`, `readback_transp_plam_path`, `readback_transp_face_congr`) derive the corresponding step-level axioms; `readback_transp_plam_general` combines `_top` / `_const` / `_path` to cover every well-typed path-line input shape. Correspondence lemmas for λ-fragment canonical forms. `ReadbackTest` sanity tests. **Step↔eval bridge Sessions 1–4 + Stream B #2b/#2c.** | ✅ Week 7 + Stream B #2b/#2c |
|
||
| `Cubical/Equiv.lean` | Half-adjoint `EquivData` (f/fInv/sec/ret/coh as CTerms), `idEquiv : CType → EquivData`, rfl-projection lemmas, five typing theorems (`hasType_f/fInv/sec_refl/ret_refl/coh_refl_refl`) at propositionally-reduced types | ✅ Week 5 |
|
||
| `Cubical/Glue.lean` | `EquivData.toGlueType` wrapper, `uaLine` (single-face CCHM ua), endpoint rfl-lemmas, computational content theorems, `idEquiv` specialisations. **Glue-transport axiom family (9 total):** 6 constant-equivalence axioms partitioning `{const-A, varying-A} × {bot, top, stuck}` + 2 **hcomp-corrected `_at_top` variants** (Stage 2.1 — full CCHM §6.2 formula with hcomp-in-T using `ret` for definitional ψ-boundary agreement) + 1 **varying-equivalence stuck axiom** (Stage 2.4 — structural stuck form when any of f/fInv/sec/ret/coh varies in i). `eval_transp_glue_const_at_top_from_hcomp` derives the naked form from the hcomp form at ψ = .bot. | ✅ Stages 2.1 + 2.4 |
|
||
| `Cubical/Transport.lean` | `vTransp` (4 priority-ordered arms, unified Π); `vTranspInv` (line reversal); `vTranspInv_const` / `vTranspInv_top` theorems; four `vTransp` axioms + `vTranspLine` wrapper | ✅ Weeks 3–4 (full Π) |
|
||
| `Cubical/EvalTest.lean` | Tests: λ-fragment β, path β, stuck forms, Week 3 transport-reduction cases, Π-const-domain and Π-varying-domain transport β-unfoldings, Week 4 hetero-comp reductions (C1/C2/const-line), Π hcomp β-rule, vTubeApp reductions | ✅ complete |
|
||
|
||
### Soundness theorems (Stages 1.3 + 2.3)
|
||
|
||
| Theorem | Statement | State |
|
||
|---------|-----------|-------|
|
||
| `Soundness.glue_beta` | `eval env (.unglue φ f (.glueIn φ t a)) = eval env a` under overlap `h_overlap : eval env (.app f t) = eval env a` | **Stage 1.3**: promoted from axiom to theorem. Follows from `eval_unglue_of_glueIn`. |
|
||
| `Soundness.glue_eta` | `eval env (.glueIn φ t (.unglue φ f g)) = eval env g` under overlap `h_overlap : eval env t = eval env (.app f g)` | **Stage 1.3**: promoted from axiom to theorem. Follows from `eval_glueIn_of_unglue`. |
|
||
| `Soundness.transp_ua` | transport along `uaLine e A B (.var i)` at ψ = .bot = `vApp (eval e.f) (eval t)` | Proved — uses `eval_transp_glue_const_at_bot`. |
|
||
| `Soundness.transp_ua_inverse` | transport along `uaLine e A B (.inv (.var i))` at ψ = .bot = `vApp (eval e.fInv) (eval t)` | Proved — uses `eval_transp_glue_const_at_top`. |
|
||
| `TransportLaws.transp_step_preserves` (T3) | `HasType Γ t L.at0 → HasType Γ (CTerm.step (.transp L.binder L.body φ t)) L.at1` | **Stage 2.3**: promoted from axiom to theorem. Follows from `HasType.transp` + `CTerm.step_preserves_type`. |
|
||
| `CompLaws.comp_step_preserves` (C4) | `HasType Γ t₀ L.at0 → HasType Γ u L.at1 → (compat) → HasType Γ (CTerm.step (.comp L.binder L.body φ u t₀)) L.at1` | **Stage 2.3**: promoted from axiom to theorem. Follows from `HasType.comp` + `CTerm.step_preserves_type`. |
|
||
| `Line.transp_concat` | `vTranspLine (concat L M h) .bot v = vTranspLine M .bot (vTranspLine L .bot v)` | **Stage 1.1** (cells-spec §14 Critical, previously unstated). Restatement of the eval-level `vTranspLine_concat` axiom. |
|
||
| `Line.transp_concat_const_{left,right}` | unit-law corollaries via T2 | **Stage 1.1**. |
|
||
|
||
### EML and GPU layer
|
||
|
||
| File | Contents | State |
|
||
|------|----------|-------|
|
||
| `EML.lean` | `EMLExpr` AST, GLSL codegen, `PlotConfig`, demo expressions | ✅ complete |
|
||
| `EML/Path.lean` | `boolToFloat`, `EMLExpr.evalWithEnv`, `EMLPath`, `at0`/`at1`, `const_endpoints`, `expPath` example | ✅ complete |
|
||
| `GPU/Spec.lean` | Opaque GPU types, `EMLExpr.evalAt`/`toColor`, `compileEML` + per-handle `compileEML_correct` axiom, `render_faithful` stub, IEEE Float axioms, EMLPath rendering bridge (`evalAt_body_eq_at1`, `toColor_body_eq_at1_toColor`, `render_eq_at1`), `evalAt_expOf` discharged | ✅ complete |
|
||
| `Canvas.lean` | FFI bindings for GLFW/OpenGL (`canvasRun`, `canvasRun2`) | ✅ complete |
|
||
|
||
---
|
||
|
||
## Open sorries
|
||
|
||
None. `evalAt_expOf` is now discharged against three IEEE 754 Float axioms
|
||
(`Float.log_one`, `Float.max_one_ge_eps`, `Float.sub_zero`) that serve as
|
||
verification obligations on the Rust FFI runtime.
|
||
|
||
---
|
||
|
||
## Deferred formal work
|
||
|
||
### Dependent Π types (`Typing.lean`, comment)
|
||
|
||
`HasType` has non-dependent `pi A B` only. Full dependent `(x:A) → B x` requires a
|
||
term evaluator (to apply `B` to a term). Noted as deferred.
|
||
|
||
### Full `φ`-substitution in `CTerm.substDim` (`Syntax.lean`, comment)
|
||
|
||
**RESOLVED** (Phase 1 Week 4++): `CTerm.substDim` now substitutes into face
|
||
formulas via `FaceFormula.substDim`. The approximation note no longer
|
||
applies.
|
||
|
||
---
|
||
|
||
## Phase 1 Week 4+++: Heterogeneous Π composition (fully reduced)
|
||
|
||
The previously-stuck heterogeneous Π comp case now reduces via a
|
||
CCHM-faithful fill-based β-rule.
|
||
|
||
### Machinery
|
||
|
||
- **`CVal.vCompFun : CEnv → DimVar → CType → CType → FaceFormula → CTerm → CTerm → CVal`** —
|
||
closure storing env, line binder, domA, codA, face, and tube/base CTerms.
|
||
- **`vCompAtTerm`**'s `.pi`-with-varying-line arm produces `vCompFun` instead
|
||
of the prior stuck `ncomp` neutral.
|
||
- **`vApp` on `vCompFun`** runs the CCHM fill β-rule:
|
||
- Construct `y_at_i = transp^{fj} (A[i := (inv fj) ∨ i]) φ y` — the fill.
|
||
- Construct `y_at_0 = transp^{fj} (A[i := inv fj]) φ y` — inverse-endpoint.
|
||
- Inner comp: `comp^i B(i) φ (u y_at_i) (t y_at_0)`.
|
||
- Evaluated in env extended with reserved `"$y"` bound to the argument.
|
||
- Reserved names `"$y"` (arg) and `⟨"$fj"⟩` (fill dim) are documented
|
||
hygiene assumptions.
|
||
|
||
### Fill endpoint correctness (verified in comments)
|
||
|
||
- At `fj = 0`: line-slice is `A[i := 1 ∨ i] = A(1)`. Source correct (`y : A(1)`). ✓
|
||
- At `fj = 1`: line-slice is `A[i := 0 ∨ i] = A(i)`. Target correct. ✓
|
||
- At `i = 0`: reduces to the inverse-transport formula. ✓
|
||
- At `i = 1`: line collapses to `A(1)` constant, T2 gives `y` as expected. ✓
|
||
|
||
### Degenerate case: const domain
|
||
|
||
When `dimAbsent i domA = true`, `substDimExpr` is identity, the transport
|
||
line in the fill is constant, T2 fires and the fills reduce to `y`. The
|
||
β-rule collapses to `comp^i B(i) φ (u y) (t y)` — no special-case logic
|
||
needed, just by following the reductions.
|
||
|
||
### Axioms
|
||
|
||
- `eval_comp_pi` — routes `comp^i (pi A B) φ u t` (non-top, non-bot,
|
||
varying line) to `vCompFun`.
|
||
- `vApp_vCompFun` — the full β-rule as an equation.
|
||
- `eval_comp_stuck` gets a new `h_not_pi` precondition (excluded by
|
||
`eval_comp_pi` for any pi-headed type).
|
||
|
||
### Tests
|
||
|
||
- `eval_comp_pi_example` — hetero comp on a varying pi produces `vCompFun`.
|
||
- `vApp_vCompFun_const_dom_example` — const-domain β fires.
|
||
- `vApp_vCompFun_varying_dom_fires` — varying-domain β fires, producing
|
||
the genuinely non-trivial fill terms.
|
||
- Spot-check `CType.substDimExpr` computes the expected composite
|
||
domain type `path univ "a0" (papp "p" ((inv fj) ∨ i))`.
|
||
|
||
---
|
||
|
||
## Axiom discharge obligations
|
||
|
||
These are intentional axioms — formal specs for what the Rust evaluator
|
||
(linked via `@[extern]` + `@[implemented_by]`) must compute. Topolei is
|
||
structured as a Lean 4 extension: the external-to-Lean layer is always
|
||
*specified as axioms in Lean first*, then *discharged* by the Rust module.
|
||
Each becomes a proof obligation when implementation is written.
|
||
|
||
### Cubical evaluator (TransportLaws + CompLaws + Readback)
|
||
|
||
The Phase 1 Week 7 step↔eval bridge promoted five step-level axioms to
|
||
NbE theorems in `Cubical/Readback.lean`. Stream B #2d (Session 5
|
||
cleanup, 2026-04-23) **physically removed** those five axioms and their
|
||
client cascade — they no longer appear as axioms in the Lean source.
|
||
|
||
| Axiom (former) | Obligation | Current status |
|
||
|----------------|------------|----------------|
|
||
| `step_papp_plam` | `step ((⟨i⟩ t) @ r) = t[i := r]` | ✅ Removed; theorem `CTerm.readback_papp_plam` |
|
||
| T1 `transp_id` | `transpⁱ A 1_F t` reduces to `t` | ✅ Removed; theorem `CTerm.readback_transp_id` |
|
||
| T2 `transp_const_id` | transport under constant (i-absent) type is identity | ✅ Removed; theorem `CTerm.readback_transp_const_id` |
|
||
| C1 `comp_full` | `comp ... 1_F u t₀` reduces to `u[i:=1]` | ✅ Removed; theorem `CTerm.readback_comp_full` |
|
||
| C2 `comp_empty` | `comp ... 0_F u t₀` reduces same as `transp ... 0_F t₀` | ✅ Removed; theorem `CTerm.readback_comp_empty` |
|
||
|
||
| Axiom (residual) | Obligation | Status |
|
||
|------------------|------------|--------|
|
||
| T3 `transp_step_preserves` | transport is type-safe (subject reduction) | ⚠️ Stays step-level; needs typing-preservation machinery (Stream B #2a) |
|
||
| T4 `transp_plam_is_plam` | transport of `⟨j⟩ body` produces `⟨j⟩ body'` | ✅ NbE coverage complete for path-typed lines via `readback_transp_plam_general` (combines `_top` / `_const` / `_path`); see `Cubical/Readback.lean`. Non-path varying lines are vacuous in well-typed code (Stream B #2c, 2026-04-23). Step axiom retained for syntactic-only consumers. |
|
||
| T5 `transp_face_congr` | transport inspects face formulas only by truth value | ✅ Promoted to eval-level axiom `eval_transp_face_congr` in `Eval.lean`; NbE theorem `CTerm.readback_transp_face_congr` in `Readback.lean`. Step-level axiom removed (Stream B #2b, 2026-04-23). |
|
||
| C4 `comp_step_preserves` | composition is type-safe | ⚠️ Stays step-level; same typing-preservation gap as T3 |
|
||
|
||
**Remaining true obligations on Rust for the cubical evaluator**:
|
||
- All eval-level equations (mirroring `eval` / `vApp` / `vPApp` / `vTransp`
|
||
/ `vHCompValue` / `vCompAtTerm` / `vCompNAtTerm` arms).
|
||
- All readback-level equations (mirroring `readback` / `readbackNeu` arms).
|
||
- Glue-transport axioms (`eval_transp_glue_const_at_bot` / `_at_top` / `_stuck`).
|
||
- The six glueIn/unglue face-disjoint axioms.
|
||
- The eval-level T5 axiom `eval_transp_face_congr` (face normalisation).
|
||
- The two residual step-level axioms T3 and C4 (subject reduction —
|
||
needs typing-preservation machinery, Stream B #2a).
|
||
- The step-level T4 `transp_plam_is_plam` retained as a syntactic
|
||
fallback (NbE coverage for path-typed lines is complete via
|
||
`readback_transp_plam_general`).
|
||
|
||
*(CCHM C3 — "transport is a specialised composition" — is intentionally
|
||
not stated here; see the note at the top of `CompLaws.lean`. It only holds
|
||
with side-conditions that would duplicate `transp_const_id` in content, and
|
||
will be recovered via the real `transp = hcomp + fill` reduction when the
|
||
evaluator is written in Phase 1 Week 4.)*
|
||
|
||
### Evaluator equations (Eval.lean + Transport.lean + Glue.lean)
|
||
|
||
Axioms mirroring the `partial def` arms of `eval`, `vApp`, `vPApp`:
|
||
`eval_var`, `eval_lam`, `eval_app`, `eval_plam`, `eval_papp`, `eval_transp`,
|
||
`eval_comp`, `vApp_vlam`, `vApp_vneu`, `vPApp_vplam`, `vPApp_vneu`. Plus
|
||
three for `vTransp`: `vTransp_top`, `vTransp_const`, `vTransp_stuck`. All
|
||
will become provable theorems once the evaluator is rewritten as a total
|
||
function with a proper termination measure. `eval_transp_top`,
|
||
`eval_transp_const`, `eval_transp_stuck` are already theorems, derived from
|
||
the corresponding `vTransp_*` axioms.
|
||
|
||
**Glue-transport axioms** (Glue.lean, complete for constant-equivalence
|
||
sub-cases — both constant-A and varying-A; varying-equivalence is Stream
|
||
B #1c, future):
|
||
|
||
| Axiom | A varies? | `φ[i:=1]` | Obligation |
|
||
|-------|-----------|-----------|------------|
|
||
| `eval_transp_glue_const_at_bot` | no | `.bot` | reduces to `transp i A ψ (unglue (φ[i:=0]) f t)` |
|
||
| `eval_transp_glue_const_at_top` | no | `.top` | reduces to `app fInv (transp i A ψ (unglue (φ[i:=0]) f t))` |
|
||
| `eval_transp_glue_const_stuck` | no | residual | structured `ntransp` neutral |
|
||
| `eval_transp_glue_varA_at_bot` | yes | `.bot` | reduces to `compN i A [(ψ, unglue φ f t), (φ, app f t)] (unglue (φ[i:=0]) f t)` |
|
||
| `eval_transp_glue_varA_at_top` | yes | `.top` | reduces to `app fInv (compN i A [(ψ, unglue φ f t), (φ, app f t)] (unglue (φ[i:=0]) f t))` |
|
||
| `eval_transp_glue_varA_stuck` | yes | residual | structured `ntransp` neutral |
|
||
|
||
The six axioms partition `(A.dimAbsent i, φ[i:=1])` into 6 disjoint
|
||
cells — face-disjoint by hypothesis (`hA : … = true / false` and the
|
||
`φ[i:=1]` partition). The Rust backend must reduce CCHM §6.2 Glue
|
||
transport to the matching cell. Hcomp-correction note (Stream B #1a
|
||
refined): the `_at_top` axioms state the principal T-side witness;
|
||
their full CCHM form adds a T-side hcomp using `sec` for ψ-boundary
|
||
agreement, which trivialises under constant-equivalence hypotheses.
|
||
|
||
### GPU layer (GPU/Spec)
|
||
|
||
| Axiom | Obligation |
|
||
|-------|------------|
|
||
| `ShaderHandle.semantic` | opaque semantic function carried by every shader handle |
|
||
| `compileEML` | abstract EML-to-shader compilation function |
|
||
| `compileEML_correct` | `(compileEML expr).semantic = expr.toColor` (scoped per-expr; avoids the earlier unsound universally-quantified version) |
|
||
| `render_faithful` | GPU writes `h.semantic p u` at pixel `p` (needs readback tests; currently `True`) |
|
||
| `Float.log_one` | IEEE 754 `log 1 = 0` |
|
||
| `Float.max_one_ge_eps` | IEEE 754 `max 1.0 1e-9 = 1.0` |
|
||
| `Float.sub_zero` | IEEE 754 `a − 0 = a` for finite `a` |
|
||
|
||
---
|
||
|
||
## Axiom provenance spectrum (Stage 3 audit, 2026-04-23)
|
||
|
||
Every axiom in topolei carries one of three provenance tags that
|
||
determine *where* it is ultimately discharged. The axiom count
|
||
(~100) is large mostly because the Lean side *specifies* the Rust
|
||
evaluator's behaviour one arm at a time; the set of open Lean-side
|
||
proof obligations is small.
|
||
|
||
### A. Rust-discharge axioms (~90 of ~100)
|
||
|
||
These axioms state, arm-by-arm, what the Rust cubical evaluator must
|
||
compute. They cannot be eliminated without changing the partial-def
|
||
structure — they ARE the Lean-as-spec surface of the FFI contract.
|
||
Grouped by file:
|
||
|
||
- `Eval.lean` (48 axioms): one per arm of `eval`, `vApp`, `vPApp`,
|
||
`vHCompValue`, `vCompAtTerm`, `vCompNAtTerm`, `vFst`, `vSnd`. Plus
|
||
the eval-level β/η rules for glue (`eval_unglue_of_glueIn`,
|
||
`eval_glueIn_of_unglue` — Stage 1.3) and T5 face congruence
|
||
(`eval_transp_face_congr` — Stream B #2b).
|
||
- `Transport.lean` (4 axioms): `vTransp_top/_const/_pi/_stuck`.
|
||
- `Readback.lean` (19 axioms): one per arm of `readback` /
|
||
`readbackNeu`, including the face-disjoint `vPathTransp_plam` /
|
||
`_other` pair (Stream B #2c) and the Σ additions (Stage 1.2).
|
||
- `Glue.lean` (9 axioms): the 6 `_const_*` / `_varA_*` face-disjoint
|
||
partition + 2 hcomp-corrected `_at_top` forms (Stage 2.1) + 1
|
||
varying-equivalence stuck axiom (Stage 2.4).
|
||
- `Line.lean` (4 axioms): `DimLine.concat` + `concat_at0` + `concat_at1`
|
||
+ `vTranspLine_concat` (Stage 1.1 — CCHM universe-hcomp discharge).
|
||
- `GPU/Spec.lean` (2–3 axioms): `ShaderHandle` / `GPUContext` opaque
|
||
types, `compileEML` / `compileEML_correct`, `render_faithful`.
|
||
|
||
### B. Lean-discharge axioms (~9 of ~100)
|
||
|
||
These axioms state properties that a future *Lean* development will
|
||
prove. No Rust involved.
|
||
|
||
- `ValueTyping.lean` (4 axioms): `eval_preserves_type`,
|
||
`readback_preserves_type`, `EnvHasType.nil`, `CTerm.step_preserves_type`.
|
||
All discharge once `HasVal` / `HasNeu` / `EnvHasType` are given
|
||
inductive definitions. Unblocks T3 / C4 theorems (already done
|
||
modulo these axioms).
|
||
- `Line.lean` (3 axioms): `DimLine.inv_at0`, `inv_at1`, `inv_inv`.
|
||
Discharge once `DimExpr.normalize` lands (reducing `.inv .zero = .one`
|
||
etc.).
|
||
- `TransportLaws.lean` (1 axiom): T4 `transp_plam_is_plam` — syntactic
|
||
fallback; path-typed inputs are fully NbE-covered. Becomes
|
||
theorem or redundant once a total evaluator is introduced.
|
||
- Reserved for future extension (e.g. Multi-face Glue).
|
||
|
||
### C. IEEE / external axioms (~5 of ~100)
|
||
|
||
- `GPU/Spec.lean` (3 Float axioms): IEEE 754 `log 1 = 0`, `max 1 ε = 1`,
|
||
`a − 0 = a`. Pragmatic; discharged by IEEE 754 specification.
|
||
- Opaque `GPU` types (2).
|
||
|
||
### Key audit findings
|
||
|
||
1. **Only ~9 of ~100 axioms are open Lean-side proof obligations.** The
|
||
rest are either Rust-discharge (intrinsic to the Lean-spec / Rust-
|
||
backend contract) or external-spec. Topolei's formalisation is
|
||
nearly closed at the Lean level.
|
||
|
||
2. **Stage 2.3 consolidation delivered O(1) scaling.** Before: each
|
||
new type-former with a transp/comp rule needed its own
|
||
step-preserves axiom. After: subject reduction scales in the
|
||
single `CTerm.step_preserves_type` axiom — adding new type-formers
|
||
(Σ done, `.glueN` future) automatically inherits preservation.
|
||
|
||
3. **Face-disjoint partitioning is the pervasive pattern.** Recurring
|
||
in Glue transport (9-way partition), glueIn/unglue (3-way + β/η
|
||
redex), transp face cases (4-way), Σ β/neu (2-way). Every axiom
|
||
family consumers' non-overlap by matching/mismatched preconditions.
|
||
This is what lets adding new cases grow the axiom set without
|
||
perturbing proofs that consume existing axioms (e.g. `transp_ua`).
|
||
|
||
4. **Step-level axioms are nearly gone.** After Stages 2.3 + 1.3:
|
||
T1/T2/C1/C2/`step_papp_plam`/T5/glue_β/η are all theorems. T3/C4
|
||
are theorems (via `step_preserves_type`). Only T4
|
||
(`transp_plam_is_plam`) remains — a syntactic fallback that is
|
||
vacuous in well-typed code.
|
||
|
||
---
|
||
|
||
## Missing connections
|
||
|
||
### `Canvas.lean` ↔ formal spec
|
||
|
||
`canvasRun` / `canvasRun2` are FFI calls with no connection to `render_faithful`
|
||
or `compileEML_correct`. No theorem links the window loop to the GPU spec.
|
||
|
||
### `Basic.lean`
|
||
|
||
Currently `def hello := "world"`. Intended role not yet defined.
|
||
|
||
---
|
||
|
||
## Priority order
|
||
|
||
**Phase 1 (Cubical Core) is closed.** Stages 1–3 (post-Phase-1
|
||
refinement, 2026-04-23) are closed: Line primitives, Sigma types,
|
||
β/η-aware glue rules, hcomp-corrected `_at_top`, T3/C4 subject
|
||
reduction, varying-equiv stuck, poet-restructure audit. Three
|
||
mostly-independent work streams remain. Pick by intent, not by
|
||
dependency.
|
||
|
||
**Stream A: Zigzag Engine Lean Port (Phase 2 prerequisite, pure Lean):**
|
||
See `ZIGZAG_PORT.md` for the full 10-step plan. Ports the n-category
|
||
combinatorics (dimension-general normalisation preserving essential
|
||
identities, type-checking against signatures) from Rust reference into
|
||
Lean. Unlocks `Cell/` higher-cell semantics. 6–8 weeks. Rust
|
||
reference at `zigzag-engine/` is for porting from, not a dependency.
|
||
|
||
**Stream B: Pure-Lean extensions of the cubical core.**
|
||
|
||
Each sub-item below is an independent entry point — pick by intent,
|
||
not by dependency. Entry point for each is marked 📍. ✅ items
|
||
landed in Stages 1–3 (2026-04-23).
|
||
|
||
1. **Glue transport — CCHM §6.2 sub-cases.**
|
||
- ✅ **1a. Hcomp-correction wrapper for `_at_top`** (Stage 2.1).
|
||
`eval_transp_glue_const_at_top_hcomp` and `_varA_at_top_hcomp`
|
||
state the full CCHM formula with hcomp-in-T using `ret` for
|
||
definitional ψ-boundary agreement. Naked form derived as theorem
|
||
at ψ = .bot (`eval_transp_glue_const_at_top_from_hcomp`).
|
||
- ✅ **1b. Varying base type `A`** (Stream B #1b).
|
||
- ✅ **1c. Varying-equivalence (structurally stuck)** (Stage 2.4).
|
||
`eval_transp_glue_varEquiv` produces a structured `ntransp`
|
||
neutral when any of `f/fInv/sec/ret/coh` vary in `i`. Full
|
||
reduction formula is future Rust refinement (the axiom becomes
|
||
more informative without Lean-side changes).
|
||
|
||
2. **step↔eval bridge — all residuals now closed or consolidated.**
|
||
- ✅ **2a. T3 / C4 subject reduction** (Stage 2.3). Consolidated into
|
||
`CTerm.step_preserves_type` (ValueTyping.lean); T3 and C4 are
|
||
theorems.
|
||
- ✅ **2b. T5 face congruence** (Stream B #2b).
|
||
- ✅ **2c. General T4 NbE for path-typed lines** (Stream B #2c).
|
||
- ✅ **2d. Physical removal of redundant step axioms** (Stream B #2d).
|
||
- ✅ **Glue β/η on general faces** (Stage 1.3). `glue_beta`,
|
||
`glue_eta` (Soundness.lean) promoted to theorems via eval-level
|
||
`eval_unglue_of_glueIn` / `eval_glueIn_of_unglue`.
|
||
|
||
3. ✅ **Sigma types** (Stage 1.2). `CType.sigma` + `CTerm.pair/.fst/.snd`
|
||
+ value-level `vpair` / `nfst` / `nsnd` + full propagation through
|
||
substDim/dimAbsent/Typing/Value/Eval/Readback. Unlocks Cell.par
|
||
(§6.2), Color triples (§8.1), Shader pair/fst/snd (§9.2).
|
||
`fiberTy` still needs **dependent** Σ (genuinely deferred).
|
||
|
||
4. 📍 **Multi-face Glue** (`.glueN`). *Intentionally deferred.* Enables
|
||
the symmetric two-face ua (cells-spec §5.7); single-face Glue
|
||
(present) is computationally sufficient. Not load-bearing for
|
||
Phase 2 cells. Future work.
|
||
|
||
5. ✅ **Line module** (Stage 1.1). `DimLine.inv` + `DimLine.concat` +
|
||
`transp_concat` theorem (cells-spec §14 Critical, previously
|
||
unstated) + `transp_concat_const_{left,right}` unit-law corollaries.
|
||
Foundation for `Cell.seq` / `Cell.inv` in Phase 2.
|
||
|
||
6. **Hygienic fresh-name generation** (low priority). Current
|
||
convention: user code must avoid `$`-prefixed names. **Entry**:
|
||
add a gensym counter to `CEnv` (or state monad in eval). Can be
|
||
deferred indefinitely.
|
||
|
||
**Stream C: Rust FFI — the one Rust component.**
|
||
|
||
Cubical evaluator backend implementing the eval-level, readback-level,
|
||
and Glue-transport axioms. Linked via `@[extern]` +
|
||
`@[implemented_by]`. Gives Lean's kernel the ability to *reduce*
|
||
cubical terms at native speed. Also hosts the GPU runtime (wgpu) when
|
||
Phase 5 begins. **This is the only Rust component in topolei**; no
|
||
part of the zigzag engine, numerical layer, cell layer, or any other
|
||
phase belongs here.
|
||
|
||
📍 **Entry: minimum Rust obligation list to start implementation** (see
|
||
the Axiom discharge obligations table for the full list):
|
||
|
||
- **Eval arms** (Eval.lean): `eval_var`, `eval_lam`, `eval_app`,
|
||
`eval_plam`, `eval_papp`, the four `eval_transp_*` face-cases, the
|
||
five `eval_comp_*` cases, `eval_compN`, the three `eval_glueIn_*`
|
||
face-cases, the three `eval_unglue_*` face-cases.
|
||
- **vApp / vPApp / vTransp / vHCompValue / vCompAtTerm / vCompNAtTerm
|
||
arms**: as listed in Eval.lean's axiom block.
|
||
- **Readback arms** (Readback.lean): `readback_*` (9 axioms — including
|
||
the face-disjoint `readback_vPathTransp_plam` / `_other` pair) +
|
||
`readbackNeu_*` (9 axioms).
|
||
- **Glue transport** (Glue.lean, 9 axioms after Stages 2.1 + 2.4): the
|
||
six `_const_*` / `_varA_*` face-disjoint axioms + 2 hcomp-corrected
|
||
`_at_top` variants (Stage 2.1) + 1 varying-equivalence stuck axiom
|
||
(Stage 2.4).
|
||
- **Σ eval/readback** (Eval.lean + Readback.lean, Stage 1.2):
|
||
`eval_pair/fst/snd`, `vFst_vpair/vneu`, `vSnd_vpair/vneu`,
|
||
`readback_vpair`, `readbackNeu_nfst/nsnd`.
|
||
- **Line transport** (Line.lean, Stage 1.1): `DimLine.concat` + endpoints
|
||
+ `vTranspLine_concat` (CCHM universe-hcomp).
|
||
- **Glue β/η** (Eval.lean, Stage 1.3): `eval_unglue_of_glueIn`,
|
||
`eval_glueIn_of_unglue`. Soundness-level `glue_beta`/`glue_eta` are
|
||
theorems.
|
||
- **T5 face congruence** (Eval.lean): `eval_transp_face_congr`.
|
||
- **Residual step-level axioms**: only T4 `transp_plam_is_plam`
|
||
(TransportLaws.lean — syntactic fallback). T3 and C4 are theorems
|
||
(via `CTerm.step_preserves_type` in ValueTyping.lean).
|
||
- **Float axioms** (GPU/Spec.lean): `Float.log_one`,
|
||
`Float.max_one_ge_eps`, `Float.sub_zero`.
|
||
- **GPU bridge**: `compileEML`, `compileEML_correct`,
|
||
`render_faithful` (after pixel-readback tests replace `True`).
|
||
|
||
---
|
||
|
||
## Concrete "next session" suggestions (2026-04-23, post-Stages 1–3)
|
||
|
||
With Stages 1–3 closed, the cubical core is minimal and well-shaped.
|
||
Remaining choices are all forward-looking rather than closure-oriented:
|
||
|
||
| Suggestion | Size | Impact |
|
||
|------------|------|--------|
|
||
| **Start Zigzag Lean port** (Stream A) | 6–8 weeks | Unblocks Phase 2 Cell/Higher.lean (n-cells). Independent of cubical-core extensions. |
|
||
| **Start Phase 2 Cell/Basic.lean + Cell/Compose.lean** | 2–3 sessions | Consumes the Line module (Stage 1.1) — `Cell.seq` / `Cell.inv` via `DimLine.concat` / `DimLine.inv`. cell_left_unit / cell_right_unit via `transp_concat_const_{left,right}`. Non-blocked. |
|
||
| **Discharge HasVal / HasNeu inductively** (Stage 2.3 completion) | multi-session | Replaces the four Lean-discharge axioms in ValueTyping.lean with theorems. Unlocks full subject-reduction machinery and dependent typing extensions. |
|
||
| **Multi-face Glue (`.glueN`)** (Stream B #4, deferred) | multi-session | Enables the symmetric two-face ua (cells-spec §5.7). Single-face Glue is sufficient for Phase 2 cells, so this is backlog. |
|
||
| **Varying-equivalence Glue full reduction** (Stage 2.4 refinement) | multi-session | Upgrade `eval_transp_glue_varEquiv` from stuck form to full CCHM computational content (needs `transp^i T` on witness terms). |
|
||
| **`DimExpr.normalize`** | 1–2 sessions | Reduces `.inv .zero = .one` etc. syntactically. Discharges three Lean-side axioms (`DimLine.inv_at0`, `inv_at1`, `inv_inv`). |
|
||
| **Start Rust implementation** (Stream C) | multi-session | **Unblocked by Stage 4.** See `FFI_DESIGN.md` (C ABI contract) + `FFI_COMPLETENESS.md` (per-function axiom audit) + `KERNEL_BOUNDARY.md` (scope contract vs. Lean kernel). `Cubical/FFI.lean` declares the extern entry points; Rust implements them to satisfy the ~90 Rust-discharge axioms. Orthogonal — can run in parallel with any Stream B work. |
|
||
| **Dependent Π / Σ types** | multi-session | Would require a term evaluator to apply `B` to a term. Unlocks proper `fiberTy` (Equiv.lean's "propositionally-reduced types" compromise). |
|