cubical-transport-hott-lean4/docs/ZIGZAG_PORT.md

# 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.