vub_smallest
plain-language theorem explainer
The torsion gaps satisfy |17| > |11| and |17| > |6|, so the generation-1–3 channel has the largest gap. That forces the smallest mass–weak overlap and hence the smallest CKM entry |V_ub|. Anyone deriving the CKM hierarchy from Q₃ torsion cites this numerical fact. The proof is a one-line norm_num check on integer absolute values.
Claim. As natural numbers, $|17| > |11|$ and $|17| > |6|$. In the mass–weak setting this means the torsion gap $\Delta\tau_{13} = 17$ is strictly larger than the gaps $11$ and $6$, so the $1$–$3$ mixing channel has the smallest overlap.
background
The module builds the two orthonormal bases on generation space whose overlap is the CKM matrix. Mass eigenstates come from the CW filtration on $Q_3$: passive-subcell couplings yield torsion values ${0, 11, 17}$ and thence $\varphi$-ladder rungs. Weak eigenstates come from the SU(2) gauge subgroup (even sign flips on the cube). The bases decompose $\mathbb{C}^8$ differently, so their axes mismatch and mixing is forced.
Physically, larger torsion gap means smaller mass–weak overlap. The $1$–$3$ channel carries $\Delta\tau_{13} = 17$, the largest listed gap; the companion integers $11$ and $6$ are the other torsion/flip-count scales that enter the hierarchy $|V_{ub}| \ll |V_{cb}| \ll |V_{us}|$. The present lemma records only the elementary size comparison among those three integers.
proof idea
Term-mode proof discharged by a single norm_num tactic. Lean reduces the two inequalities on Int.natAbs of the concrete literals $17$, $11$, and $6$ to true arithmetic facts; no lemmas from the torsion or gauge modules are invoked.
why it matters
Inside Recognition Science the CKM matrix is not fitted: it is the change-of-basis matrix between the CW/torsion mass axes and the even-flip weak axes on $Q_3$. The doc-comment states that $|V_{ub}|$ is smallest precisely because $\Delta\tau_{13} = 17$ is the largest torsion gap. This lemma supplies the raw numerical premise for that hierarchy (and for the companion claim that the full ordering follows from $17 > 6 > \cdots$ with flip-count modulation).
It sits in the Foundation layer that links particle generations, Gray-code chirality, and torsion forcing to the observed mixing pattern. No downstream theorems currently depend on it in the graph, so it functions as a named arithmetic anchor for the CKM-from-torsion narrative rather than as an intermediate step in a longer proof chain. Framework landmarks touched: the three-generation structure on the cube and the torsion set ${0,11,17}$ that feeds the $\varphi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.