bitFlipOp_involution
plain-language theorem explainer
Flipping the same coordinate bit twice on an 8-vertex cube index returns the original vertex. Anyone building the Gray-code cycle operator or relating cycle steps to single-bit flips needs this involution. The proof is exhaustive case analysis on the three bit indices and eight vertices, discharged by native decision.
Claim. For every bit index $k \in \{0,1,2\}$ and every vertex label $v \in \{0,\ldots,7\}$, applying the single-bit flip of coordinate $k$ twice yields $v$ again: $F_k(F_k(v)) = v$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$ induced by the 8-tick Gray-code Hamiltonian cycle on the cube $Q_3$. The eight vertices form the computational basis; each tick advances along an edge that flips exactly one coordinate bit.
The operator bitFlipOp k is the map on Fin 8 that XORs the vertex index with $2^k$, i.e. toggles bit $k$. Upstream, flippedBit records which bit flips at each step of the Gray cycle, so each cycle step is expected to equal one of these bit-flip maps.
An involution statement is the algebraic prerequisite for treating those flips as order-two generators of the cycle dynamics and for relating the permutation matrix of the full period-8 cycle to a product of bit flips.
proof idea
Pure finite exhaustion. Case-split on the three values of $k$ and the eight values of $v$, then native_decide checks the concrete XOR identity $(v \oplus 2^k) \oplus 2^k = v$ on each pair. No intermediate lemmas are invoked; the definition of the bit-flip map is unfolded by the decision procedure.
why it matters
Inside Recognition Science the eight-tick octave (forcing landmark T7) is realized as the Gray cycle on $Q_3$. The cycle operator’s eigenvalues are the 8th roots of unity and feed generation structure and CKM mixing. Establishing that each elementary bit flip squares to the identity is the elementary group-law fact behind writing cycle steps as bit flips (the sibling claim that each cycle step equals the flip named by flippedBit). Even with no recorded downstream users yet, the lemma closes the order-two property needed before period-8 and eigenstructure results for $U_{\mathrm{cycle}}$ can be trusted as products of those flips.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.