gap_23
plain-language theorem explainer
The torsion gap between the second and third quark generations equals 6. Anyone deriving CKM mixing from Q₃ cube geometry cites this as Δτ₂₃, the integer that sets the |V_cb| mass-basis suppression scale φ^{-6}. The proof is a one-line native decision on the fixed generation torsions 17 and 11.
Claim. With generation torsions $\tau=(0,11,17)$ on $\mathrm{Fin}\,3$, the torsion gap between generations 2 and 3 is $\Delta\tau_{23}:=\tau_3-\tau_2=6$.
background
In the CKM-from-cube module, mass eigenstates on the three-generation space are labeled by generation torsion (CW coupling level): $\tau_1=0$ (ground), $\tau_2=11$ (edge-dressed), $\tau_3=17$ (edge+face-dressed). The torsion gap is the integer difference $\Delta\tau_{ij}=\tau_j-\tau_i$. Off-diagonal mass-basis overlap is suppressed by the J-cost factor $\varphi^{-|\Delta\tau_{ij}|}$.
Weak eigenstates come from the SU(2) even-sign-flip generators on the Q₃ cube (Gray-code chirality $[4,2,2]$). CKM entries $V_{ij}$ are overlaps between weak state $i$ and mass state $j$, with mixing angles of the schematic form $\sin^2\theta_{ij}\propto(\mathrm{flip\ count\ ratio})\times\varphi^{-|\Delta\tau_{ij}|}$.
The three concrete gaps $\Delta\tau_{12}=11$, $\Delta\tau_{23}=6$, $\Delta\tau_{13}=17$ are the discrete inputs that later force the observed CKM magnitude hierarchy.
proof idea
One-line computational proof. Unfold torsionGap 1 2 to $\tau_2-\tau_1$ with the fixed table $\tau=(0,11,17)$, so the goal is $17-11=6$, discharged by native_decide.
why it matters
This is the smallest torsion gap and therefore the weakest mass-basis suppression among the three generation pairs. The sibling hierarchy result records $\Delta\tau_{23}<\Delta\tau_{12}<\Delta\tau_{13}$, which the module doc states forces the CKM magnitude ordering $|V_{cb}|>|V_{ub}|$ and $|V_{us}|>|V_{ub}|$ once flip-count weights are included.
In the broader Recognition chain the integer 6 is not free: it is the difference of the forced generation torsions ${0,11,17}$ coming from Q₃ edge/face dressing (eleven passive edges, six faces). That geometry sits on the eight-tick octave and $D=3$ cube already fixed by T7–T8. No downstream theorem yet consumes this lemma directly; it is scaffolding for the explicit Wolfenstein-scale comparisons in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.