grayFlipCounts
plain-language theorem explainer
Names the per-axis bit-flip tally of the canonical 3-bit Gray code walk on the cube as a map from axes to natural numbers. Anyone citing Gray-code chirality, CP breaking, or the baryon-asymmetry sign chain uses this map as the flip-count input to IsChiral. It is a one-line alias of the list-count definition that tallies flips along the eight-tick path.
Claim. Let $Q_3$ carry the canonical 3-bit Gray code cycle of length 8. Define the flip-count function $c:\{0,1,2\}\to\mathbb{N}$ by $c(i)=$ number of edges in the cycle that flip coordinate $i$. Explicitly $c=(4,2,2)$ on the three axes.
background
The module treats the directed 8-tick recognition walk on the 3-cube as the geometric source of CP violation. The walk is the Gray path $[0,1,3,2,6,7,5,4]$, whose successive bit flips are the pattern $[0,1,0,2,0,1,0,2]$. Counting occurrences yields four flips of axis 0 and two each of axes 1 and 2, breaking $S_3$ permutation symmetry of the cube axes.
Upstream, bitFlipCount is exactly that tally: for each bit index it counts how often that index appears in the flipped-bit list of the cycle. The J-cost $J(x)=J(1/x)$ remains particle–antiparticle symmetric (CPT), so any CP breaking must come from the directed path geometry rather than from the cost functional.
Face-pairs of the cube are identified with particle generations, so unequal flip counts mean unequal generation couplings over one octave (period $2^3$, landmark T7).
proof idea
Pure definitional alias: the flip-count map is definitionally equal to the existing per-bit list-count along the Gray cycle. No tactics, no lemmas beyond unfolding the synonym. Downstream theorems such as cycle_is_chiral then feed this map into IsChiral and discharge the unequal-count obligation by native_decide on the concrete values 4 and 2.
why it matters
This is the named flip-count object that every chirality and CP statement in the module consumes. cycle_is_chiral, cp_broken_by_chirality, and cpt_ok_cp_broken all assert IsChiral of this map; ChiralityCert packages that fact with the explicit counts $[4,2,2]$ and CPT preservation via $J(x)=J(x^{-1})$.
Cosmology reuses it: derivation_chain_complete lists IsChiral grayFlipCounts as the chirality link from the Gray path to a positive Jarlskog invariant and positive baryon asymmetry sign; BaryonAsymmetryCert sits on that chain. Standard-model side, CKMStructureCert draws on the same generation-asymmetric coupling.
Framework landmarks: eight-tick octave (T7), $D=3$ spatial axes as generations (T8), and the contrast with J-symmetry (T5) that keeps CPT while the directed walk breaks CP. The 4:2:2 split is the concrete geometric origin of flavor mixing and the baryon-asymmetry sign in RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.