MassBasisAssignment
plain-language theorem explainer
Three-valued label assigning each fermion generation its preferred Q₃ axis coupling in the mass basis: gen 1 is the isotropic ground state, gen 2 locks to axis 0 (maximum flip count), gen 3 takes residual axes {1,2}. Anyone building CKM mixing from cube geometry cites this enum. Pure inductive definition with three constructors and no proof obligations.
Claim. The mass-basis assignment is a three-valued label on fermion generations determined by CW excitation ordering: generation 1 is the ground state (no excitation, coupled equally to all axes); generation 2 is the edge-dressed state, preferentially coupled to spatial axis $0$ (the axis with the most flips per cycle); generation 3 is the face-plus-edge state, coupled to the residual axes $\{1,2\}$.
background
The module constructs the two orthonormal bases on generation space whose overlap is the CKM matrix. Mass eigenstates come from the CW-level coupling structure (which passive subcells each generation couples to). Weak eigenstates come from the SU(2) gauge subgroup action (even sign flips on the cube). The CKM matrix is the change-of-basis between them.
In RS both bases live on the same $Q_3$ geometry but arise from different decompositions of $\mathbb{C}^8$: the CW filtration respects subcell dimension and yields torsion ${0,11,17}$ on the $\varphi$-ladder, while the gauge subgroup respects sign parity. The mismatch between those filtrations forces mixing.
This inductive records the mass-side axis assignment. Doc-comment rationale: gen 2 has torsion 11 equal to passive field edges, so it prefers the axis flipped most often (axis 0, four flips per cycle), minimizing J-cost; gen 3 inherits the leftover axes.
proof idea
No proof body. The declaration is an inductive type with three nullary constructors (gen1_ground, gen2_axis0, gen3_axes12) and automatic DecidableEq/Repr instances. The physical content sits entirely in the naming and the surrounding doc-comment; later defs such as the mass-axis map pattern-match on these constructors.
why it matters
This enum is the discrete skeleton of the mass eigenbasis on $Q_3$. Downstream siblings (massBasisAxis, both_bases_label_axes, MixingAngleData, axisMismatch) turn the three labels into concrete axis maps and compare them with the weak-basis assignment coming from even sign-flip irreps. The module thesis is that CW filtration and SU(2) parity decompose $\mathbb{C}^8$ differently, so the two bases cannot coincide and CKM mixing is forced rather than fitted.
In the broader RS chain the assignment sits between the eight-tick octave (T7) / $D=3$ (T8) geometry and the $\varphi$-ladder mass formula: torsion values ${0,11,17}$ fix rung positions once the preferred axes are chosen. No used-by edges are recorded yet; the type is infrastructure for the mixing-angle data structure that follows in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.