bitFlipCount
plain-language theorem explainer
Counts how often a chosen cube axis (bit in Fin 3) flips along the canonical 8-tick Gray-code walk on Q₃. Downstream work cites it for the 4:2:2 flip pattern that breaks S₃ and feeds the chirality×torsion route to the η_B rung −44. The body is a one-line list count of the flippedBit schedule.
Claim. For each axis $b \in \{0,1,2\}$, $\mathrm{bitFlipCount}(b)$ is the number of steps of the length-8 Gray-code cycle on the 3-cube at which axis $b$ is the flipped coordinate.
background
The module GrayCodeChirality treats the directed 8-tick recognition walk on the 3-cube $Q_3$ as the geometric source of CP violation. The walk is the Gray code $[0,1,3,2,6,7,5,4]$; successive edges flip a single bit, recorded by flippedBit : Fin 8 → Fin 3 with schedule $[0,1,0,2,0,1,0,2]$.
J-cost is symmetric, $J(x)=J(1/x)$, so particle↔antiparticle exchange (CPT) is preserved. Chirality arises because the directed path treats the three axes unequally: bit 0 flips four times, bits 1 and 2 twice each. Face-pairs are identified with particle generations, so unequal flip counts couple generations asymmetrically.
This definition is the raw histogram of that schedule: for a fixed axis it counts occurrences of that axis in the eight-step flip list. Sibling lemmas then prove the concrete values 4, 2, 2 and the nonzero flip-asymmetry vector $(4/3,-2/3,-2/3)$.
proof idea
Definitional, not a proof. Build the finite list List.ofFn flippedBit (the eight values of the Gray-code flip schedule) and apply List.count at the chosen bit : Fin 3. No tactics or lemmas beyond the upstream schedule flippedBit and ordinary list cardinality.
why it matters
This is the counting primitive behind Gray-code chirality and the CP-breaking story in the module. The 4:2:2 histogram is what flipAsymmetryNonzero, cycle_is_chiral, and generation-coupling asymmetry rest on; under cycle reversal winding signs flip while J-symmetry (CPT) stays intact.
Downstream, cosmology uses it heavily. eta_B_rung_from_chirality is defined as $-(bitFlipCount(0)\cdot|torsionGap(0,1)|)=-(4\times 11)=-44$, and chirality_product_equals_gap_minus_one equates that product to the dimension-gap identity $D^2(D+2)-1-A$ at $D=3$. The same integer enters EtaBExactRungCert as route B among the three arithmetic expressions of $-44$.
Framework landmarks: T7 eight-tick octave (period $2^3$) and T8 $D=3$ fix the cube and the walk length; the asymmetric flip pattern is the RS origin of flavor mixing and of the chirality factor in the baryon-asymmetry rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.