suppressionExponent
plain-language theorem explainer
Defines the integer φ-suppression exponent between two quark generations as the negative absolute torsion gap. Anyone deriving CKM off-diagonal amplitudes from Q₃ torsion cites this. The body is a one-line arithmetic wrapper around the signed torsion difference.
Claim. For generation indices $i,j \in \{0,1,2\}$, the suppression exponent is $-(|\tau_j - \tau_i|)$, an integer power of $\varphi$ in the mass-basis overlap $\propto \varphi^{-|\Delta\tau_{ij}|}$.
background
The module builds the CKM matrix from Q₃ cube geometry: generation torsion ${0,11,17}$ for the mass basis and Gray-code chirality $[4,2,2]$ for the weak basis. Mass eigenstates are labeled by CW coupling level (torsion): ground state $\tau=0$, edge-dressed $\tau=11$, edge+face-dressed $\tau=17$.
Off-diagonal mass-basis overlap is J-cost suppressed by the absolute torsion gap. Upstream, torsionGap is the signed difference $\tau_j - \tau_i$. The present definition converts that gap into the non-positive integer exponent that multiplies $\log\varphi$ in the amplitude.
In RS units the golden ratio $\varphi$ is the self-similar fixed point (forcing chain T6); powers of $\varphi$ set mass-ladder and mixing suppressions throughout the Standard Model sector.
proof idea
Pure definition, not a proof. It takes the absolute value of the signed torsion gap and negates it, so the exponent is always $\le 0$. Downstream equalities (suppression_12, suppression_23, suppression_13) discharge the concrete values $-11$, $-6$, $-17$ by native_decide on the fixed torsion table.
why it matters
This is the φ-power that enters every off-diagonal CKM structural amplitude. Downstream, unnormalizedAmplSq sets diagonal entries to 1 and off-diagonal entries to $\varphi^{2\cdot\mathrm{exponent}}$, i.e. $\varphi^{-2|\Delta\tau|}$. The three named theorems pin the hierarchy 1–2 : $\varphi^{-11}$, 2–3 : $\varphi^{-6}$, 1–3 : $\varphi^{-17}$, matching the module's stated torsion differences $|11-0|$, $|17-11|$, $|17-0|$.
Together with flip-count weights from Gray-code chirality, the exponent supplies the $\varphi^{-|\Delta\tau|}$ factor in $\sin^2\theta_{ij} \propto (\mathrm{flip_ratio})\times\varphi^{-|\Delta\tau_{ij}|}$. It is the bridge from the mass-torsion ladder (and the broader φ-ladder mass formula) into CKM mixing angles and Wolfenstein parameters later in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.