gray_axis12_symmetric
plain-language theorem explainer
Gray-code flip counts on spatial axes 1 and 2 are equal (both 2), encoding the [4,2,2] chirality of the Q₃ cube. Anyone deriving CKM structure or the Wolfenstein A correction from Q₃ geometry cites this symmetry. The proof is pure definitional equality: both sides reduce to 2.
Claim. The Gray-code flip count on axis $1$ equals that on axis $2$: $\mathrm{flipCount}(1)=\mathrm{flipCount}(2)$ (both equal $2$).
background
Module CKMExact derives the Wolfenstein parameter $A$ from Q₃ face-flux geometry, with zero sorry and zero axioms. The starting datum is the Gray-code flip pattern $[4,2,2]$ on the three cube axes: axis 0 flips four times, axes 1 and 2 flip twice each.
flipCount is the Fin-3 lookup encoding that pattern: $\langle 0\rangle\mapsto 4$, $\langle 1\rangle\mapsto 2$, $\langle 2\rangle\mapsto 2$. Generation labels (first/second/third) arise from parity patterns across the same three dimensions, so axis symmetry between 1 and 2 is the geometric seed of generation torsion later in the module.
The local derivation chain is: Gray flips $\to$ generation torsion ${\Delta\tau_{12}=11,\Delta\tau_{23}=6}$ $\to$ structural $A=6/11$ $\to$ face-flux correction $3/2$ $\to$ $A_{\mathrm{corrected}}=9/11$.
proof idea
Term-mode one-liner by rfl. Both sides of the equality are applications of flipCount at concrete Fin 3 values $\langle 1\rangle$ and $\langle 2\rangle$; the definition reduces each to the literal natural $2$, so reflexivity closes the goal with no lemmas.
why it matters
Locks the axis-1/axis-2 half of the $[4,2,2]$ Gray chirality that the module treats as first-principles input. Downstream, ckmExactCert packages $A_{\mathrm{structural}}=6/11$, the Berry face-flux factor $3/2$, and $A_{\mathrm{corrected}}=9/11$ (PDG $0.826\pm 0.013$, RS within $0.6\sigma$).
The same $[4,2,2]\times$ torsion geometry produces the factor $44=4\times 11$ that appears in $\alpha^{-1}$, $\eta_B\approx\varphi^{-44}$, and the CKM $A$ formula. Without axis-1/2 equality the face-flux ratio $\mathrm{faceFlux}(12)/\mathrm{faceFlux}(23)=6/4$ would not be forced, and the $9/11$ prediction would lose its geometric warrant. Ties to the eight-tick/Q₃ octave (T7) and three-generation structure forced upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.