grayFlipAxis
plain-language theorem explainer
Assigns to each of the eight Gray-code steps on the 3-cube the coordinate axis that flips at that step. Anyone counting Q₃ axis flips for the Wolfenstein A correction cites this table. It is a pure pattern-match on Fin 8 encoding the cycle 000→001→011→010→110→111→101→100.
Claim. Define $g:\{0,\ldots,7\}\to\{0,1,2\}$ by the Gray-code traversal $000\to001\to011\to010\to110\to111\to101\to100\to000$, sending step index $k$ to the unique spatial axis flipped at that step: $g(0)=0$, $g(1)=1$, $g(2)=0$, $g(3)=2$, $g(4)=0$, $g(5)=1$, $g(6)=0$, $g(7)=2$.
background
The module derives the Wolfenstein CKM parameter $A$ from $Q_3$ geometry. The three-cube carries the eight-tick Gray code (the closed Hamiltonian path on the vertices of ${0,1}^3$). Each edge of that path flips exactly one coordinate; the sequence of flipped axes is the content of this map.
Recognition Science forces an eight-tick octave (T7) and $D=3$ spatial dimensions (T8), so the Gray code on $Q_3$ is the natural discrete clock. Downstream counts of how often each axis flips yield the chirality signature $[4,2,2]$, which multiplies generation torsion to produce $A_{\mathrm{corrected}}=9/11$.
Sibling definitions flipCount and flip_axis0/1/2 simply tally the preimages of this map.
proof idea
Definition by exhaustive case split on Fin 8. Each constructor is assigned a Fin 3 literal, with norm_num discharging the bound proofs. No lemmas are invoked; the body is the lookup table itself.
why it matters
This table is the atomic input to the five-line derivation of $A_{\mathrm{corrected}}=9/11$ stated in the module doc. Step 1 of that derivation reads off flip counts $(4,2,2)$ for axes $(0,1,2)$ directly from the preimages of $g$. Those counts reappear in the "44 connection": $4\times 11$ links the fine-structure constant, the baryon-to-photon ratio $\eta_B\approx\varphi^{-44}$, and the CKM $A$ parameter, all governed by the same $Q_3$ chirality.
Without a fixed Gray-code axis sequence there is no well-defined face-flux correction, so the structural ratio $\Delta\tau_{23}/\Delta\tau_{12}=6/11$ cannot be upgraded to the PDG-compatible $9/11$. The definition therefore sits at the base of the fully proved (0 sorry, 0 axioms) CKMExact result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.