def
definition
def or abbrev
genOfTorsion
show as:
view Lean formalization →
formal statement (Lean)
98@[simp] noncomputable def genOfTorsion (t : Torsion8) : Derivation.GenClass :=
proof body
Definition body.
99 match (t.val % 3) with
100 | 0 => Derivation.GenClass.g1
101 | 1 => Derivation.GenClass.g2
102 | _ => Derivation.GenClass.g3
103
104/-- **LEPTON RUNG DERIVATION**
105 The charged lepton rungs {2, 13, 19} are derived from the reduced length ℓ
106 and the generation torsion τ_g.
107
108 ℓ = 2 (minimal neutral loop)
109 τ_g ∈ {0, 11, 17} for generations {1, 2, 3}
110
111 r = ℓ + τ_g
112 Generation 1 (e): 2 + 0 = 2
113 Generation 2 (mu): 2 + 11 = 13
114 Generation 3 (tau): 2 + 17 = 19 -/