mixingData
plain-language theorem explainer
Packages the RS-derived ingredients that fix qualitative CKM mixing on the 3-cube: Gray-code bit flip counts (4,2,2), CW torsion rungs (0,11,17), and the cube face/edge counts (6,12). Anyone deriving Cabibbo-scale hierarchy from Q₃ geometry cites this bundle. The body is a structure instance: flip counts from Gray-code lemmas, torsion and topology by reflexivity, total flips by native decision.
Claim. The mixing-angle data on $Q_3$ is the record with flip counts $f(0)=4$, $f(1)=2$, $f(2)=2$ (Gray-code bit flips over the eight-tick cycle), torsion rungs $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$, face count $6$, edge count $12$, and $f(0)+f(1)+f(2)=8$. All entries are fixed by Recognition Science primitives with no free parameters.
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 rungs on the $\varphi$-ladder; weak eigenstates come from the even sign-flip action of the SU(2) subgroup of the cube gauge group. The mismatch of those decompositions of $\mathbb{C}^8$ forces mixing.
MixingAngleData is the parameter-free bundle of geometric inputs that control that mismatch: per-axis flip counts along the eight-tick Gray cycle, the torsion triple ${0,11,17}$, and the cube's face and edge counts. Flip counts are defined by counting which coordinate bit flips at each tick of the cycle; the lemmas bit0_flips_four, bit1_flips_two, and bit2_flips_two pin the values $4,2,2$.
Torsion values are the CW-level rungs that place the three generations on the $\varphi$-ladder (mass formula yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Face and edge counts $6$ and $12$ are the ordinary $Q_3$ incidence numbers used later for overlap normalizations.
proof idea
Definitional structure instance, not a proof. Flip-count field is the Gray-code function bitFlipCount. The three equalities $f(0)=4$, $f(1)=2$, $f(2)=2$ are supplied by the native-decide theorems bit0_flips_four, bit1_flips_two, bit2_flips_two. Torsion is the piecewise map $0\mapsto 0$, $1\mapsto 11$, $2\mapsto 17$, with values discharged by rfl. Face and edge counts are the literals $6$ and $12$, again by rfl. The sum identity $4+2+2=8$ is closed by native_decide.
why it matters
This is the concrete RS packing of the structural data that later qualitative mixing claims read off: the Cabibbo (1-2) angle is largest because the flip-count gap $|4-2|=2$ matches the 0-2 gap while the torsion gap $\Delta\tau_{12}=11$ is smaller than $\Delta\tau_{13}=17$, so overlap is larger. It sits in the Foundation layer that derives mass and weak bases from the same $Q_3$ geometry (eight-tick octave, $D=3$ cube, Gray chirality, torsion forcing), rather than from free Yukawa matrices.
No downstream theorems yet consume the bundle (used-by is empty); the immediate consumers are the qualitative mixing predictions in the same module and the planned Phase-2 exact CKM elements. It closes the "zero free parameters" interface promised by MixingAngleData and ties the CKM hierarchy to T7 (eight-tick) and the CW torsion ladder rather than to fitted angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.