Word
plain-language theorem explainer
Word is the type of finite sequences of ribbon syllables, each carrying a tick, direction, bit and gauge tag on the eight-tick clock. Mass-model developers in Recognition Science cite it when assembling states for the φ-ladder before applying normalization or rung extraction. The declaration is a direct type abbreviation with no further computation.
Claim. A word is a finite list of ribbon syllables, where each syllable consists of a starting tick on the eight-tick clock, a direction (positive or negative), an integer bit, and a gauge tag.
background
The module supplies a placeholder mass-ribbon construction. A Ribbon is the structure with fields start : Tick, dir : Bool, bit : Int, tag : GaugeTag that encodes one syllable on the eight-tick clock. The file records the φ-ladder ribbon machinery as a narrative scaffold; the RS derivations are not yet formalised and downstream code treats the objects as demo inputs.
proof idea
The declaration is a direct abbreviation that aliases List Ribbon to the name Word.
why it matters
Word supplies the input type for ell (reduced length of normal form), massCanonFromWord (canonical mass from word, generation and charge), rungFrom, normalForm, rewriteOnce and ringSeq. It therefore anchors the ribbon-based mass construction that feeds the eight-tick octave and φ-ladder steps of the forcing chain. The module remains a scaffold pending full formalization of the RS derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.