flip_axis1
plain-language theorem explainer
Along spatial axis 1 of the Q₃ cube, the Gray-code Hamiltonian path flips that bit exactly twice. Anyone deriving the Wolfenstein A parameter from Q₃ face flux cites this as the middle entry of the [4,2,2] flip signature. The proof is pure definitional reflexivity on the piecewise flipCount table.
Claim. If $\mathrm{flipCount}:\mathrm{Fin}\,3\to\mathbb{N}$ records Gray-code bit flips on the three spatial axes of $Q_3$, then $\mathrm{flipCount}(1)=2$.
background
The module derives the Wolfenstein CKM parameter $A$ from first-principles $Q_3$ geometry. The opening step is the Gray-code flip signature on the three-cube: the unique (up to orientation) Hamiltonian cycle on the vertices of $Q_3$ flips coordinate axes with multiplicities $[4,2,2]$.
flipCount is the piecewise definition of that multiplicity: axis $0$ contributes $4$ flips, axes $1$ and $2$ contribute $2$ each. The three companion lemmas flip_axis0/1/2 simply expose those table entries as theorems so later arithmetic (total flips, axis asymmetry, face-flux ratios) can cite them by name.
Local setting is the fully closed CKMExact development: zero sorry, zero axioms, ending at $A_{\mathrm{corrected}}=9/11$.
proof idea
One-line definitional reflexivity. The goal is flipCount ⟨1, _⟩ = 2; the second clause of the flipCount match returns 2 on the nose, so rfl closes.
why it matters
This is step 1 of the five-line derivation in the module header: Gray code $[4,2,2]$ supplies the numerator/denominator structure that later multiplies generation torsion $\Delta\tau_{23}/\Delta\tau_{12}=6/11$ by the face-flux correction $3/2$ to give $A_{\mathrm{corrected}}=9/11$. The same $[4,2,2]$ chirality reappears in the “44 connection” ($4\times 11$) that links $\alpha^{-1}$, $\eta_B\approx\varphi^{-44}$, and the CKM $A$ parameter. Downstream siblings (total_flips, gray_asymmetry, gray_axis12_symmetric) assemble the three axis lemmas into the global asymmetry used by the flux correction. Framework landmark: the eight-tick/$D=3$ cube whose Gray code is forced by T7–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.