weakBasisAxis
plain-language theorem explainer
The weak-basis axis assignment sends each of the three generation indices to a spatial axis in {0,1,2}, namely the axis left unflipped by that generation's even sign-flip generator. Explicitly the map is the identity. CKM-from-cube and mass/weak mismatch arguments cite it as the weak-side axis label. The body is a one-line alias of the weak complement axis.
Claim. The weak-basis axis assignment is the map $w:\{0,1,2\}\to\{0,1,2\}$ that sends each generation index to the spatial axis not flipped by the corresponding even sign-flip generator $\sigma_{jk}$. Explicitly $w(0)=0$, $w(1)=1$, $w(2)=2$ (the identity), identical to the weak complement-axis map.
background
This module builds the two orthonormal bases on the three-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) gauge subgroup realized as even sign flips on the cube $Q_3$ (GaugeFromCube Layer 2).
The weak complement axis for generation $i$ is the coordinate axis that the matching even flip generator does not flip: $\sigma_{23}$ leaves axis 0, $\sigma_{13}$ leaves axis 1, $\sigma_{12}$ leaves axis 2. That assignment is therefore the identity on $\mathrm{Fin},3$. The present definition simply names that map as the weak-basis axis label.
Axis labels alone do not produce mixing. The module doc stresses that mass states are eigenstates of a J-cost operator weighted by flip counts $[4,2,2]$, while weak states are eigenstates of the even-sign-flip generators; those internal structures differ even when the axis labels coincide.
proof idea
One-line definitional alias: the weak-basis axis map is defined to be exactly the weak complement-axis map already constructed by case analysis on $\mathrm{Fin},3$. No tactics or lemmas are invoked; equality of the two names is definitional.
why it matters
Feeds the theorem that both mass and weak axis assignments are the identity under this simple labeling. That result isolates the true source of CKM mixing: not a mismatch of axis labels, but the different internal eigenstructures (J-cost flip-count weights versus even-sign-flip irreps). Downstream, precise CKM entries are overlap integrals between those eigenstates (CKMFromCube).
In the RS picture this sits on the $Q_3$ / eight-tick register that also forces $D=3$ (T8) and the gauge content from the cube. The mass side still ties to the $\varphi$-ladder and torsion forcing; the weak side ties to the even-flip SU(2) action. Naming the weak axis map keeps the two bases comparable before the overlap is computed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.