Word
plain-language theorem explainer
A word is defined as a finite sequence of ribbon syllables on the eight-tick clock. Mass derivations in the Recognition framework cite this when extracting rungs and canonical masses from ribbon patterns. The declaration is a direct type abbreviation with no further axioms or reductions.
Claim. A word $W$ is a list of ribbons, where each ribbon is a 4-tuple $(s,d,b,t)$ with starting tick $s$ in the eight-tick clock, direction $d$ (clockwise or counterclockwise), bit value $b = 1$, and gauge tag $t$.
background
In the Masses.Ribbons module a ribbon is the atomic syllable on the eight-tick clock, carrying a start tick, direction flag, integer bit, and tag. Words assemble these syllables into sequences that later undergo rewriting and length reduction. The module imports only Mathlib and sits inside the larger ribbon model for particle masses.
proof idea
The declaration is a one-line abbreviation that directly identifies Word with the list type over Ribbon.
why it matters
This definition supplies the input type for every downstream ribbon operation, including ell (reduced length), rungFrom (generation class), massCanonFromWord (canonical mass), and normalForm (rewriting). It therefore anchors the ribbon-to-mass pipeline that feeds the phi-ladder mass formula and the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.