gen1_flips
plain-language theorem explainer
Generation 1, identified with cube axis 0, is driven by four bit flips in one 8-tick Gray-code cycle. Anyone citing the 4:2:2 generation-coupling split or the geometric origin of flavor asymmetry would quote this equality. The proof is a one-line term that reuses the native decision of the bit-0 flip count.
Claim. The number of times generation $1$ (axis $0$) is actively driven in one Gray-code cycle equals $4$: if $N(g)$ is the flip count of the axis paired to generation $g$, then $N(1)=4$.
background
The module studies the canonical 3-bit Gray-code walk on the cube $Q_3$, the directed 8-tick path $[0,1,3,2,6,7,5,4]$ with flip pattern $[0,1,0,2,0,1,0,2]$. That walk is the recognition operator's discrete trajectory. J-cost is symmetric, $J(x)=J(1/x)$, which the module identifies with CPT; chirality of the directed path is what breaks CP while preserving CPT.
Face-pairs of the cube are identified with fermion generations, and each generation is tied to a coordinate axis. The flip count on that axis is how many times per cycle the generation is actively driven. The definition generationFlipCount is exactly the per-bit flip counter, so generation index $0$ is axis $0$. Upstream, bit0_flips_four already records that bit $0$ flips four times (by native_decide on the fixed cycle).
proof idea
One-line term proof: the claim is definitionally the same as bit0_flips_four, because generation flip counts are the bit flip counts. No extra tactics; the equality is just the already-proved bitFlipCount 0 = 4 under that alias.
why it matters
This pins the first coordinate of the flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$ that the module uses to prove the Gray cycle is chiral and that generations couple unequally. The 4:2:2 split breaks $S_3$ axis permutation and is the stated RS origin of flavor mixing (CKM/PMNS) and of CP violation with CPT intact (T7 eight-tick octave on $Q_3$). No downstream Lean users are wired yet; the equality is a named generation-facing restatement of the bit-0 count for the generation-coupling narrative and the master chirality certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.