Docs cleanup: archive PHASE1, accept ZIGZAG_PORT, fix stale paths

- 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) <noreply@anthropic.com>

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
 

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.

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.

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.

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)