four_from_chirality
plain-language theorem explainer
Along Gray-code axis 0 of the Q₃ cube, the bit-flip count is exactly 4. Anyone deriving the Wolfenstein A parameter or the shared 44-factor in α⁻¹, η_B, and CKM cites this as the chirality input of the [4,2,2] pattern. The equality is definitional: closed by rfl against the flipCount table.
Claim. The Gray-code flip count on spatial axis $0$ equals $4$: if $N_0$ is the number of bit flips of the $Q_3$ Gray code when only the $0$-th coordinate changes, then $N_0 = 4$.
background
Module CKMExact derives the Wolfenstein parameter $A$ from $Q_3$ face-flux geometry, with zero sorry and zero axioms. The opening step is the Gray-code chirality pattern $[4,2,2]$: flip counts $(N_0,N_1,N_2)=(4,2,2)$ on the three spatial axes of the three-cube.
flipCount tallies how many edges of the Gray-code Hamiltonian path on $Q_3$ flip a given axis bit. Axis $0$ is the distinguished long axis of that path; axes $1$ and $2$ are the short pair. The same $[4,2,2]$ data later multiplies generation torsion $\Delta\tau_{12}=11$ to produce the integer $44$ that also appears in $\alpha^{-1}$ and $\eta_B$.
Local setting is the five-line chain: Gray flips $\to$ generation torsion ${0,11,17}$ $\to$ structural $A=6/11$ $\to$ face-flux correction $3/2$ $\to$ $A_{\mathrm{corrected}}=9/11$.
proof idea
Term-mode proof by rfl. The left-hand side is flipCount evaluated at the Fin-3 index $0$ (well-formed by norm_num); the right-hand side is the numeral $4$. Both sides reduce definitionally to the same natural, so reflexivity closes the goal. No lemmas are applied beyond the definition of flipCount and the axis table that encodes the Gray path.
why it matters
This is step 1 of the module's five-line derivation of $A_{\mathrm{corrected}}=9/11\approx 0.818$ (PDG $0.826\pm 0.013$, within $0.6\sigma$). The doc-comment pins the meaning: "$4=$ flipCount(axis$_0$) from the $[4,2,2]$ chirality of the Gray code."
Together with $\Delta\tau_{12}=11$ it supplies the factor $44=4\times 11$ that the module identifies as common to three RS observables: $\alpha^{-1}=44\pi\cdot\exp(-w_8\ln\varphi/44\pi)$, $\eta_B\approx\varphi^{-44}$, and $A_{\mathrm{corrected}}=9/11$. That is the "$44$ connection" governed by $Q_3$ chirality times generation torsion.
No downstream theorems are wired yet in the graph (used_by empty), but sibling lemmas flip_axis1, flip_axis2, and total_flips complete the $[4,2,2]$ triple that feeds A_structural_eq and A_corrected_exact. Framework landmarks: eight-tick/$Q_3$ geometry (T7) and the three-generation ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.