flippedBit
plain-language theorem explainer
Records, for each of the eight Gray-code steps on the 3-cube, which coordinate axis flips. Anyone proving cycle chirality, face windings, or the cycle-operator certificate cites this table. The body is an exhaustive case split on Fin 8 matching the standard binary-reflected Gray path.
Claim. Let the vertices of $Q_3$ be indexed by $\{0,\ldots,7\}$ in Gray-code order. The map $t \mapsto k(t)$ with $k(t)\in\{0,1,2\}$ returns the unique bit position that changes between consecutive vertices of the cycle: $000\to001$ flips bit $0$, $001\to011$ flips bit $1$, and so on through the eight edges, ending with $100\to000$ flipping bit $2$.
background
The module FaceWinding equips the 3-cube $Q_3$ with signed face windings of a fixed Hamiltonian cycle, the geometric seed of CP violation in Recognition Science. Vertices are bit-strings of length 3; edges flip exactly one bit. The cycle is the standard 8-step Gray path (the eight-tick octave of the forcing chain, T7).
Each cube face fixes one axis and one side value. An edge lies on a face only when the flipped bit is not that fixed axis and both endpoints match the face side. The present map is the bookkeeping that names, at each cycle step, which axis moves.
Downstream counts of how often each axis flips (the 4:2:2 split) break $S_3$ symmetry among axes and feed generation-axis coupling and chiral charge.
proof idea
Pure definition by exhaustive pattern match on Fin 8. Each clause hard-codes the bit that differs between successive Gray-code vertices, as annotated in the source comments (e.g. step 0: $000\to001$ flips bit 0; step 3: $010\to110$ flips bit 2). No lemmas are invoked; the table is the content.
why it matters
This table is the combinatorial spine of cube chirality. In the same module it drives bit_flip_counts (bit 0 flips four times, bits 1 and 2 twice each) and axis_flip_asymmetry, which break axis-permutation symmetry, and it enters edgeOnFace and edgeFaceSign used to build faceWinding and the nonzero total chiral charge.
In CycleOperator it identifies each cycle step with a single bit-flip operator (cycle_step_is_bitflip), appears in the cycle-operator certificate, and underlies axis-flip counts that couple generations to axes. Framework-wise it sits under the eight-tick octave (T7) and the $D=3$ cube (T8), converting the Gray cycle into the signed face windings that RS treats as the geometric origin of CP violation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.