MixingAngleData
plain-language theorem explainer
Packages the discrete geometric inputs that fix CKM mixing on the 3-cube: per-axis bit-flip counts (4,2,2), generation torsions (0,11,17), and cube face/edge counts (6,12). Anyone deriving CKM angles from mass vs weak bases on Q₃ cites this bundle. It is a pure data structure with value equalities and the total-flip sum 8; no proof beyond field constraints.
Claim. A record of structural mixing ingredients on $Q_3$: maps $c,\tau:\{0,1,2\}\to\mathbb{N},\mathbb{Z}$ with $c(0)=4$, $c(1)=c(2)=2$, $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$; integers $F=6$ (faces) and $E=12$ (edges); and the identity $c(0)+c(1)+c(2)=8$. All entries are fixed RS primitives (no free parameters).
background
The module builds two orthonormal bases on 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) even sign-flip action on the cube (GaugeFromCube Layer 2). The mismatch of those decompositions of $\mathbb{C}^8$ forces mixing.
Flip counts record how many vertices each coordinate bit flips under the relevant generators; their sum is the eight-tick register size. Face and edge counts are the standard $D=3$ cube incidences ($F=2D=6$, $E=12$), matching the upstream face-count definition $F=2D$. Torsion values are the generation offsets already forced in the mass sector.
This structure only holds those discrete numbers together so downstream code can compute axis overlaps without re-deriving each constant.
proof idea
No proof body: it is a structure declaration. Each field is either a map/value or a Prop equality constraining that value. Instantiation (see mixingData) supplies concrete functions and closes the equalities by named lemmas such as bit-flip counts and the fixed torsions; the structure itself only packages the interface.
why it matters
Feeds the concrete instance mixingData, documented as "the mixing data for $Q_3$, fully computed from RS primitives." That instance is the bridge from axis mismatch to numerical CKM angles: flip counts weight the weak-basis overlaps, torsions place mass eigenstates on the $\varphi$-ladder, and face/edge counts normalize cube combinatorics.
In the forcing chain this sits after $D=3$ (T8) and the eight-tick octave (T7): total flips sum to 8, faces are $2\cdot 3$. Zero free parameters is the RS claim that CKM ingredients are not fitted Yukawas but cube geometry plus CW torsion. Parent consumers of mixingData use this bundle rather than ad-hoc constants when assembling the change-of-basis matrix between mass and weak axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.