cyclePerm
plain-language theorem explainer
The 8-cycle map on the cube vertices: each vertex goes to the next one along the Gray-code path of the eight-tick octave. Anyone building the cycle operator, its period-8 facts, or the CKM/CP path from the Q₃ schedule cites this map. The definition is the one-line composition of Gray order with its inverse shifted by one tick.
Claim. Define a map $\sigma:\{0,\ldots,7\}\to\{0,\ldots,7\}$ by $\sigma(v)=G\bigl(G^{-1}(v)+1\bigr)$, where $G$ is the Gray-code ordering of the eight vertices of the 3-cube (tick $\mapsto$ vertex) and $G^{-1}$ is its inverse (vertex $\mapsto$ tick). Thus if $v$ is visited at tick $t$, then $\sigma(v)$ is the vertex visited at tick $t+1$ (mod 8).
background
The module builds the cycle operator on $\mathbb{C}^8$: the unitary permutation matrix induced by the directed 8-tick Gray-code tour of the vertices of the 3-cube $Q_3$. Those eight vertices are the natural basis; one full period of the tour is the algebraic object whose eigenvalues (8th roots of unity) and eigenphases feed generation structure and mixing.
Two auxiliary maps fix the schedule. The Gray order $G$ sends tick index to the vertex visited at that tick (the standard gray8At path). Its inverse $G^{-1}$ sends a vertex to the unique tick at which it appears. Adding one tick and reapplying $G$ advances one step along the Hamiltonian cycle on $Q_3$, flipping exactly one bit per step.
This sits in the eight-tick octave forced by the Recognition foundation chain (period $2^3$), the discrete time base for recognition dynamics on the cube.
proof idea
Pure definition, not a proved theorem. The body is the single term $v\mapsto G(G^{-1}(v)+1)$, with $G$ the Gray order and $G^{-1}$ the explicit inverse table (vertex $\mapsto$ tick). No tactics or lemmas are invoked at the definition site; later native_decide and fin_cases proofs expand this composition against the concrete Gray tables.
why it matters
This map is the combinatorial skeleton of the cycle operator $U_{\mathrm{cycle}}$: the permutation matrix of $\sigma$ is the unitary whose eighth power is the identity and whose DFT-8 eigenmodes carry the per-tick phases used for generation and mixing. Downstream, the certificate bundles period eight, minimality of that period, injectivity, and the identity of each step with a single bit flip; separate lemmas record the explicit table $0\mapsto 1,,1\mapsto 3,\ldots$, injectivity, exact period 8, and non-identity before 8 iterates.
The same permutation seeds the canonical path in the CP-phase derivation, so the Gray cycle on $Q_3$ is the bridge from the eight-tick foundation (T7) to Standard-Model phase structure. Without a fixed, bijective advance map there is no well-defined $U_{\mathrm{cycle}}$ and no eigenvalue story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.