ckmStructureCert
plain-language theorem explainer
A single certificate packaging the Q₃ cube facts that underwrite CKM structure: three generations, forced torsions {0,11,17} with gap hierarchy and additivity, Gray-code flip counts (4,2,2), and cycle chirality. Cite it when assembling the RS derivation of quark mixing from cube geometry rather than fitting angles by hand. The body is a structure instance: rfl and native_decide close the numeric fields; Gray-code lemmas supply flip counts and chirality.
Claim. A verified CKM structural certificate asserts: face-pair generation count equals $3$; generation torsions satisfy $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$; absolute torsion gaps obey $|\Delta\tau_{12}| < |\Delta\tau_{01}|$ and $|\Delta\tau_{01}|+|\Delta\tau_{12}|=|\Delta\tau_{02}|$; Gray-cycle bit-flip counts are $4,2,2$ with the first unequal to the second; and the Gray flip-count vector is chiral.
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 generation torsion (CW coupling level) $\tau\in{0,11,17}$: ground, edge-dressed, and edge+face-dressed. Off-diagonal mass overlap is J-cost suppressed as $\varphi^{-|\Delta\tau{ij}|}$. Weak eigenstates are the even-sign-flip SU(2) generators along the three cube axes. Mixing angles then scale as $\sin^2\theta{ij}\propto(\mathrm{flip_count_ratio})\times\varphi^{-|\Delta\tau_{ij}|}$.
The certificate type bundles the discrete geometric inputs: three generations from face-pair counting, the forced torsion triple, gap hierarchy and additivity of torsion differences, Gray-code bit-flip asymmetry $(4,2,2)$, and chirality of the canonical Gray cycle. Upstream, bit0_flips_four, bit1_flips_two, bit2_flips_two fix the flip counts by decision procedure, and cycle_is_chiral records that unequal axis flip counts make the eight-tick cycle chiral (the RS seed of CP violation). Three-generation counting is the standard $8=2^3$ face-pair identity.
proof idea
A structure instance, not a deep proof. Three-generation equality and the three torsion equalities are closed by rfl. Hierarchy, additivity of absolute torsion gaps, and flip asymmetry are closed by native_decide on concrete integers. Flip counts are the triple of upstream lemmas bit0_flips_four, bit1_flips_two, bit2_flips_two. Chirality is a one-line application of cycle_is_chiral (itself the unequal-count argument $4\neq 2$).
why it matters
This is the module's structural seal for CKM-from-cube: every discrete geometric hypothesis needed before writing mixing-angle formulas is collected in one place. It sits on the eight-tick octave (T7) and the $D=3$ cube that forces three generations from $2^3$, and it imports Gray-code chirality as the discrete origin of generation-asymmetric (CP-violating) treatment of axes. Downstream use sites are not yet wired in this graph; the certificate is the natural hypothesis package for any later theorem that builds $\sin^2\theta_{ij}$ or full $V_{\mathrm{CKM}}$ from torsion gaps and flip-count ratios. It does not itself evaluate numerical CKM entries or close the $\alpha$ band; it only freezes the cube inputs those calculations need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.