grayCycle3ClosedWalk
plain-language theorem explainer
Packages the canonical 3-bit Gray cycle as a closed walk on the 3-cube Q₃. Anyone citing the T7 eight-tick realization (circle defect, no higher spheres) uses this object as the concrete witness. The definition is a one-field structure instance: the walk path is exactly the period-8 Gray path on 3-bit patterns.
Claim. Let $Q_3$ be the 3-dimensional hypercube graph on $2^3=8$ vertices (3-bit patterns). The standard binary-reflected Gray cycle of length 8 is recorded as a closed walk $W$ on $Q_3$, i.e. a map $W:\mathrm{Fin}(8)\to\{\text{3-bit patterns}\}$ given by the Gray path of period 8.
background
The module strengthens the 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 realizes a higher sphere $S^p$ for $p\ge 2$. Smooth topology stays predicate-level; the module supplies the finite arithmetic and the exact names the forcing chain needs.
A closed walk on the $D$-cube is a phase-indexed path through $D$-bit pattern space: a structure with a single field path : Fin(2^D) → Pattern D. Hamiltonian means that path is bijective (every vertex visited once). The upstream Gray object is the 3-bit Gray-cycle path of period 8, Fin 8 → Pattern 3, built from the standard Gray code on eight labels.
T7 in the forcing chain forces the eight-tick octave (period $2^3$). This definition is the concrete $D=3$ walk that later theorems identify with that octave.
proof idea
Not a proof: a structure instance. The type is ClosedWalkOnCube 3, whose only field is a path Fin(2^3) → Pattern 3. The body sets that field to the existing Gray path of period 8. No tactics, no lemmas beyond the type former.
why it matters
This is the canonical witness for T7 cycle realization at $D=3$. Downstream, it is shown to be Hamiltonian, to realize as a circle under any cellular completion of dimension 3, and not to realize as $S^p$ for $p\ge 2$. The unified forcing chain's T7-to-realization bridge is literally the statement that, for every cellular completion of dimension 3, the realized defect of this walk equals the circle.
In the primer landmarks this sits at T7 (eight-tick octave, period $2^3$) and feeds the T7/T8 dimension route toward $D=3$ spatial dimensions. Without a named closed walk, the realization theorems have nothing concrete to specialize to.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.