WeakBasisAssignment
plain-language theorem explainer
Labels the three quark generations by the even SU(2) sign-flip generators on the cube: gen1 with σ₂₃, gen2 with σ₁₃, gen3 with σ₁₂. Each constructor records the complement axis (the axis not flipped). Anyone building the weak eigenbasis or CKM overlap on Q₃ cites this enumeration. It is a plain three-constructor inductive with decidable equality.
Claim. An enumeration of weak-basis generation labels on $Q_3$: generation 1 paired with the even flip $\sigma_{23}$ (complement axis $0$), generation 2 with $\sigma_{13}$ (complement axis $1$), and generation 3 with $\sigma_{12}$ (complement axis $2$). Equality of labels is decidable.
background
The module fixes two orthonormal bases on the three-generation space whose overlap is the CKM matrix. Mass eigenstates come from the CW filtration and torsion rungs ${0,11,17}$ on the $\varphi$-ladder. Weak eigenstates come from the SU(2) gauge subgroup realized as even sign flips on the cube (GaugeFromCube Layer 2).
Even sign-flip generators act on pairs of spatial axes. The Weyl-group pairing used here is: gen 1 (down-type) with $\sigma_{23}$ (flips axes 1 and 2), gen 2 (charm-type) with $\sigma_{13}$ (flips 0 and 2), gen 3 (top-type) with $\sigma_{12}$ (flips 0 and 1). The axis left unflipped is the complement axis and serves as the weak-basis label.
The mismatch with the mass-basis axis assignment is what forces nontrivial mixing angles; both decompositions act on $\mathbb{C}^8$ but respect different filtrations (subcell dimension versus sign parity).
proof idea
No proof body: a three-constructor inductive definition. Constructors are the generation–generator pairs above, with comments recording complement axes $0,1,2$. Derives DecidableEq and Repr so labels can be compared and printed in later axis maps.
why it matters
Gives the discrete type for the weak eigenbasis on $Q_3$, dual to the mass-basis assignment. Downstream siblings map each label to its complement axis and compare the two bases; their mismatch is the geometric source of CKM mixing in Recognition Science.
Fits the foundation story that both mass and weak structure are forced by the same eight-tick cube geometry (T7 octave, $D=3$), while the CW filtration and the even-flip SU(2) action decompose the register differently. Without this enumeration there is no typed weak axis map and no structured mixing-angle data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.