torsionGap
plain-language theorem explainer
Integer torsion gap between two quark generations: Δτ(i,j) = τ_j − τ_i on Fin 3. CKM and η_B derivations cite it as the J-cost exponent that suppresses mass-basis off-diagonals and as the factor 11 in the chirality×torsion route to the rung −44. Pure abbreviation of the generation torsion difference; no proof content.
Claim. For generations $i,j \in \{0,1,2\}$, the torsion gap is the integer $\Delta\tau_{ij} := \tau_j - \tau_i$, where $\tau$ is the generation torsion assignment on the mass basis ($\tau \in \{0,11,17\}$).
background
The module builds the CKM matrix from Q₃ cube geometry, generation torsion, and Gray-code chirality. Mass eigenstates on Fin 3 are labeled by CW torsion levels: generation 1 at torsion 0 (ground), generation 2 at 11 (edge-dressed), generation 3 at 17 (edge+face-dressed). Off-diagonal mass-basis overlap is suppressed as $\varphi^{-|\Delta\tau_{ij}|}$, so the signed difference of those integers is the basic geometric input.
Weak eigenstates are organized by even-sign-flip SU(2) generators on the cube axes. Mixing angles combine a flip-count ratio with the same torsion gap. Downstream cosmology reuses the gap as a pure integer: bit-flip count on generation 0 times $|\Delta\tau_{01}|$ equals 4×11=44, matching the D=3 dimension-gap identity used for the η_B rung.
proof idea
One-line definition: subtract the generation torsion of i from that of j. No lemmas, tactics, or hypotheses. Sibling abbreviations (gap_12, gap_13, gap_23) specialize the same difference to fixed pairs; hierarchy and suppression lemmas then take absolute values and feed $\varphi$-exponents.
why it matters
This is the shared integer that links CKM mass-basis suppression to the baryon-asymmetry rung. Downstream, eta_B_rung_from_chirality is defined as $-(bitFlipCount(0)\cdot|torsionGap(0,1)|)=-(4\cdot 11)=-44$, and chirality_product_equals_gap_minus_one equates that product to the D=3 dimension gap minus the active-edge count. The EtaBExactRungCert packages agreement of three arithmetic routes to −44 (dimension, chirality×torsion, fermionic DOF); the rung assignment to η_B remains hypothesis-grade, but the integer content is structural.
In the CKM story the same gaps enter $\sin^2\theta_{ij}\propto (flip_count_ratio)\times\varphi^{-|\Delta\tau_{ij}|}$. Framework landmarks: T8 forces D=3, which makes both sides of the 44-identity hold; the eight-tick/Gray chirality supplies the flip counts. Parent consumers include the full EtaBExactRungDerivation suite and EtaBCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.