RungSpec
plain-language theorem explainer
RungSpec pairs a reduced word length ell with one of three generation classes to label positions on the Recognition Science mass ladder. Mass modelers cite it when building explicit phi-powered spectra from ribbon words. The declaration is a bare structure with no axioms or computational steps.
Claim. A rung specification consists of a natural number $ell$ (the reduced length of a word) together with a generation class $g$ belonging to the set ${g_1, g_2, g_3}$.
background
The masses module constructs particle masses on the phi-ladder by first reducing words in the ribbon algebra and then assigning each reduced object to a rung. The upstream definition ell extracts the length of the normal form of a word, while GenClass is the inductive enumeration of the three generations. These two pieces are packaged together so that rung numbers can be computed uniformly for all kernel types.
proof idea
The declaration is a structure definition with an empty proof body. It simply records the ell field supplied by the ribbons module and the GenClass inductive type already present in the same file.
why it matters
RungSpec supplies the input type for rungOf, which returns the integer rung as ell plus tauOf of the generation. That integer enters the mass formula yardstick times phi to the power (rung minus 8 plus gap), linking ribbon reductions directly to the T7 eight-tick octave and the T8 requirement of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.