cyclePerm_injective
plain-language theorem explainer
The Gray-code cycle map on the eight vertices of the 3-cube is injective, hence a bijection of a finite 8-set. Anyone assembling the unitary cycle operator or the cycle-operator certificate cites this. The proof is exhaustive Fin-8 case analysis against the explicit Gray order and its inverse.
Claim. Let $\sigma:\{0,\ldots,7\}\to\{0,\ldots,7\}$ send each vertex $v$ to the next vertex on the canonical 3-bit Gray-code cycle (tick index of $v$, plus one, mapped back to a vertex). Then $\sigma$ is injective, and therefore bijective.
background
The module builds the cycle operator on $\mathbb{C}^8$: the unitary permutation operator induced by the 8-tick Gray-code walk on the vertices of the 3-cube $Q_3$. Those eight vertices are the computational basis; one full Gray step defines a permutation of the basis, and the corresponding permutation matrix is $U_{\mathrm{cycle}}$.
The cycle permutation itself is defined by conjugating addition-by-one on tick indices with the Gray order: if grayOrder (alias of gray8At) lists vertices in visit order $[0,1,3,2,6,7,5,4]$ and grayOrderInv recovers the tick at which a vertex appears, then $\sigma(v)=\mathrm{grayOrder}(\mathrm{grayOrderInv}(v)+1)$. Explicitly the map is $0\mapsto 1$, $1\mapsto 3$, $2\mapsto 6$, $3\mapsto 2$, $4\mapsto 0$, $5\mapsto 4$, $6\mapsto 7$, $7\mapsto 5$.
Injectivity on a finite set of equal cardinality is the first half of showing $\sigma$ is a genuine 8-cycle permutation (period and minimality are sibling lemmas).
proof idea
Term-mode proof by exhaustive case split. Introduce $a,b:\mathrm{Fin},8$ with $\sigma(a)=\sigma(b)$; run fin_cases on both indices (64 pairs) and discharge each goal by simp_all unfolding cyclePerm, grayOrderInv, grayOrder, and gray8At. No intermediate lemmas are required beyond the explicit lookup tables for the Gray order and its inverse.
why it matters
Feeds directly into cycleOpCert, which packages the structural facts needed for the cycle operator: period eight, minimal period, injectivity, single-bit-flip steps, and flip asymmetry. Without injectivity the permutation matrix would not lie in $\mathrm{GL}(8,\mathbb{C})$ and the spectral story (eigenvalues the 8th roots of unity, DFT-8 eigenmodes, generation phases) would not start.
In the Recognition framework this is the algebraic skeleton of the eight-tick octave (forcing landmark T7): the directed Gray dynamics on $Q_3$ that later sources CKM mixing angles from eigenstate phases. It is a small but load-bearing brick in the Foundation chain from Gray chirality and face winding up to the unitary cycle operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.