ClosedWalkOnCube
plain-language theorem explainer
A closed walk on the D-dimensional hypercube is a phase-indexed map from the 2^D discrete ticks into the space of D-bit patterns. Anyone citing the T7 cycle realization (eight-tick octave, circle image of a Hamiltonian cube walk) uses this carrier type. It is a bare structure definition: one field, no proof obligations.
Claim. For each natural number $D$, a closed walk on the $D$-cube is a map $\mathrm{path}\colon \{0,\ldots,2^D-1\}\to\{\text{$D$-bit patterns}\}$ that indexes vertices of the hypercube by discrete phase.
background
The module T7 Cycle Realization supplies the theorem surface for the strengthened T7/T8 dimension route: the T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed walk in the cube graph realizes a higher sphere $S^p$ for $p\ge 2$. Smooth-topology content stays predicate-level; the module proves elementary finite-dimensional arithmetic and exposes the names the forcing chain needs.
The $D$-cube has $2^D$ vertices, each a $D$-bit pattern. A closed walk is therefore a map from a cyclic phase set of size $2^D$ into that vertex set. The sibling predicate Hamiltonian asserts that this map is bijective (every vertex visited exactly once). Spatial dimension $D=3$ is the value forced by T8 in the forcing chain, giving the familiar eight-tick octave $2^3=8$.
Upstream, the Gray-cycle infrastructure supplies concrete paths on the cube; this structure is the common type those paths inhabit when treated as closed walks.
proof idea
No proof: this is a structure definition with a single field path. Downstream predicates (Hamiltonian as bijectivity of the path, edge-distinctness, circle image) and theorems are stated relative to inhabitants of this type. Instantiation is by supplying a concrete phase-to-pattern map, as in the explicit 3-bit Gray cycle closed walk.
why it matters
This carrier is the common domain for the T7 cycle realization package. Downstream, Hamiltonian closed walks are shown (at the present predicate layer) to have circle image, edge-distinct realizability for $D\ge 2$, and to realize no higher sphere $S^p$ with $p\ge 2$. The explicit Gray cycle on $Q_3$ is packaged as an inhabitant, feeding the eight-tick octave of T7 and the $D=3$ step of T8 in the forcing chain.
Parent results that quantify over this type include the circle-image theorem for Hamiltonian walks, the edge-distinctness API for $D\ge 2$, the no-higher-sphere obstruction, and the concrete Gray-cycle walk on the 3-cube. The module reserves full CW/covering-dimension formalization for a later Mathlib-backed pass; the structure itself is already the stable interface those later proofs will reuse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.