leptonRung
plain-language theorem explainer
leptonRung computes the integer rung for a charged lepton by adding a generation-dependent torsion offset to the reduced length ℓ. Researchers assigning masses on the phi-ladder in Recognition Science would cite this when locating electrons, muons, and taus. The definition proceeds by a direct case match on the generation class to select the offset 0, 11, or 17 before adding it to ℓ.
Claim. $r = ℓ + τ_g$ where $τ_g = 0$ for generation 1, $τ_g = 11$ for generation 2, and $τ_g = 17$ for generation 3, with $ℓ$ the reduced ribbon length.
background
The module supplies placeholder ribbon machinery for mass assignments in Recognition Science and is classified as a Model. GenClass is the inductive type with constructors g1, g2, g3 that labels the three fermion generations. leptonRung supplies the rung values placed on the phi-ladder for charged leptons, using base length 2 together with the listed torsions to produce the sequence 2, 13, 19.
proof idea
The definition matches on the generation class to bind the torsion offset and returns the sum with the input length parameter.
why it matters
It is invoked by lepton_rungs_correct to verify the rungs 2, 13, 19 and by rungFrom to extract rungs from words. Within the Recognition framework the definition populates the lepton sector of the mass formula on the phi-ladder, consistent with the eight-tick octave and spatial dimension 3, although the module remains a narrative scaffold pending full formalization of the derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.