rungFrom
plain-language theorem explainer
The definition assembles an integer rung index for phi-ladder mass placement by adding a generation torsion to the reduced length of a ribbon word. Mass-spectrum builders in Recognition Science cite it when feeding words into canonical mass formulas. It is realized as a direct composition of the reduced-length extractor with the lepton-rung adder.
Claim. For generation class $g$ and ribbon word $w$, the rung index equals the reduced length of the normal form of $w$ plus a torsion offset that is 0 for $g=1$, 11 for $g=2$, and 17 for $g=3$.
background
A Word is a list of ribbon syllables, each carrying a gauge tag and a direction on the eight-tick clock. The ell function returns the length of the word after normalization to minimal form by cancelling opposing pairs. leptonRung then adds a generation torsion drawn from the inductive GenClass type whose three constructors label the first, second and third generations.
proof idea
The definition is a one-line wrapper that applies leptonRung to the reduced length ell of the input word and the supplied generation class.
why it matters
rungFrom supplies the integer rung consumed by massCanonFromWord when it calls Derivation.massCanonPure and by deltaOf when it extracts rung differences for sector primitives. It therefore occupies the rung-derivation step of the phi-ladder mass formula (yardstick times phi to the power of rung minus 8 plus gap). The module remains a narrative scaffold, so the torsion values still await derivation from the Recognition Composition Law or the T7 eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.