torsionDiff
plain-language theorem explainer
TorsionDiff subtracts the canonical torsion offsets of two fermion generations to produce their integer rung difference on the phi-ladder. Mass-ratio derivations in the RSLedger module cite this definition when establishing the scalings phi^11, phi^17, and phi^6. The definition reduces directly to subtraction of the generationTorsion values.
Claim. For generations $g_1$ and $g_2$, the torsion difference equals $τ(g_1) - τ(g_2)$, where $τ$ maps the first generation to 0, the second to 11, and the third to 17.
background
The RSLedger module supplies the rich ledger structure that derives fermion masses from discrete rungs on the phi-ladder rather than from ad-hoc formulas. Each generation carries a torsion offset $τ_g$ obtained from D=3 cube combinatorics, and the full rung for a sector is baseRung plus $τ_g$. Mass ratios then follow as $m_f / m_g = φ^{r_f - r_g}$ once the rung difference is known.
proof idea
This is a one-line definition that subtracts the outputs of generationTorsion applied to each input generation.
why it matters
TorsionDiff supplies the rung difference consumed by the canonical mass-ratio theorems massRatio_21_canonical, massRatio_31_canonical, and massRatio_32_canonical, which recover the phi-power scalings phi^11, phi^17, and phi^6. It closes the geometric step that links Q3 cube combinatorics to the Recognition Science mass formula on the phi-ladder. The parent RSLedger structure depends on it for complete rung assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.