cyclePerm_period
plain-language theorem explainer
The Gray-code cycle permutation on the eight cube vertices has period eight: its eighth iterate is the identity on every vertex. Anyone citing the algebraic period of the recognition cycle (cycle-operator certificate, CP-phase path closure) depends on this fact. The proof is exhaustive case analysis on Fin 8 decided by native computation.
Claim. Let $\sigma$ be the Gray-code cycle permutation on the eight vertices of the 3-cube (each step advances one tick along the Gray path). Then for every vertex $v$, $\sigma^{8}(v)=v$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary induced by the 8-tick Gray-code cycle on the vertices of $Q_3$. Those eight vertices form the natural basis; one tick flips exactly one bit (the bit named by the Gray schedule), so the dynamics is a permutation of Fin 8.
That permutation is defined by advancing the Gray order by one: if $v$ is visited at tick $t$, the image is the vertex visited at $t+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$. The present theorem records that this map has period eight on the nose.
In the broader forcing chain this is the combinatorial content of the eight-tick octave (T7): one full recognition cycle returns every vertex state to itself before any continuous unitary or eigenvalue analysis begins.
proof idea
Term-mode proof by exhaustion. Introduce an arbitrary vertex $v:\mathrm{Fin},8$, case-split on all eight values, and discharge each equality by native decision on the concrete definition of the cycle permutation. No intermediate lemmas are required beyond the definition of the permutation itself; the finite domain makes the period check a pure computation.
why it matters
This is the period half of the cycle-operator certificate: the certificate packs period eight, minimality of that period, injectivity, and the bit-flip step law into one verified bundle. Downstream, the Standard Model CP-phase derivation uses it twice: once to identify the canonical eight-tick transport path with the eighth iterate of the permutation, and once as the direct return-to-start lemma after eight ticks.
Physically it underwrites the claim that eigenvalues of the cycle operator are eighth roots of unity and that DFT-8 modes are the eigenbasis. That is the algebraic seed for generation-dependent phase accumulation and the CKM mixing angles built later in the same module family. It is the discrete T7 landmark (eight-tick octave) stated at the level of the vertex permutation, before the matrix form $U_{\mathrm{cycle}}^8=I$ is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.