evenFlipOnVertex
plain-language theorem explainer
An even sign flip acts on the eight vertices of the 3-cube by XOR-ing a two-bit mask that flips exactly one prescribed pair of axes. Anyone assembling the weak eigenbasis from the cube's SU(2) gauge action cites this map. The body reads the axis pair from the even-flip generator table, packs it into a bit mask, and XORs that mask onto the vertex label, with a finite-case bound proof.
Claim. For each generator index $g \in \{0,1,2\}$ and each vertex $v \in \{0,\ldots,7\}$ of the 3-cube $Q_3$, return the vertex obtained by flipping the two coordinate bits selected by $g$: axes $(0,1)$ when $g=0$, $(0,2)$ when $g=1$, and $(1,2)$ when $g=2$. Equivalently, XOR the integer label of $v$ with the corresponding two-bit mask in $\{3,5,6\}$.
background
The module builds the two orthonormal bases on generation space whose overlap is the CKM matrix. Mass eigenstates come from the CW filtration and torsion rungs; weak eigenstates come from the SU(2) subgroup of the cube gauge group, realized as even sign flips (Layer 2 of GaugeFromCube).
Vertices of $Q_3$ are labeled by $\mathrm{Fin},8$, i.e. 3-bit strings. An even sign flip toggles exactly two bits at once, preserving the parity of the number of 1-bits. The sibling table evenFlipGenerator lists the three independent pairs: axes $(0,1)$, $(0,2)$, and $(1,2)$. That table is the only combinatorial input to this map.
These flips generate the weak irreps that later assign each generation to an SU(2) doublet. The mismatch between that assignment and the mass-axis assignment forces nonzero mixing angles.
proof idea
Pure definition, not a theorem. Read the Boolean triple of axes from the even-flip generator table for the given index; pack it into the integer mask $1\cdot[\mathrm{axis},0]+2\cdot[\mathrm{axis},1]+4\cdot[\mathrm{axis},2]$ (so the three generators yield masks 3, 5, and 6); return the subtype element whose value is the bitwise XOR of the input vertex with that mask. The subtype bound is discharged by exhaustive fin_cases on generator and vertex plus native_decide.
why it matters
This is the concrete action of the even sign-flip generators on vertex states, the operational form of the SU(2) cube gauge subgroup used for the weak basis. The immediate parent is the involution theorem: applying the same flip twice recovers the identity, which is needed before the flips can serve as group elements or projectors onto weak doublets.
In the broader RS picture the weak basis is one of the two decompositions of $\mathbb{C}^8$ on $Q_3$; the other is the mass basis from CW filtration and torsion ${0,11,17}$ on the $\varphi$-ladder. Their axis mismatch is what forces CKM mixing. The construction sits downstream of the eight-tick / Gray-code cube structure (T7) and the gauge-from-cube layer that isolates even flips as the SU(2) content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.