cycle_step_is_bitflip
plain-language theorem explainer
Each step of the Gray-code cycle on the 3-cube equals a single bit flip, the bit named by the tick. Anyone assembling the cycle operator on ℂ⁸ or the CKM-from-cube pipeline cites this identity. The proof is exhaustive case analysis on the eight ticks, discharged by native decision.
Claim. For every tick $t \in \{0,\ldots,7\}$, the cycle permutation applied to the Gray-ordered vertex at $t$ equals the single-bit flip of that same vertex on the bit selected by $t$.
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 cube $Q_3$. The eight vertices form the standard basis; one full period is the permutation that advances each vertex one step along the Gray path.
By construction of Gray codes on $Q_3$, consecutive vertices differ in exactly one coordinate. The helper bitFlipOp k flips bit $k$ of a vertex index in $\mathrm{Fin},8$. The tick-dependent choice of which bit moves is flippedBit t. The cycle permutation and the Gray ordering of ticks are the other two ingredients of the identity.
This sits inside the eight-tick octave (forcing step T7, period $2^3$): the directed recognition dynamics on the cube, later packaged as an $8\times 8$ permutation matrix whose eigenvalues are the 8th roots of unity.
proof idea
Term-mode proof by exhaustive case split: fin_cases t expands the eight values of $t:\mathrm{Fin},8$, and each goal is closed by native_decide. No algebraic lemmas are invoked; both sides are concrete functions on a finite type, so native evaluation settles equality pointwise.
why it matters
The identity is one of the five fields of cycleOpCert, the certificate that the cycle permutation has period eight, is minimal, is injective, advances by single bit flips, and has the stated flip asymmetry. Without it, the geometric claim that each tick is a pure edge of $Q_3$ would be missing from the certificate.
That certificate underwrites the cycle operator $U_{\mathrm{cycle}}\in\mathrm{GL}(8,\mathbb{C})$, the algebraic object from which the module derives CKM mixing: eigenvalues are 8th roots of unity and eigenstates are DFT-8 modes (the same modes used in Born-rule forcing). Framework landmark: T7 eight-tick octave on the cube, with $D=3$ spatial bits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.