torsion_diff_32
plain-language theorem explainer
The lemma states that the torsion difference between the third and second generations equals 6. Researchers computing inter-generation mass ratios on the φ-ladder in Recognition Science would cite this when evaluating the exponent for third-over-second generation particles. The proof is a one-line simplification that unfolds the definition of torsionDiff.
Claim. Let τ(g) denote the torsion offset of generation g. Then τ(third) − τ(second) = 6.
background
The RSLedger module places fermion masses on discrete rungs of the φ-ladder. Each generation carries a torsion offset τ_g obtained from D=3 cube combinatorics: τ₁ = 0 for the ground generation, τ₂ = 11 for the edge-dressed generation, and τ₃ = 17 for the face-plus-edge generation. The function torsionDiff(g1, g2) is defined as generationTorsion g1 minus generationTorsion g2, so that mass ratios satisfy m_f / m_g = φ raised to the rung difference.
proof idea
The proof is a one-line wrapper that applies the definition of torsionDiff and substitutes the concrete torsion values for the third and second generations.
why it matters
This lemma supplies the numerical exponent 6 required for the Gen 3 / Gen 2 mass ratio φ^6 listed in the module documentation. It directly links the cube-derived torsion set {0, 11, 17} to the inter-generation scaling that appears in the Recognition Science mass formula. The result supports the φ-ladder structure without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.