bitFlipOp
plain-language theorem explainer
Single-bit flip on the eight vertices of the 3-cube: given bit index k in {0,1,2} and vertex v in Fin 8, return v with bit k toggled via XOR. Anyone building the Gray-code cycle operator or proving that each tick is a pure edge step cites this map. The body is a pure definition: XOR with 1 shifted by k, with a Fin-boundedness proof by exhaustive native_decide.
Claim. For each bit index $k \in \{0,1,2\}$, define the map $F_k : \mathrm{Fin}\,8 \to \mathrm{Fin}\,8$ by $F_k(v) = v \oplus 2^k$ (bitwise XOR of the vertex label with the single bit $k$). The result remains in $\{0,\ldots,7\}$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$ induced by the 8-tick Gray-code traversal of the cube $Q_3$. The eight vertices form the computational basis; each tick advances along a Hamiltonian cycle in which consecutive vertices differ by exactly one bit.
That one-bit change is the geometric content of a recognition tick. Upstream, the holography layer already defines an analogous flip on face configurations: XOR the configuration word with $1 \ll i$ and reduce mod 16. Here the same XOR pattern is specialized to vertex labels in $\mathrm{Fin},8$ and to the three spatial bit axes of $Q_3$.
The Gray-code ordering (grayOrder) and the schedule of which bit flips at tick $t$ (flippedBit) live in sibling definitions. Together they turn the abstract cycle permutation into a product of these elementary bit flips, matching the eight-tick octave forced at T7.
proof idea
Definitional, not a theorem. The map sends $v$ to the subtype element whose value is $v.\mathrm{val}\ \mathrm{XOR}\ (1 \ll k.\mathrm{val})$. Boundedness in $\mathrm{Fin},8$ is discharged by double fin_cases on $k$ and $v$ plus native_decide (24 constant cases). No external lemmas are invoked beyond the bitwise primitives and Fin constructors.
why it matters
This is the elementary generator of the directed 8-tick dynamics. Downstream, cycle_step_is_bitflip equates each Gray-cycle step to exactly one such flip: $\mathrm{cyclePerm}(\mathrm{grayOrder}, t) = F_{\mathrm{flippedBit}, t}(\mathrm{grayOrder}, t)$. The involution theorem records $F_k^2 = \mathrm{id}$, so each edge is its own inverse.
CycleOperatorCert packages both facts into the structural certificate for the cycle operator: period eight, minimal period, injectivity, step-is-bitflip, and Gray-code chirality asymmetry. That certificate underwrites the permutation matrix $U_{\mathrm{cycle}}\in\mathrm{GL}(8,\mathbb{C})$ whose eigenvalues are the 8th roots of unity and whose eigenmodes feed Born-rule forcing and the CKM mixing angles.
In the forcing chain this sits under T7 (eight-tick octave, period $2^3$) and T8 ($D=3$ spatial axes, hence three bit indices). Without a clean single-bit flip there is no algebraic identification of recognition ticks with cube edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.