suppression_23
plain-language theorem explainer
The φ-suppression exponent between the second and third quark generations equals −6, so their mass-basis overlap scales as φ^{−6}. Anyone assembling CKM mixing angles from Q₃ torsion gaps cites this evaluation. The proof is a one-line native_decide check of the absolute torsion gap.
Claim. For zero-based generation indices $1$ and $2$ (the second and third generations), the $\varphi$-suppression exponent equals $-6$. Equivalently, if $\Delta\tau$ is the torsion gap between those generations, then $-|\Delta\tau|=-6$, so the off-diagonal mass overlap amplitude scales as $\varphi^{-6}$.
background
This module builds the CKM matrix from Q₃ cube geometry, generation torsion ${0,11,17}$, and Gray-code chirality. Mass eigenstates sit at those torsion levels: ground state $\tau=0$, edge-dressed $\tau=11$, and edge+face-dressed $\tau=17$. Off-diagonal mass overlaps are J-cost suppressed as $\varphi^{-|\Delta\tau|}$.
The suppression exponent for a generation pair is defined as the negative absolute torsion gap: it is $-(|\tau_i-\tau_j|)$. Sibling facts record the three pair values: $1$–$2$ gives $\varphi^{-11}$, $2$–$3$ gives $\varphi^{-6}$, and $1$–$3$ gives $\varphi^{-17}$. Weak eigenstates are the even-sign-flip SU(2) generators on the cube; mixing angles combine flip-count ratios with these $\varphi$ powers.
proof idea
One-line computational proof. Unfold the definition of the suppression exponent as the negation of the absolute torsion gap on Fin-3 indices $1$ and $2$, then discharge the resulting integer equality by native_decide. No intermediate lemmas are required beyond that definition.
why it matters
Fills the $2$–$3$ entry in the three-pair suppression table that drives CKM angles in the cube derivation. With torsion levels $11$ and $17$, the gap is $6$, matching the module claim that the $2$–$3$ mass overlap scales as $\varphi^{-6}$. Together with the $1$–$2$ and $1$–$3$ companions, it supplies the $\varphi^{-|\Delta\tau|}$ factors in $\sin^2\theta_{ij}\propto(\mathrm{flip_count_ratio})\times\varphi^{-|\Delta\tau_{ij}|}$. No downstream theorems currently depend on it in the graph; it is a leaf evaluation inside the CKM-from-cube scaffold. The torsion triple itself is forced upstream by the mass/weak basis and torsion-forcing imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.