total_flips
plain-language theorem explainer
The three Q₃ Gray-code axis flip counts sum to 8: 4+2+2. Anyone deriving Wolfenstein A from face-flux corrections, or citing the broken S₃ chirality of the eight-tick Gray code, uses this identity. The proof is pure definitional reflexivity after unfolding the piecewise flipCount table.
Claim. If the Gray-code flip counts on the three spatial axes of the 3-cube are $4$, $2$, and $2$ respectively, then their sum equals $8$ (one bit flip per tick of the eight-tick cycle).
background
The module derives the Wolfenstein CKM parameter $A$ from Q₃ geometry. The cube's Gray-code Hamiltonian cycle on eight vertices (the eight-tick octave) flips one bit per edge. Counting flips by axis yields the chirality pattern $[4,2,2]$, not the symmetric $[8/3,8/3,8/3]$.
Locally, flipCount is the piecewise table sending axis $0\mapsto 4$, $1\mapsto 2$, $2\mapsto 2$. The Foundation GrayCodeChirality development proves the same total via native decision on bit-flip counters and records that the imbalance breaks $S_3$ axis-permutation symmetry. That total of eight is the T7 landmark: period $2^3$.
Downstream steps multiply these counts into generation torsion $\Delta\tau_{12}=11$, $\Delta\tau_{23}=6$ and face-flux ratios to obtain $A_{\mathrm{corrected}}=9/11$.
proof idea
One-line definitional proof. Unfolding flipCount at the three Fin 3 constructors yields the ground term $4+2+2$, which reduces by rfl to $8$. No lemmas are invoked; the equality is closed by the kernel after reduction of the piecewise definition.
why it matters
Closes the first line of the five-line CKMExact derivation: Gray code $[4,2,2]$ with total flips $8$. That total is the eight-tick octave (forcing-chain T7) realized as one flip per tick. The same $[4,2,2]$ pattern feeds the "44 connection": $44=4\times 11$ appears in $\alpha^{-1}$, in $\eta_B\approx\varphi^{-44}$, and in the structural factor of $A_{\mathrm{corrected}}=9/11$. The Foundation twin theorem states the identical sum for bit-flip counters and uses the imbalance to prove $S_3$ is broken; this module-local copy anchors the CKM arithmetic on the same geometric fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.