torsion_diff_21
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the torsion values from cube geometry.
- Does not compute explicit particle masses or ratios.
- Does not address sector base rungs or third-generation offsets.
- Does not extend to non-fermion sectors.
formal statement (Lean)
76@[simp] lemma torsion_diff_21 : torsionDiff .second .first = 11 := by
proof body
One-line wrapper that applies simp.
77 simp [torsionDiff]
78