flipCount
plain-language theorem explainer
Encodes the Gray-code flip multiplicities on the three axes of the cube Q₃ as the triple (4, 2, 2). Anyone deriving the Wolfenstein A parameter, face fluxes, or the 44-connection from Q₃ chirality cites this table. It is a pure by-cases definition, not a proved count.
Claim. Define the Gray-code flip count on the three axes of the 3-cube by $f(0)=4$, $f(1)=2$, $f(2)=2$. That is, axis $0$ flips four times per eight-tick cycle and axes $1$ and $2$ each flip twice.
background
The module derives the Wolfenstein CKM parameter $A$ from the geometry of the 3-cube $Q_3$ (eight vertices, the eight-tick octave of the forcing chain). Edges of $Q_3$ are traversed in Gray-code order: successive vertices differ by a single bit flip, and each flip is assigned to one coordinate axis.
The observed chirality of that Gray code is the multiplicity triple $[4,2,2]$: four flips on axis $0$, two on axis $1$, two on axis $2$. Generation indices are identified with axes (gen $1\mapsto$ axis $0$, etc.). Face flux between two generations is then the sum of the flip counts on the two spanning axes.
This table is the numerical seed for the five-line derivation that produces $A_{\mathrm{corrected}}=9/11$ and for the shared factor $44=4\times 11$ that also appears in $\alpha^{-1}$ and $\eta_B$.
proof idea
Definitional: pattern-match on the three values of $\mathrm{Fin},3$ and return the constants $4$, $2$, $2$. No lemmas, no tactics. The companion one-line theorems flip_axis0/1/2 simply unfold the definition by rfl.
why it matters
This is step 1 of the module's five-line derivation of $A$. Downstream, faceFlux sums two values of the table; berry_correction_eq then obtains the Berry factor $3/2$ as the ratio of face fluxes $6/4$. Multiplying the structural ratio $\Delta\tau_{23}/\Delta\tau_{12}=6/11$ by that factor yields $A_{\mathrm{corrected}}=9/11$, certified inside CKMExactCert and rephrased as $N_c^2/\Delta\tau_{12}$ in A_from_color_and_torsion.
The same $4=f(0)$ enters the 44-connection: $44=4\times 11$ appears identically in the fine-structure formula, the baryon-to-photon ratio $\eta_B\approx\varphi^{-44}$, and the CKM expression. Thus the table is the geometric origin of the shared Q₃ chirality that ties CKM mixing to $\alpha$ and cosmology. Framework landmarks: eight-tick octave (T7) and $D=3$ (T8) supply the cube whose Gray code is being counted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.