torsion_diff_21
plain-language theorem explainer
The lemma fixes the torsion offset between second and first generations at exactly 11. Mass-ratio derivations on the φ-ladder cite it to obtain m₂/m₁ = φ¹¹. The proof is a one-line simp wrapper that unfolds the difference definition.
Claim. The torsion difference satisfies τ₂ − τ₁ = 11, where τ_g denotes the generation torsion offset derived from D=3 cube geometry.
background
The RSLedger module equips the Recognition ledger with φ-tier structure so that fermion masses sit on discrete rungs of the φ-ladder. Each generation carries a torsion offset τ_g obtained from Q₃ cube combinatorics: τ₁ = 0, τ₂ = E_passive(D) = 11, τ₃ = 17. The upstream definition torsionDiff(g1,g2) := generationTorsion g1 − generationTorsion g2 supplies the integer difference used throughout the ledger.
proof idea
The proof is a one-line simp wrapper that applies the definition of torsionDiff, reducing the expression directly to the concrete values 11 − 0.
why it matters
This supplies the numerical offset required for the inter-generation mass ratio φ¹¹ between second and first generation fermions, as recorded in the module documentation. It translates the D=3 cube result E_passive(D)=11 into the ledger, supporting the rung formula rung = baseRung + τ_g and the overall φ-ladder mass construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.