CKMStructureCert
plain-language theorem explainer
A structure packing the cube-geometry facts that underwrite CKM mixing: three generations from face pairs, forced torsions {0,11,17} with hierarchy and additivity of gaps, and Gray-code flip counts [4,2,2] that are chiral. Anyone deriving quark mixing angles from Q₃ cites this bundle. It is a pure interface definition; the verified inhabitant is the separate certificate value.
Claim. A CKM structure certificate is a record asserting: (i) the number of opposite-face pairs on the 3-cube equals 3; (ii) generation torsions satisfy $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$; (iii) absolute torsion gaps obey $|\Delta\tau_{12}| < |\Delta\tau_{01}|$ and $|\Delta\tau_{01}|+|\Delta\tau_{12}|=|\Delta\tau_{02}|$; (iv) Gray-code bit-flip counts are $4,2,2$ on the three axes (hence asymmetric on axes 0 and 1); (v) those flip counts form a chiral cycle (not invariant under all axis permutations).
background
The module derives the CKM matrix as the overlap $V_{ij}=\langle\mathrm{weak}_i|\mathrm{mass}j\rangle$ on the three-generation space, with both bases fixed by $Q_3$ geometry. Mass eigenstates are labeled by torsion (CW coupling level): ground state $\tau=0$, edge-dressed $\tau=11$, edge+face-dressed $\tau=17$. Off-diagonal mass overlaps are suppressed by $\varphi^{-|\Delta\tau{ij}|}$. Weak eigenstates are the even-sign-flip $SU(2)$ generators complementary to each cube axis.
torsionGap i j is the integer difference $\tau_j-\tau_i$. bitFlipCount counts how often each of the three bits flips along the 8-tick Gray cycle; grayFlipCounts is that function, and IsChiral means the three counts are not all equal (equivalently, not permutation-invariant). face_pairs D is simply $D$, so three opposite-face pairs on the spatial cube, matching the three-generation count from the $8=2^3$ tick-space argument.
proof idea
No proof body: this is a structure (record type) whose fields are the Prop obligations. Downstream, ckmStructureCert inhabits it by rfl on the generation and torsion equalities and native_decide on the gap inequalities, gap additivity, flip asymmetry, flip counts, and chirality. The mathematical content is therefore the conjunction of those seven atomic claims, not a derived implication.
why it matters
This is the single packaging point for every cube-side hypothesis the CKM derivation needs before writing mixing angles. The module sets $\sin^2\theta_{ij}\propto(\mathrm{flip_count_ratio})\times\varphi^{-|\Delta\tau_{ij}|}$; the certificate locks the numerical inputs to that formula (torsions, gaps, flip weights) and the structural facts (three generations, chirality of the Gray cycle). Downstream ckmStructureCert is the verified instance. Framework landmarks in play: T7 eight-tick octave (Gray cycle on $Q_3$), T8 $D=3$ (three face-pair generations), and the $\varphi$-ladder suppression of torsion gaps. It does not itself close numerical CKM entries; it freezes the geometry those entries rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.