suppression_13
plain-language theorem explainer
The mass-basis CKM suppression exponent between generations 1 and 3 equals −17. Anyone assembling quark mixing angles from Q₃ torsion gaps cites this closed evaluation. The proof is a one-line native decision of the integer exponent definition on Fin 3.
Claim. The suppression exponent between generation indices $0$ and $2$ equals $-17$. Equivalently, the $\varphi$-power that multiplies the mass-basis overlap amplitude between the torsion-$0$ ground state and the torsion-$17$ (edge+face-dressed) state is $\varphi^{-17}$.
background
This module builds the CKM matrix as the overlap $V_{ij}=\langle\mathrm{weak}_i\mid\mathrm{mass}_j\rangle$ on the three-generation space, with both bases fixed by Q₃ cube geometry. Mass eigenstates are labeled by generation torsion ${0,11,17}$: ground state (no passive coupling), edge-dressed (11 passive edges), and edge+face-dressed (11 edges + 6 faces).
Off-diagonal mass-basis amplitudes are J-cost suppressed by the torsion gap: $\langle\mathrm{mass}_i\mid\mathrm{mass}j\rangle\propto\varphi^{-|\Delta\tau{ij}|}$. The named exponent map records that signed power for each pair of generation indices. For indices $0$ and $2$ one has $|\tau_2-\tau_0|=|17-0|=17$, so the exponent is $-17$.
Weak eigenstates come from the SU(2) even-sign-flip generators on the cube axes; flip-count weights $[4,2,2]$ later modulate the same amplitudes. The present fact isolates only the pure torsion-gap exponent between the outer generations.
proof idea
One-line computational proof: native_decide evaluates the closed integer definition of the suppression exponent at the concrete Fin-3 pair $(0,2)$ and checks equality with $-17$. No algebraic lemmas are invoked; the result is pure definitional arithmetic on the fixed torsion table ${0,11,17}$.
why it matters
In the CKM-from-cube derivation, mixing angles satisfy $\sin^2\theta_{ij}\propto(\mathrm{flip_count_ratio})\times\varphi^{-|\Delta\tau_{ij}|}$. Pinning the $(1,3)$ exponent at $-17$ fixes the strongest mass-basis suppression channel (ground state versus fully dressed third generation) and matches the generation-torsion landmark ${0,11,17}$ from the torsion-forcing layer.
Sibling facts cover the other pairs (suppression_12, suppression_23) and the underlying gaps; together they supply the full $\varphi$-ladder skeleton for $V_{ij}$ before flip-weight modulation. No downstream consumers are wired yet in the graph, so this is a leaf evaluation waiting on the assembled CKM amplitude theorems. It sits downstream of the mass/weak basis construction and the Gray-code chirality schedule, and upstream of any numerical CKM angle comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.