gap_12
plain-language theorem explainer
The torsion gap between the first and second quark generations equals 11. Anyone deriving CKM mixing angles from Q₃ mass-basis torsion cites this exact integer difference. The proof is a one-line native decision on the definition τ₂ − τ₁ with the fixed values {0, 11, 17}.
Claim. The generation torsion gap between indices $0$ and $1$ equals $11$: $\tau(1) - \tau(0) = 11$, where the mass-basis torsions are $\tau \in \{0, 11, 17\}$ on $\mathrm{Fin}\,3$.
background
In the CKM-from-cube module, mass eigenstates on the three-generation space are labeled by CW torsion levels: generation 1 has torsion 0 (ground state), generation 2 has torsion 11 (edge-dressed), and generation 3 has torsion 17 (edge plus face). Off-diagonal mass-basis overlaps are suppressed by $\varphi^{-|\Delta\tau|}$, so the integer gaps control the mixing hierarchy.
The local definition torsionGap i j is simply $\tau j - \tau i$ as an integer. The present statement records the first adjacent gap. Upstream, the torsion triple itself is fixed by the Q₃ geometry and the Recognition torsion-forcing chain; the module then feeds these gaps into suppression exponents and flip-weight factors that build $\sin^2\theta_{ij}$.
proof idea
One-line computational discharge: native_decide evaluates torsionGap 0 1, which expands to $\tau,1 - \tau,0$, against the concrete assignment of generation torsions, and checks equality with 11. No lemmas beyond the definition are required.
why it matters
This pins the Cabibbo-sector torsion difference that enters the mass-basis overlap $\langle\mathrm{mass}1|\mathrm{mass}2\rangle \propto \varphi^{-11}$. Together with the sibling gaps (13 and 23 channels) and the Gray-code flip weights, it supplies the integer skeleton for the CKM angles under the module's rule $\sin^2\theta{ij} \propto (\mathrm{flip_count_ratio})\times\varphi^{-|\Delta\tau{ij}|}$.
In the broader Recognition chain the torsion values {0, 11, 17} sit on the $\varphi$-ladder mass formula and the eight-tick / cube geometry (T7–T8 landmarks). No downstream theorems currently depend on this name alone, but the hierarchy lemmas and suppression exponents in the same file consume the same gap data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.