evenFlip_involution
plain-language theorem explainer
Each even sign-flip on the cube Q₃ is an involution: applying the same generation-labeled flip twice returns every vertex to itself. Anyone building the weak eigenbasis from SU(2) even flips (or checking that those generators square to the identity) cites this. The proof is exhaustive finite case analysis over three generators and eight vertices, discharged by native decision.
Claim. For every generation index $g \in \{0,1,2\}$ and every vertex $v \in Q_3 \cong \mathrm{Fin}\,8$, the even sign-flip associated to $g$ satisfies $\sigma_g(\sigma_g(v)) = v$.
background
The module constructs the two orthonormal bases on generation space whose overlap is the CKM matrix: mass eigenstates from the CW/torsion filtration on Q₃, and weak eigenstates from the SU(2) gauge subgroup realized as even sign flips (GaugeFromCube Layer 2). Vertices are the eight points of the 3-cube; generations are labeled by Fin 3.
An even flip generator flips a complementary pair of spatial axes (σ₂₃, σ₁₃, σ₁₂), leaving one axis fixed. The sibling map evenFlipOnVertex applies that generator pointwise on Fin 8. The weak-basis pairing identifies each generation with the flip whose fixed axis is the generation's complement axis, so these maps are the concrete SU(2) action used downstream.
Involution is the minimal algebraic sanity check: each generator must be order two before one can treat the weak basis as an orthonormal frame built from those irreps.
proof idea
Pure finite exhaustion. Case-split on the generation index gen : Fin 3, then on the vertex v : Fin 8, and discharge each of the 24 concrete equalities by native_decide. No intermediate lemmas are invoked; the statement is a closed computation on the explicit bit-flip tables of the three even generators.
why it matters
In RS the weak basis is not postulated: it is the eigenframe of the even sign-flip SU(2) action on Q₃. Establishing that each generator is an involution licenses treating those flips as reflections (Weyl-type generators) rather than open orbits, which is required before assigning generations to doublets and before reading mixing angles off mass/weak axis mismatch.
The module's main arc is that mass axes come from CW torsion rungs {0, 11, 17} on the φ-ladder while weak axes come from these even flips; their mismatch forces CKM mixing. This lemma is a local algebraic brick under that weak-side construction. No downstream theorem currently depends on it in the graph, so it sits as infrastructure for the weak-basis and MixingAngleData development rather than a cited parent step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.