grayOrder
plain-language theorem explainer
Aliases the canonical 3-bit Gray path as the tick-to-vertex schedule on the cube Q₃: tick t visits vertex grayOrder(t) in the fixed sequence 0,1,3,2,6,7,5,4. Anyone building the eight-tick cycle operator or its permutation cites this map. The body is a one-line alias of the upstream Gray schedule.
Claim. Define the Gray order map $g:\{0,\ldots,7\}\to\{0,\ldots,7\}$ by $g(t)=$ the vertex index visited at tick $t$ along the standard 3-bit Gray cycle $(0,1,3,2,6,7,5,4)$. Thus $g$ sends tick index to cube-vertex label.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary induced by the directed 8-tick Gray walk on the 3-cube $Q_3$. The eight vertices form the computational basis; one full Gray lap is the fundamental recognition period (the eight-tick octave of the forcing chain).
Upstream, gray8At is the fixed schedule Fin 8 → Fin 8 with values $[0,1,3,2,6,7,5,4]$. Consecutive labels differ by a single bit flip, so the walk is a Hamiltonian cycle on $Q_3$. The RS tick $\tau_0=1$ is the discrete time unit; eight ticks close one octave.
grayOrder is simply that schedule under the name used throughout the cycle-operator construction: tick index in, vertex index out. Its inverse (defined next) recovers when each vertex is visited.
proof idea
Pure definitional alias: grayOrder is set equal to the upstream Gray schedule gray8At. No proof obligations; the concrete case table lives in Patterns.GrayCycle.
why it matters
This map is the coordinate chart for all cycle dynamics in the module. The cycle permutation is defined by advancing one tick in Gray order: $v\mapsto g(g^{-1}(v)+1)$. Injectivity of that permutation, the left/right inverse laws for $g^{-1}$, and the identity that each step equals a single bit flip all quote grayOrder directly.
The certificate structure bundles period-eight, minimal period, injectivity, step-is-bitflip, and flip asymmetry; every clause is stated in terms of this order. Downstream, the permutation matrix $U_{\mathrm{cycle}}$ has eigenvalues the 8th roots of unity and DFT-8 eigenmodes, the algebraic seed for generation structure and CKM mixing in the Recognition framework (T7 eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.