ell
plain-language theorem explainer
ell defines the reduced length of a ribbon word as the length of its normal form after bounded normalization passes. Mass-spectrum workers on the phi-ladder cite it when mapping syllable sequences to rung numbers in RungSpec. The definition is a direct one-line extraction of length from the output of normalForm.
Claim. For a word $W$ that is a list of ribbon syllables, the reduced length $ell(W)$ equals the length of the normal form of $W$.
background
In the masses module a Word is an abbrev for a list of Ribbon syllables. The normalForm function applies rewriteOnce repeatedly for at most length passes, returning the first fixed point. This construction sits inside a placeholder model for phi-ladder ribbon machinery; the module is explicitly marked as narrative scaffold with RS derivations not yet formalised. Upstream it depends on the tick as the fundamental RS time quantum and on the for structure recording meta-realization coherence axioms.
proof idea
One-line definition that applies normalForm to the input word and returns the length of the resulting list.
why it matters
ell supplies the ell field of RungSpec and is used by rungFrom to build rung numbers from words and generation classes. It therefore feeds the mass formula yardstick * phi^(rung-8+gap(Z)) on the phi-ladder. The definition supports downstream uses in encodeIndex for LNAL voxels and in tailFluxVanish closures for RM2U profiles. Because the module remains a model scaffold, it touches the open question of formalising the full Recognition Science mass derivations from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.