cyclePerm_explicit
plain-language theorem explainer
Explicit lookup table for the 8-tick Gray-code cycle on the vertices of the 3-cube: 0→1, 1→3, 2→6, 3→2, 4→0, 5→4, 6→7, 7→5. Anyone building the cycle operator U_cycle, checking period-8 dynamics, or tracing CKM phases from the Gray path cites this table. Proof is a one-line native decision procedure evaluating the definition on Fin 8.
Claim. Let $\sigma:\{0,\ldots,7\}\to\{0,\ldots,7\}$ be the cycle map that sends each vertex of $Q_3$ to the next vertex one tick later along the Gray-code ordering. Then $\sigma(0)=1$, $\sigma(1)=3$, $\sigma(2)=6$, $\sigma(3)=2$, $\sigma(4)=0$, $\sigma(5)=4$, $\sigma(6)=7$, and $\sigma(7)=5$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary induced by the directed 8-tick Gray-code walk on the vertices of the 3-cube $Q_3$. Those eight vertices form the standard basis; advancing one tick flips exactly one bit and therefore permutes the basis.
The underlying permutation is defined by conjugating modular increment by the Gray ordering: if $v$ is visited at tick $t$, the image is the vertex visited at tick $t+1$. In symbols, $\sigma(v)=\mathrm{grayOrder}(\mathrm{grayOrderInv}(v)+1)$. The present statement simply expands that abstract map on every residue mod 8.
This sits inside the eight-tick octave (forcing step T7): period $2^3$ on a 3-bit cube is the discrete clock from which eigenvalues, DFT-8 modes, and later mixing angles are read off.
proof idea
One-line computational proof. After unfolding the definition $\sigma(v)=\mathrm{grayOrder}(\mathrm{grayOrderInv}(v)+1)$, both grayOrder and its inverse are concrete Fin 8 maps, so the eight equalities are closed ground terms. native_decide evaluates them in the kernel and discharges the conjunction.
why it matters
Gives the concrete wiring diagram for the cycle permutation that underlies the permutation matrix $U_{\mathrm{cycle}}\in\mathrm{GL}(8,\mathbb{C})$. Downstream results in the same module (injectivity, exact period 8, non-identity before tick 8, and the identification of each step with a single bit flip) all rest on knowing where each vertex goes.
In the broader Recognition chain this is the algebraic skeleton of the eight-tick octave (T7): eigenvalues are the 8th roots of unity, eigenstates are DFT-8 modes used in Born-rule forcing, and the per-tick phases feed generation structure and CKM mixing. The module doc states that $U_{\mathrm{cycle}}$ is precisely the object from which the CKM matrix emerges; the explicit table is the first checkable witness that the Gray path really is a single 8-cycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.