both_bases_label_axes
plain-language theorem explainer
Mass and weak preferred-axis labels on the three-generation space coincide: both maps Fin 3 → Fin 3 are the identity. Anyone separating Q₃ axis bookkeeping from CKM eigenstructure cites this. The proof is exhaustive case split on three indices, each closed by reflexivity.
Claim. For every generation index $i\in\{0,1,2\}$, the preferred spatial axis of the mass basis equals that of the weak basis. Explicitly both assignments send $0\mapsto 0$, $1\mapsto 1$, $2\mapsto 2$.
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 data ${0,11,17}$ on the $\varphi$-ladder, with flip-count weights $[4,2,2]$ from Gray-code chirality. Weak eigenstates come from the SU(2) subgroup action realized as even sign-flip generators on the cube $Q_3$.
For overlap bookkeeping one first assigns each generation a preferred spatial axis in $\mathrm{Fin},3$. The mass-axis map is the identity (Gen 1 on axis 0, Gen 2 on axis 1, Gen 3 on axis 2). The weak-axis map is defined as the complement of the even-flip generator; that complement is itself the identity, so the two label maps agree pointwise.
The module doc stresses that the physical mismatch is not this axis labeling. Mass states diagonalize a $J$-cost operator weighted by flip counts; weak states diagonalize even-sign-flip irreps. Those internal decompositions of $\mathbb{C}^8$ differ even when the axis tags coincide.
proof idea
Introduce the generation index $i:\mathrm{Fin},3$. Split into the three concrete cases $i=0,1,2$ via fin_cases. In each case both massBasisAxis and weakBasisAxis reduce by definition to the same numeral in $\mathrm{Fin},3$, so rfl closes. No external lemmas are required beyond the two axis definitions (and the fact that the weak complement is the identity).
why it matters
This is the bookkeeping lemma that prevents a false reading of the CKM story: axis tags alone do not force mixing. The doc-comment is explicit that mixing lives in the internal eigenstructure (flip-count-weighted $J$-cost eigenstates versus even-sign-flip eigenstates), with precise matrix elements deferred to overlap integrals in CKMFromCube.
It sits just before the MixingAngleData section, which packages the RS-derived ingredients (flip counts $[4,2,2]$, torsion ${0,11,17}$, face/edge counts of $Q_3$, recognition angle $\theta_0=\arccos(1/4)$). Those data, not the axis labels, determine the generation coupling strengths. In the broader forcing chain this is foundation-level geometry on the eight-tick cube, not a T5–T8 uniqueness step, but it keeps the mass/weak mismatch honest before any numerical CKM claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.