rungOf
plain-language theorem explainer
The rungOf definition computes an integer rung index for a RungSpec by casting its ell field to ℤ and adding the tau offset of its gen field. Mass-spectrum researchers cite it to locate kernel specifications on the discrete phi-ladder. The definition is a direct one-line projection and addition using the case table for tauOf.
Claim. For a RungSpec $R$ with natural-number component $ell$ and generator class $g$, the rung index equals $ell + tau(g)$, where $tau$ sends the three generator classes to the integers 0, 11 and 17 respectively.
background
RungSpec is the structure pairing a natural number ell (reduced length of a normal-form word) with a GenClass (one of g1, g2, g3). tauOf is the function that returns the integer offsets 0, 11, 17 for those three classes. ell itself is imported from Ribbons as the length of the normal form of a word. This local definition supplies the rung index that LedgerUnits.rungOf later packages as the toZ coefficient of a delta-element.
proof idea
One-line definition that projects the ell field of RungSpec, casts it to ℤ, and adds the value of tauOf applied to the gen field.
why it matters
rungOf supplies the rung index used by LedgerUnits.rungOf, rungOf_fromZ and rungOf_step, and by the Derivation in Ribbons. It realizes the mapping from kernel types to positions on the phi-ladder whose masses are yardstick times phi to the power (rung minus 8 plus gap(Z)). The construction supports the self-similar fixed point (T6) and the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.