canonicalRSLedger_torsion
plain-language theorem explainer
The torsion field of the canonical RS ledger equals the generation torsion map from cube geometry. Mass-ratio derivations in the phi-ladder cite this equality to insert the fixed offsets 0, 11, 17 directly into rung calculations. The proof is a one-line reflexivity that follows from the ledger definition.
Claim. The torsion component of the canonical ledger equals the generation torsion assignment: $τ_{can} = τ_g$, where $τ_g$ sends the first generation to 0, the second to passive-field-edges(3), and the third to passive-field-edges(3) + cube-faces(3).
background
The RSLedger module supplies the rich ledger structure that derives fermion mass ratios from generation torsion offsets on the phi-ladder rather than from explicit phi-formulas. Each generation carries a torsion offset $τ_g$ obtained from three-dimensional cube combinatorics: ground state (gen 1) has $τ=0$, passive-edge mode (gen 2) has $τ=11$, and passive-edge-plus-face mode (gen 3) has $τ=17$.
proof idea
The proof is a one-line term-mode reflexivity that equates the torsion field of canonicalRSLedger to generationTorsion by direct appeal to the ledger constructor.
why it matters
This equality supplies the torsion values required by canonical_massRatiosFromTiers, canonical_massRatio_21, canonical_massRatio_31, and canonical_massRatio_32. It closes the link between D=3 cube geometry and the phi-ladder mass formula, confirming the inter-generation ratios $φ^{11}$, $φ^{17}$, $φ^6$ without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.