cyclePerm_not_identity_before_8
plain-language theorem explainer
The Gray-code cycle permutation on the eight cube vertices has no smaller positive period than 8: for every k with 0 < k < 8 there is a vertex moved by the k-fold iterate. Anyone proving that the cycle operator is a genuine order-8 element (not a divisor) cites this. The proof is a finite case split on k with native evaluation at vertex 0.
Claim. Let $\sigma$ be the cycle permutation of the eight vertices of the 3-cube induced by the Gray-code path (each step advances one tick along the path). Then for every integer $k$ with $0 < k < 8$ there exists a vertex $v$ such that $\sigma^k(v) \neq v$. Equivalently, no positive power of $\sigma$ strictly less than 8 is the identity.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary permutation matrix induced by the 8-tick Gray-code cycle on the vertices of the 3-cube $Q_3$. Those eight vertices form the standard basis; one tick advances along the Gray path by flipping exactly one bit.
The underlying combinatorial map is cyclePerm: if $v$ is visited at tick $t$, the image is the vertex visited at $t+1$, written $\mathrm{grayOrder}(\mathrm{grayOrderInv}(v)+1)$. Explicitly the orbit is $0\mapsto 1\mapsto 3\mapsto 2\mapsto 6\mapsto 7\mapsto 5\mapsto 4\mapsto 0$. A companion result already records that the eighth iterate is the identity; the present statement is the matching lower bound on the period.
This sits in the Recognition Science forcing chain at the eight-tick octave (T7, period $2^3$): the directed recognition dynamics on the cube must close only after a full octave, not at a proper divisor.
proof idea
Term-mode proof by exhaustive case analysis. Introduce $k$ with $0<k<8$, then interval_cases k splits into the seven concrete values $k=1,\ldots,7$. On each branch it suffices to exhibit one moved point: take the vertex $0$ and discharge $\sigma^k(0)\neq 0$ by native_decide against the explicit Gray-order table. No algebraic lemma beyond the definition of cyclePerm is required.
why it matters
Feeds directly into cycleOpCert as the minimal_period field, alongside period-eight, injectivity, and the single-bit-flip step law. Without this fact the certificate would only know $U_{\mathrm{cycle}}^8=I$, not that the algebraic order is exactly 8.
Exact order 8 is what forces the eigenvalues to be the full set of 8th roots of unity and the eigenstates to be the DFT-8 modes used downstream for Born-rule forcing and generation mixing. In the framework primer this is the T7 eight-tick octave: the directed recognition cycle on $Q_3$ cannot collapse to a shorter closed loop. The CKM-oriented reading of the cycle operator (phases accumulated per tick) likewise needs a primitive 8-cycle rather than a product of shorter cycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.