gen3_flips
plain-language theorem explainer
Generation 3, identified with cube axis 2, is driven exactly twice per eight-tick Gray-code cycle. Anyone citing the generation-coupling asymmetry (the kinematic source of flavor mixing) needs this count. The proof is a one-line wrapper equating generationFlipCount to bitFlipCount and applying the native decision that bit 2 flips twice.
Claim. If each particle generation is identified with a coordinate axis of the 3-cube and the flip count of a generation is the number of times that axis flips along the canonical 8-tick Gray-code cycle, then generation 3 (axis 2) has flip count $2$.
background
The module establishes that the canonical 3-bit Gray-code cycle on the cube $Q_3$ is chiral: the directed walk $[0,1,3,2,6,7,5,4]$ flips bits in the pattern $[0,1,0,2,0,1,0,2]$. Bit 0 flips four times; bits 1 and 2 each flip twice. That $4:2:2$ split breaks $S_3$ axis-permutation symmetry and is the Recognition Science origin of CP violation and flavor mixing.
Face-pairs of the cube correspond to the three particle generations. The map generationFlipCount simply reuses the per-axis bit-flip count: how many times per cycle the recognition operator actively drives that generation. Upstream, bit2_flips_two already records that axis 2 flips twice (proved by native_decide on the explicit cycle). The eight-tick period itself is the T7 landmark of the forcing chain.
proof idea
One-line term wrapper. By definition generationFlipCount is identical to bitFlipCount, so the claim reduces to bitFlipCount 2 = 2, which is exactly the already-proved lemma bit2_flips_two.
why it matters
This is the generation-3 half of the coupling asymmetry: generations 2 and 3 each see two flips while generation 1 sees four. The module doc states that this asymmetry "is the kinematic source of flavor mixing — it forces the mass and weak eigenstates to be misaligned." Together with the sibling counts for axes 0 and 1 it feeds the flip-asymmetry vector $\Delta = (4/3,-2/3,-2/3)$ used by flipAsymmetryNonzero and cycle_is_chiral, and ultimately the CP-breaking / CPT-preserving certificates. It sits inside the eight-tick (T7) Gray-code geometry that also forces $D=3$ (T8). No downstream dependents are recorded yet; the declaration is a named interface for the generation-coupling story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.