From 8561e194670f9913d1fcf99f4e946c66981e2952 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Mon, 27 Apr 2026 22:52:14 -0600 Subject: [PATCH] Docs cleanup: archive PHASE1, accept ZIGZAG_PORT, fix stale paths MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - TRANSPORT_PLAN.md → PHASE1_HISTORY.md with archival header. Path references updated from `Topolei/Cubical/*` to `CubicalTransport/*` to match the post-split namespace. Methodology preserved as a template for future formalisation phases. - ZIGZAG_PORT.md moved here from topolei. This is engine code: the port lands in `CubicalTransport/Zigzag/`, and an AI shortcut on normalisation, degeneracy, or signature-typechecking would cascade-corrupt every higher-cell proof in topolei. Added a cascade caveat header explaining how engine-level zigzag changes ripple back into the topolei interface repo. Body updated for split context. - KERNEL_BOUNDARY.md: clarified that the planned `Eq ↔ Path` bridge module is distinct from the existing trace bridge (`Topolei/Cubical/Trace.lean` in topolei). - README.md: refreshed Reference section with renames + new docs. - native/cubical/README.md: path refs updated. Co-Authored-By: Claude Opus 4.7 (1M context) --- KERNEL_BOUNDARY.md | 6 +- TRANSPORT_PLAN.md => PHASE1_HISTORY.md | 35 ++- README.md | 18 +- ZIGZAG_PORT.md | 370 +++++++++++++++++++++++++ native/cubical/README.md | 4 +- 5 files changed, 414 insertions(+), 19 deletions(-) rename TRANSPORT_PLAN.md => PHASE1_HISTORY.md (89%) create mode 100644 ZIGZAG_PORT.md diff --git a/KERNEL_BOUNDARY.md b/KERNEL_BOUNDARY.md index 2e17c92..0763ee5 100644 --- a/KERNEL_BOUNDARY.md +++ b/KERNEL_BOUNDARY.md @@ -113,8 +113,10 @@ nothing but Lean's existing primitives plus FFI. These bridges let users transport discrete-math lemmas (Nat, Bool, decidable structures, Mathlib-style hypotheses) into cubical proofs -and vice versa. Bridge module `Topolei/Cubical/Bridge.lean` is -planned (not yet written). +and vice versa. An `Eq ↔ Path` bridge module is planned (not yet +written). A different cubical bridge — `Topolei/Cubical/Trace.lean` +in the sibling `topolei` repo — already exists, but it lifts CTerms +into the polymorphic `Trace` for provenance, not for `Eq` interop. ### 2.7 Higher cells via Zigzag Lean port diff --git a/TRANSPORT_PLAN.md b/PHASE1_HISTORY.md similarity index 89% rename from TRANSPORT_PLAN.md rename to PHASE1_HISTORY.md index 03258f6..e0ffb74 100644 --- a/TRANSPORT_PLAN.md +++ b/PHASE1_HISTORY.md @@ -1,9 +1,22 @@ -# Transport & Composition — Implementation Plan +# Phase 1 History — Transport & Composition Formalization Plan -Stage goal: formally verify the CCHM transport and composition operations -in the deep embedding before writing any Rust — per Topolei's process -discipline of stating all external-to-Lean behavior as Lean axioms before -the Rust FFI side is built. +> **Archival.** This document is the original implementation plan +> that drove Phase 1 of the cubical-transport HoTT formalization +> (CCHM §5–6). Every stage listed below is *closed*: see the +> `CubicalTransport/*` modules for the delivered code and +> `CubicalTest.lean` (62/62 passing) for the verification. +> +> Paths in the original plan referred to `Topolei/Cubical/*` from the +> pre-split monolithic repo. They have been mechanically updated to +> the post-split `CubicalTransport/*` location, but otherwise the +> document is preserved as-is — methodology and step decomposition +> remain useful as a template for future formalization phases (e.g. +> the zigzag port: see `ZIGZAG_PORT.md`). + +Stage goal (original): formally verify the CCHM transport and +composition operations in the deep embedding before writing any Rust +— per the project's discipline of stating all external-to-Lean +behavior as Lean axioms before the Rust FFI side is built. Each step has one clear deliverable, depends only on prior steps, and can be built and checked independently with `lake build`. @@ -61,7 +74,7 @@ We may define one in terms of the other to avoid duplication. ## Step 2 — DimLine: lines of types -**File:** `Topolei/Cubical/DimLine.lean` +**File:** `CubicalTransport/DimLine.lean` **What:** A *line of types* `λi. A` — the domain of transport. Syntactically, it is a pair of a bound dimension variable and a body type. @@ -137,7 +150,7 @@ existing Syntax/Typing theorems still hold. ## Step 4 — Transport identity law -**File:** `Topolei/Cubical/TransportLaws.lean` +**File:** `CubicalTransport/TransportLaws.lean` **What:** The fundamental CCHM axiom: transport under the trivial cofibration `1_F` is the identity. @@ -171,7 +184,7 @@ stated as axiom with comment explaining which direction is derivable. ## Step 5 — Transport–path connection -**File:** `Topolei/Cubical/TransportLaws.lean` (continued) +**File:** `CubicalTransport/TransportLaws.lean` (continued) **What:** Transport along a constant line recovers path application. A path `p : Path A a b` is a term that, when transported with `transp`, @@ -205,7 +218,7 @@ proof or clear sorry marking the missing evaluator. ## Step 6 — System: partial elements -**File:** `Topolei/Cubical/System.lean` +**File:** `CubicalTransport/System.lean` **What:** A *system* `[φ↦u]` is a partial term — defined only on the face where `φ` holds. This is the new concept that composition @@ -246,7 +259,7 @@ def System.CompatAt0 (s : System) (i : DimVar) (t₀ : CTerm) : Prop := ## Step 7 — Composition declaration + typing rule -**File:** `Topolei/Cubical/Typing.lean` (extended) +**File:** `CubicalTransport/Typing.lean` (extended) **What:** Add `HasType.comp` — the typing rule for the composition operation. This is the main event: composition is what makes the @@ -279,7 +292,7 @@ theorem HasType.comp_inv (h : HasType Γ (.comp L φ u t₀) A) : ## Step 8 — Composition laws -**File:** `Topolei/Cubical/CompLaws.lean` +**File:** `CubicalTransport/CompLaws.lean` **What:** The three fundamental laws of composition. All three are CCHM axioms — not derivable from the syntax. diff --git a/README.md b/README.md index 9fafc68..a3d34cb 100644 --- a/README.md +++ b/README.md @@ -45,14 +45,24 @@ lake build ## Reference -- `FFI_DESIGN.md` — C ABI contract. +- `FFI_DESIGN.md` — C ABI contract between Lean and the Rust kernel. - `FFI_COMPLETENESS.md` — per-function axiom audit. - `KERNEL_BOUNDARY.md` — what this delivers in unmodified Lean 4 vs. what would need upstream Lean kernel work. - `NUMERICAL.md` — numerical implementation principles. -- `TRANSPORT_PLAN.md` — formalization plan (history of Phase 1). +- `PHASE1_HISTORY.md` — original transport/composition formalisation + plan (archived; Phase 1 closed; preserved as methodology template + for future phases). +- `ZIGZAG_PORT.md` — step-by-step Lean port plan for the n-category + combinatorial engine (Phase 2+ higher-cell backend). Lands here + in the engine. **Read the cascade caveat at the top before + editing**: changes in the ported zigzag layer cascade to the + sibling `topolei` repo. +- `native/cubical/README.md` — Rust crate build + dev guide. +- `native/cubical/WASM.md` — wasm32 ABI integration contract. ## Used by -- [`max/topolei`](../topolei) — interactive cells-spec workspace - front-end built on this engine. +- [`max/topolei`](../topolei) — the cells-spec workspace interface, + built on this engine. See its `cells-spec.md` and `STATUS.md` for + the application-side picture. diff --git a/ZIGZAG_PORT.md b/ZIGZAG_PORT.md new file mode 100644 index 0000000..3194dc0 --- /dev/null +++ b/ZIGZAG_PORT.md @@ -0,0 +1,370 @@ +# Zigzag Engine — Lean Port Plan + +*Parallel to `PHASE1_HISTORY.md` (which guided Phase 1's cubical +formalisation). This document plans the step-by-step port of the +zigzag engine from its Rust reference implementation into Lean 4, +as the combinatorial n-category backend for the cell layer.* + +> **Cascade caveat — read before editing.** +> +> The ported zigzag layer lands in *this* repo (the engine) because +> it is engine code: an AI shortcut on normalisation, degeneracy +> theory, or signature-typechecking would silently corrupt every +> downstream higher-cell proof in `topolei` that consumes the +> n-category backend. +> +> Any change to the ported zigzag layer can therefore cascade to the +> sibling `topolei` repo: cell-graph constructors, multihead-cursor +> selection, peripheral observations on n-cells, and the rendering +> pipeline that visualises higher cells will all see the change. +> Land changes carefully — engine-level breakage is not locally +> repairable from `topolei` without coordinated edits across both +> repos. Verify the engine's own `cubical-test` battery first; then +> rebuild `topolei` end-to-end against the updated engine before +> committing the cascade. + +--- + +## Decision (2026-04-22) + +**The zigzag engine will be reimplemented in Lean 4.** The existing +Rust implementation at `zigzag-engine/zigzag-engine/` is **reference +material only** — a structural template for the port, not a +dependency. This matches the project's Lean-as-host discipline and +maximises the medium-term goal of Lean-native reasoning (see below). + +**The only Rust component in this engine is the cubical evaluator FFI +backend** (`native/cubical/`) — the module that discharges the Phase 1 +axioms (`step`, `eval`, `vApp`, `vPApp`, `vTransp`, etc.) via +`@[extern]` + `@[implemented_by]`. That one Rust crate exists to +extend Lean 4 with computational cubical-transport HoTT. After the +port lands, the zigzag layer will live alongside it as Lean-only +code under `CubicalTransport/Zigzag/` — no additional Rust dependency. + +(The sibling `topolei` interface repo carries its own Rust crates — +`canvas-rs` for GPU rendering and a render scaffold — but those are +application-side, not engine-side, and unrelated to the n-category port.) + +## Why Lean, not the Rust backend (Option A over Option B) + +Axiomatic Rust backends give `axiom normalise_idempotent : ...` — +statements we can *use* but cannot *prove*. Porting to Lean makes +each such statement a **theorem** the kernel checks. The project's +medium-term goal is to maximise what can be reasoned about in Lean; +that forecloses FFI-backed hiding of mathematical content. + +The Rust implementation was itself AI-assisted and is not +hand-polished artefact we are throwing away; it is a +test-oracle-quality scaffold that the Lean port can match against. + +## Reference materials + +- `zigzag-engine/papers/zigzag-normalisation-2205.08952.pdf` — + Heidemann-Reutter-Vicary, LICS 2022. The algorithm (Construction 17) + and correctness (Proposition 19). +- `zigzag-engine/papers/layout-algorithm-2305.06938.pdf` — + Tataru-Vicary, 2024. Explosion / k-points / layout. +- `zigzag-engine/papers/homotopy-io-2402.13179.pdf` — + Corbyn et al., FSCD 2024. The parent proof assistant. +- `zigzag-engine/zigzag-engine/src/*.rs` — reference Rust + implementation (11,003 lines across 13 modules). +- `zigzag-engine/zigzag-engine-spec/zigzag-engine-spec.md` — original + spec for the reference implementation. + +## Port destination + +All Lean modules land under `CubicalTransport/Zigzag/`: + +| Lean module | Rust reference | Approx. size | +|-------------|----------------|--------------| +| `Zigzag/Monotone.lean` | `src/monotone.rs` (325 LOC) | ~150 LOC + proofs | +| `Zigzag/Core.lean` | `src/zigzag.rs` (291 LOC) | ~150 LOC | +| `Zigzag/Diagram.lean` | `src/diagram.rs` (1484 LOC) | ~600 LOC | +| `Zigzag/Signature.lean` | `src/signature.rs` (200 LOC) | ~100 LOC | +| `Zigzag/Degeneracy.lean` | `src/degeneracy.rs` (1284 LOC) | ~500 LOC + proofs | +| `Zigzag/Normalise.lean` | `src/normalise.rs` (849 LOC) | ~400 LOC + proofs | +| `Zigzag/Typecheck.lean` | `src/typecheck.rs` (597 LOC) | ~250 LOC | +| `Zigzag/Explosion.lean` | `src/explosion.rs` (1414 LOC) | ~500 LOC | +| `Zigzag/Tests.lean` | `tests/` + `examples/` | ~200 LOC `#eval` regressions | + +**Intentionally not ported:** +- `src/import.rs` (1491 LOC) — homotopy.io interop, not needed. +- `src/discover.rs` (1981 LOC) — search over diagrams; decide later. +- `src/python.rs` (716 LOC) — Python bindings, not needed. +- `src/layout.rs` (320 LOC) — geometric layout; deferred to Phase 4 + Interaction, may be a Lean module or may defer to a Rust + `@[implemented_by]` optimisation later. + +Core port size: roughly **2,500–3,000 Lean lines** to match the +algorithmic core of the Rust implementation, with proofs adding +perhaps another 1,000–2,000 depending on how far the correctness +theorems are pursued (Step 9 below). + +--- + +## Steps + +### Step 1 — `Zigzag/Monotone.lean` (foundation) + +**Content**: +- `MonotoneMap (n m : Nat)` structure with `entries : List (Fin m)` + and `is_monotone` proof. +- Composition, identity, face maps `dᵢ`. +- Wraith's R equivalence `Δ₊ → Δ₌ᵒᵖ` as a pure function. +- Preimage computation. + +**Proofs**: +- `MonotoneMap.compose_assoc` +- `MonotoneMap.wraith_r_involution` (R² = id on the nose) +- `MonotoneMap.face_map_image` — face maps omit exactly one element. + +**Deliverable test**: `#eval` the `inspect_half_braid` example's +monotone substructure; compare to the Rust engine's output on the +same input. + +--- + +### Step 2 — `Zigzag/Core.lean` (zigzags themselves) + +**Content**: +- `Zigzag (T : Type) : Type` — `{ regular : Vec T, singular : Vec T, + forward : Vec Morphism, backward : Vec Morphism }`. +- `ZigzagMap` — singular map `fˢ : n → m` in `Δ₊` with regular/singular + slices and the commutativity conditions as `Prop`-valued fields. +- Composition of zigzag maps. + +**Proofs**: +- `ZigzagMap.compose_respects_commutativity` — composition preserves + the commutativity predicates. +- `Zigzag.identity_is_length_zero` — the identity zigzag is trivially + a zero-length zigzag. + +--- + +### Step 3 — `Zigzag/Diagram.lean` (the main data structure) + +**Content**: +- Mutual inductive `Diagram` / `DiagramN` / `Cospan` / `Rewrite` / + `Cone`. Same shape as Rust's `pub enum Diagram { Diagram0(Generator) + | DiagramN(DiagramN) }`. +- Smart constructors: `Diagram.identity`, `Diagram.attach`, + `Diagram.compose`. +- Dimension predicate `Diagram.dimension : Diagram → Nat`. +- Source/target extractors. +- Regular-slice / singular-slice computation (mirrors + `DiagramN.regular_slice` in the Rust). + +**Proofs**: +- `Diagram.dimension_of_attach` — attaching a generator of dimension `k` + produces a diagram of dimension `k`. +- `Diagram.source_source` / `Diagram.target_target` boundary + consistency. +- Globularity predicate + decidability. + +--- + +### Step 4 — `Zigzag/Signature.lean` + +**Content**: +- `Generator` structure: id, dimension, invertibility. +- `GeneratorData` with source / target diagrams. +- `Signature` as a list/hashmap of `GeneratorData`. +- Well-formedness: every `GeneratorData`'s source / target dimension + = `generator.dimension - 1`. + +**Proofs**: +- `Signature.well_formed` is decidable. + +--- + +### Step 5 — `Zigzag/Degeneracy.lean` + +**Content**: +- Predicates: `IsSimpleDegeneracy`, `IsParallelDegeneracy`, + `IsDegeneracy` (closure under composition of the first two). +- Constructors: `Degeneracy.insert_identity_cospan` (the basic simple + degeneracy). +- Factorisation: every degeneracy factors as simple ∘ parallel + (Lemma 7 from the paper). + +**Proofs**: +- `Degeneracy.isomorphisms_are_degeneracies` (Lemma 6). +- `Degeneracy.factorisation_unique_up_to_iso` (Lemma 7). +- `Degeneracy.is_monomorphism` (Lemma 8). +- `Degeneracy.left_cancellation` (Lemma 10). +- `Degeneracy.finite_subobjects` (Lemma 14). + +**This step is where the bulk of the Phase 1-style proof work sits.** +Some of these may start as `axiom` and promote to `theorem` as the +infrastructure firms up — same pattern as how T1/T2/C1/C2 worked in +`Cubical/TransportLaws.lean`. + +--- + +### Step 6 — `Zigzag/Pullback.lean` (Proposition 13) + +**Content**: +- Pullback construction for degeneracy maps. +- `pullback_is_degeneracy` statement. + +**Proofs**: +- `Degeneracy.pullback_exists` — the construction terminates. +- `Degeneracy.pullback_legs_are_degeneracies` (Proposition 13). + +**Note**: Proposition 13 is the most algorithmically dense piece. **OK +to start as an axiom**. Pattern to follow: state the axiom, write the +construction as a `partial def` with test-case regression, upgrade to +a total def + theorem when the proof is clearer. Exactly how +`step`/`eval` were handled in Phase 1. + +--- + +### Step 7 — `Zigzag/Normalise.lean` (Construction 17) + +**Content**: +- `NormalisationResult` structure: `normal_form`, `degeneracy`, + `factorisations`. +- `Sink` structure for relative normalisation. +- `normalise : Diagram → NormalisationResult` (absolute case). +- `normalise_sink : Sink → NormalisationResult` (relative case). +- Termination: structural recursion on `Diagram.dimension`. + +**Proofs**: +- `normalise_idempotent` — the headline result (easy, structural). +- `normalise_preserves_globularity` (Proposition 23). +- `normalise_correctness` (Proposition 19) — relative to the axiom + set from Steps 5–6. + +**Test**: port Rust unit tests from `tests/integration_tests.rs` to +Lean `#eval` regressions (Eckmann-Hilton dim 3, syllepsis dim 5, +Figure 6 dim 4 essential-identity). + +--- + +### Step 8 — `Zigzag/Typecheck.lean` + +**Content**: +- `SingularContent` extraction. +- Piece decomposition. +- `type_check : Diagram → Signature → Except TypeError Unit`. + +**Proofs**: +- `type_check_sound` — if `type_check D Σ` returns `ok`, then all + pieces' normalisations are in `Σ`. + +--- + +### Step 9 — `Zigzag/Tests.lean` (regression battery) + +Port the Rust test cases: +- `tests/integration_tests.rs` — normalisation regressions. +- `tests/nontrivial_constructors.rs` — diagram construction. +- `examples/inspect_half_braid.rs` — the Eckmann-Hilton braiding. +- `examples/render_braiding.rs` — braiding as a 3-diagram. +- `examples/scaffold_analysis.rs` / `trace_scaffold.rs` / `trace_merge.rs` — reduction traces. + +Each becomes a Lean `#eval` or `example` proving the expected output. +These are the correctness gradient that catches porting errors early. + +--- + +### Step 10 — `Cell/Zigzag.lean` (bridge to cubical core) + +**Content**: +- Translator: `CType → Option Diagram` for the dimensions where both + make sense (0-cells, 1-cells, 2-cells-via-Path). +- Translator: `Diagram → Option CType` for the inverse. +- Identity / compose / whisker operations at the `Cell` layer that + dispatch to the right backend: cubical for low dimensions (where + univalence matters), zigzag for higher dimensions (where + combinatorial composition dominates). + +**This is where the two formalisms meet.** Cubical Phase 1 gives us +equivalence and transport; Zigzag gives us higher-composition and +normalisation; `Cell/` combines them. + +--- + +## Explosion and layout (post-core) + +Steps 11+ (not critical for the n-category reasoning goal): +- `Zigzag/Explosion.lean` — k-points, poset structure. Lean-native + port of `src/explosion.rs` (1414 Rust LOC). +- `Zigzag/Layout.lean` — constraint system. May remain pure Lean or + may defer the QP solver to a Rust `@[implemented_by]` optimisation. + **Decided later** once performance requirements are known. + +--- + +## Axiom discipline (from Phase 1 experience) + +The port follows the same axiom-first pattern established in Phase 1: + +1. **First pass**: data structures pure; algorithm as `def` (maybe + `partial def`); key correctness statements as `axiom`. +2. **Second pass**: tighten `partial def` into `def` with structural + termination; promote axioms to theorems where the proof is + mechanical. +3. **Third pass**: prove the hard theorems (Proposition 13, correctness + of Construction 17 relative to the degeneracy axioms). + +At every stage, axioms are **formal specs for what the algorithm must +satisfy**, not blanket assumptions. The Rust reference implementation +tests each axiom via example; the Lean port must match those tests. + +--- + +## Relationship to the broader project + +- **Phase 1 (Cubical Core)** — complete in this engine repo + (`CubicalTransport/*`). Not touched by this port. +- **Phase 2 (Cells)** — lives in the sibling `topolei` interface + repo. The zigzag Lean port *is* a prerequisite for cells-spec + §6.3 "Higher Cells": topolei's `Cell/Basic.lean` (when it lands) + can begin using cubical-only semantics for 0/1/2-cells, and higher + cells then use the zigzag backend from Step 10 below. When the + port lands here in the engine, the `topolei` repo gains higher-cell + capability without local code changes — that is the cascade. +- **Rust FFI (cubical evaluator)** — independent work stream within + this engine repo. The zigzag port does not depend on it. When the + Rust FFI lands, it backs the cubical axioms; the zigzag Lean code + becomes a consumer of the now-computational cubical layer. +- **Numerical layer** (`NUMERICAL.md`) — independent. Schemes can use + zigzag diagrams as structural source / target types once the port + is complete. + +--- + +## Sizing + +- Steps 1–4: ~2 weeks (data structures + basic algorithms). +- Steps 5–7: ~3–4 weeks (degeneracy + normalisation + proofs; this + is the heart of the port). +- Step 8: ~3 days. +- Step 9: ~1 week (regression battery). +- Step 10: ~1 week (bridge). +- **Total: 6–8 weeks** for the core port with correctness theorems. + +Comparable to Phase 1 in size; same single-developer feasibility. + +--- + +## Success criteria + +The port is **complete** when: + +1. All regression tests from `zigzag-engine/tests/` pass as Lean + `#eval`s or `example`s. +2. `normalise_idempotent` is a theorem (not an axiom). +3. The Eckmann-Hilton (dim 3), syllepsis (dim 5), and Figure 6 (dim 4) + examples type-check and normalise to their documented results. +4. `Cell/Zigzag.lean` (Step 10) compiles and bridges to the cubical + core without circular dependencies. +5. The sibling `topolei/STATUS.md` can claim "Phase 2 Higher-Cell + backend: closed in Lean" with zero new Rust dependency (beyond the + cubical-evaluator FFI in this engine, which is a separate work + stream). + +At that point, topolei has a Lean-native combinatorial n-category +engine, provably correct where proven, with the Rust zigzag engine +demoted from reference to archive. diff --git a/native/cubical/README.md b/native/cubical/README.md index 7021488..b00eb36 100644 --- a/native/cubical/README.md +++ b/native/cubical/README.md @@ -46,7 +46,7 @@ Artifacts: via `node test/wasm_harness.mjs`). See `WASM.md` for integration with a Lean-wasm composite artifact. - **Phase D.properties ✅**: 46 property-based tests in - `Topolei/Cubical/PropertyTest.lean` covering λ β-rules, Σ β-rules, + `CubicalTransport/PropertyTest.lean` covering λ β-rules, Σ β-rules, eval determinism, DimExpr idempotence + literals, FaceFormula absorption, readback roundtrip. 55/55 total (9 smoke + 46 property). - **Phase D.bench ✅**: baseline perf benchmarks via `cubical-bench` @@ -66,7 +66,7 @@ lake build cubical-test Expected output: `── 9 / 9 passed ──`, covering λ-fragment eval, Σ β-rules, readback, and normalizer reductions. Source: -`Topolei/Cubical/FFITest.lean` + `CubicalTest.lean`. +`CubicalTransport/FFITest.lean` + `CubicalTest.lean`. ### Wasm smoke tests (Node.js harness)