ringSeq
plain-language theorem explainer
ringSeq constructs a deterministic list of n ribbon syllables for any gauge tag, spreading them over the eight-tick cycle with strictly alternating directions. Mass-model builders in Recognition Science cite it when generating phi-ladder inputs for ribbon words. The definition is a direct computational construction that applies modular arithmetic to index ticks and parity to set directions.
Claim. For gauge tag $g$ and natural number $n$, ringSeq$(g,n)$ yields the list of $n$ ribbon syllables $r_k$ ($k=0$ to $n-1$) where each $r_k$ has tick index $k mod 8$, direction true precisely when $k$ is even, bit value 1, and tag $g$.
background
The Masses.Ribbons module is explicitly a narrative scaffold for mass-ribbon constructions; its derivations remain informal and the code is treated as demo input. GaugeTag is the placeholder type Unit. Word is the abbreviation List Ribbon. Tick is the abbreviation Fin 8, realising the eight-tick octave. Upstream, TimeEmergence.Tick supplies the atomic ledger unit with index-based ordering, while present extracts the current snapshot.
proof idea
Direct definition: map List.range n to a Ribbon constructor, computing the tick via k % 8 wrapped in Fin 8, direction via k % 2 = 0, and fixing bit 1 together with the supplied tag. No lemmas or tactics are invoked.
why it matters
Supplies the canonical ring pattern required by the eight-tick clock (T7) for any subsequent ribbon-based mass formula on the phi-ladder. It populates the Word type used in the scaffold for yardstick * phi^(rung-8+gap(Z)) constructions. Although no downstream theorems yet depend on it, the definition closes the placeholder for embedding the Recognition Composition Law into the mass sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.