generationFlipCount
plain-language theorem explainer
Each fermion generation is identified with a cube axis; its flip count is how many times that axis flips on the canonical eight-tick Gray-code walk. The map is definitionally the bit-wise flip counter on Fin 3. Chirality, CKM/PMNS coupling, and Cabibbo-angle arguments cite it as the kinematic drive strength per generation. The body is a pure alias, not a computation.
Claim. For each generation index $i \in \{0,1,2\}$, write $N(i)$ for the number of times bit $i$ flips along the directed 8-tick Gray-code cycle on the 3-cube $Q_3$. The generation flip count is the map $i \mapsto N(i)$, identical to the axis bit-flip count.
background
The module Gray Code Chirality treats the canonical 3-bit Gray walk on $Q_3$ as the geometric carrier of the eight-tick recognition operator. The walk flips bits in the pattern $[0,1,0,2,0,1,0,2]$: bit 0 flips four times per cycle, bits 1 and 2 twice each. That $4:2:2$ split breaks $S_3$ axis symmetry and is the RS source of CP violation while J-cost symmetry $J(x)=J(1/x)$ keeps CPT.
Upstream, the bit-flip count of an axis is the multiplicity of that bit in the flipped-bit list of the cycle. Face-pairs of the cube are identified with the three fermion generations, so each generation inherits the flip count of its axis. The eight-tick period is the T7 octave of the forcing chain; the three axes are the $D=3$ spatial directions of T8.
Locally, the generation flip count is just a semantic rename of the bit-flip count, so later statements can speak in generation language without changing the underlying arithmetic.
proof idea
One-line definitional alias: the generation flip count is set equal to the bit-flip count on Fin 3. No tactics, no lemmas, no computation. Downstream equalities such as generation 1 seeing four flips are proved by rewriting through this alias to the already-established bit counts (bit0_flips_four, bit1_flips_two, bit2_flips_two).
why it matters
This alias is the bridge from cube geometry to flavor physics. It feeds gen1_flips, gen2_flips, gen3_flips and the coupling asymmetry theorem, which states generation 1 is driven twice as often as generations 2 and 3 and is called the kinematic source of mass–weak misalignment. That asymmetry is packaged into ChiralityCert and reused by large_cabibbo_from_coupling_ratio, whose doc-comment ties the $2:1$ drive ratio to the large Cabibbo angle versus smaller $2$–$3$ mixing.
In the framework landmarks this sits under T7 (eight-tick octave) and T8 ($D=3$): the directed Gray path on the 3-cube is chiral, so CP breaks while CPT (J-symmetry) is preserved. Without a generation-indexed flip count, the module could not state flavor coupling in particle language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.