flippedBit_sequence
plain-language theorem explainer
The bit-flip sequence along the length-8 Gray-code Hamiltonian cycle on the 3-cube is exactly [0,1,0,2,0,1,0,2]. Researchers working face windings, chirality, or CP geometry on Q₃ cite this frozen enumeration. Proof is a one-line native decision of a finite table equality.
Claim. Evaluating the flipped-bit map at every step of the 8-tick Gray cycle on the 3-cube yields the list $[0,1,0,2,0,1,0,2]$. In other words, successive edges of the cycle flip coordinates $0,1,0,2,0,1,0,2$ in that order.
background
The module develops signed winding numbers of a Hamiltonian cycle on the 3-cube $Q_3$, the discrete geometric source of CP violation in Recognition Science. Each of the six faces of $Q_3$ is tied to a generation pair; the winding records net clockwise-minus-counterclockwise traversal of that face by the cycle.
Time is the standard binary-reflected Gray code on three bits (the eight-tick octave). Exactly one coordinate flips at each step. The flipped-bit map $\mathrm{Fin},8\to\mathrm{Fin},3$ records which coordinate flips at step $k$. Its definition is the eight-clause table: steps $0,2,4,6$ flip bit 0; steps $1,5$ flip bit 1; steps $3,7$ flip bit 2.
Freezing that map as an explicit list makes the 4-2-2 flip-count asymmetry available to later combinatorial arguments about face orientation and chirality.
proof idea
One-line computational proof. Both sides are closed finite terms: List.ofFn applied to the eight-clause flipped-bit definition versus the literal list $[0,1,0,2,0,1,0,2]$. The tactic native_decide evaluates the equality in the kernel and closes the goal. No algebraic lemmas are required.
why it matters
The module comment identifies the 4-vs-2-vs-2 flip asymmetry (bit 0 flips four times; bits 1 and 2 twice each) as the combinatorial origin of chirality. Face windings and the nonzero total chiral charge built later in the same file depend on knowing which edges of each face are crossed and in which order; that order is governed by this sequence.
In the RS forcing chain the result sits under the eight-tick octave (T7) and the forcing of three spatial dimensions (T8): the Gray cycle on $Q_3$ is the discrete clock whose face windings seed CP violation. The dependency graph currently lists no downstream consumers, so the lemma functions as an explicit witness inside the face-winding development rather than a widely imported API fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.