gen2_flips
plain-language theorem explainer
Generation 2, identified with cube axis 1, experiences exactly two bit flips in one eight-tick Gray-code cycle on Q₃. Anyone comparing generation-dependent drive of the recognition operator across the three face-pair generations cites this count. The proof is a one-line alias of the native decision that bit 1 flips twice.
Claim. The flip count attached to generation $2$ (cube axis $1$) equals $2$: that generation is actively driven twice per eight-tick Gray-code cycle.
background
The module proves that the canonical 3-bit Gray-code cycle on the cube $Q_3$ is chiral, and takes that chirality as the Recognition Science geometric origin of CP violation. 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 while bits 1 and 2 each flip twice, so the $4{:}2{:}2$ split breaks $S_3$ axis-permutation symmetry of the cube.
Face-pairs of $Q_3$ are identified with the three fermion generations. The map generationFlipCount sends each axis index in $\mathrm{Fin},3$ to the number of times that bit flips in one cycle; it is definitionally equal to the raw bit-flip counter. Upstream, the lemma that bit 1 flips twice is already proved by native_decide on the explicit cycle.
proof idea
One-line term wrapper: the claim is definitionally identical to the upstream equality that bit 1 flips twice, because the generation flip-count map is just the bit-flip counter reindexed by axis. No extra algebra or case split is required.
why it matters
This is one of the three generation-coupling counts that make the $4{:}2{:}2$ asymmetry concrete. Together with the axis-0 count of four and the axis-2 count of two, it supplies the numerical content of generation-coupling asymmetry: different generations are driven unequally by the eight-tick recognition operator (T7 octave). That unequal drive is the module's proposed origin of flavor mixing (CKM/PMNS), while J-cost symmetry $J(x)=J(1/x)$ keeps CPT intact. No downstream theorem currently depends on this alias alone; it exists to name the generation-2 slot in the chirality certificate bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.