weakComplementAxis
plain-language theorem explainer
For each of the three weak-basis generations, the complement axis is the spatial axis left unflipped by that generation's even sign-flip generator on the cube. The assignment is the identity map on Fin 3. Anyone building the weak eigenstate basis for the RS CKM construction cites it. The body is a three-clause pattern match, one clause per generation index.
Claim. Define the weak complement axis assignment $w:\{0,1,2\}\to\{0,1,2\}$ by $w(i)=i$. Generation $1$ (resp. $2$, $3$) is paired with axis $0$ (resp. $1$, $2$), the unique axis not flipped by the corresponding even sign-flip $\sigma_{23}$ (resp. $\sigma_{13}$, $\sigma_{12}$) from the cube $SU(2)$ gauge action.
background
The module builds the two orthonormal bases on generation space whose overlap is the CKM matrix: mass eigenstates from the CW filtration and torsion rungs, and weak eigenstates from the $SU(2)$ subgroup of the cube gauge action (even sign flips). Both live on the same $Q_3$ structure but decompose $\mathbb{C}^8$ by different principles, so the bases need not coincide.
Even sign flips $\sigma_{ij}$ come from GaugeFromCube Layer 2. Each such generator flips two spatial axes and leaves one fixed. The fixed axis is the natural label for the weak-basis generation tied to that generator: $\sigma_{23}$ fixes axis $0$, $\sigma_{13}$ fixes axis $1$, $\sigma_{12}$ fixes axis $2$.
This definition records that pairing as a map on $\mathrm{Fin},3$. Downstream code treats it as the weak-basis axis assignment and immediately proves it is the identity.
proof idea
Pure definition by pattern match on $\mathrm{Fin},3$. The three constructors return $0$, $1$, and $2$ respectively; there is no lemma application and no tactic proof. The inline comments record the physical reading (which even flip leaves which axis fixed). The companion theorem weakComplement_is_identity later discharges $\forall i,, w(i)=i$ by fin_cases and rfl.
why it matters
This is the weak half of the mass/weak axis labeling that forces CKM mixing in RS. The module doc states that mass axes come from CW filtration and torsion ${0,11,17}$ on the $\varphi$-ladder, while weak axes come from even sign-flip irreps; the mismatch between those decompositions is the geometric origin of flavor mixing.
Downstream, weakBasisAxis is defined as this map, and weakComplement_is_identity records that the simple axis labeling is the identity. The real mixing is deferred to internal structure: mass states as eigenstates of the $J$-cost operator weighted by flip counts, weak states as even-flip irreps. The definition sits in the Foundation chain that connects the eight-tick cube gauge action (T7) to generation space and the CKM change-of-basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.