flip_axis2
plain-language theorem explainer
On the three-cube Gray-code walk, the bit-flip count along spatial axis 2 equals 2. Anyone deriving the Wolfenstein A parameter from Q₃ face flux cites this as the axis-2 half of the chirality signature [4,2,2]. The proof is pure definitional unfolding by rfl.
Claim. The Gray-code flip count on the cube along axis $2$ is exactly $2$: $\mathrm{flipCount}(2) = 2$.
background
The module derives the Wolfenstein CKM parameter $A$ from first principles of $Q_3$ geometry (the three-cube). The opening step records the Gray-code chirality signature $[4,2,2]$: along the three spatial axes the closed Gray walk flips bit $0$ four times and bits $1$ and $2$ twice each.
flipCount is the Fin-3-indexed table of those counts, defined by cases as $4$, $2$, $2$. Axis $2$ is the last coordinate of that table. Together with the companion statements for axes $0$ and $1$, this pins the geometric input that later multiplies generation torsion $\Delta\tau$ and face-flux ratios to give $A_{\mathrm{corrected}}=9/11$.
proof idea
One-line definitional proof. The goal is flipCount ⟨2, _⟩ = 2. By the third clause of the case-split definition of flipCount, the left-hand side reduces definitionally to $2$, so rfl closes.
why it matters
This is line 1 of the five-line CKMExact derivation in the module doc: Gray code $[4,2,2]$ with flip counts $(4,2,2)$ on axes $(0,1,2)$. The same $[4,2,2]$ chirality reappears in the “44 connection”: $44=4\times 11$ links $\alpha^{-1}$, the baryon-to-photon ratio $\eta_B\approx\varphi^{-44}$, and $A_{\mathrm{corrected}}=9/11$. Downstream the three flip-count lemmas feed total_flips, gray_asymmetry, and the structural ratio $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$ before the face-flux correction $3/2$ yields $9/11\approx 0.818$ (PDG $0.826\pm 0.013$). No used_by edges are recorded yet; the lemma is scaffolding for those later equalities inside the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.