bit_flip_counts
plain-language theorem explainer
Across the eight-step Gray-code Hamiltonian cycle on the 3-cube, coordinate bit 0 flips four times while bits 1 and 2 each flip twice. Anyone tracing the combinatorial origin of chirality or CP violation in Recognition Science would cite this count. The proof is a one-line native decision on the finite flip schedule.
Claim. For the Gray-code Hamiltonian cycle on the 3-cube $Q_3$, let $b_k \in \{0,1,2\}$ be the coordinate bit flipped at step $k$ of the eight-tick cycle. Then $|\{k : b_k = 0\}| = 4$, $|\{k : b_k = 1\}| = 2$, and $|\{k : b_k = 2\}| = 2$.
background
The module studies signed winding numbers of a Hamiltonian cycle on the 3-cube $Q_3$ around each of its six faces. Each face corresponds to a generation pair; the winding measures how the eight-tick cycle wraps the face boundary, and a nonzero winding is the geometric origin of CP violation in Recognition Science.
The schedule of which coordinate flips at each step is the function sending step index $k \in {0,\ldots,7}$ to a bit in ${0,1,2}$. Explicitly it is the Gray-code flip list: bit 0, then 1, then 0, then 2, then 0, and so on. Counting how often each bit appears in that list is the elementary combinatorial input to face-pair structure and asymmetric winding.
This sits inside the eight-tick octave forced at T7 of the unified forcing chain, with spatial dimension $D = 3$ forced at T8, so the cube $Q_3$ and its Gray cycle are the discrete geometry underlying the recognition clock.
proof idea
The proof is a pure computational check: build the length-8 list of flipped bits by evaluating the flip schedule at every Fin 8 index, then ask Lean’s native decision procedure to verify the three multiplicity equalities (four zeros, two ones, two twos). No algebraic lemmas are invoked; the finite domain makes the claim decidable by enumeration.
why it matters
The doc-comment states the point directly: the 4-vs-2-vs-2 asymmetry is the combinatorial origin of chirality. Opposite faces (same axis, different side) are each traversed by the cycle, but the uneven flip schedule means different face-pairs see different winding patterns. That feeds the module’s main line: face windings, total chiral charge (proved nonzero), and the geometric account of CP violation.
Framework landmarks: the eight-tick period is T7; three spatial bits are T8’s $D = 3$. Without this count, the later claim that the cycle distinguishes forward from backward on faces would lack its elementary source. No downstream theorems currently depend on it in the graph, so it is a proved leaf that closes the flip-schedule side of the face-winding story rather than an intermediate lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.