Ribbon
plain-language theorem explainer
Ribbon defines the basic syllable for the eight-tick ribbon model of masses as a quadruple of start tick, direction flag, integer bit, and gauge tag. Researchers constructing particle representations on the phi-ladder would cite this structure when building words for mass assignments. The declaration is a direct structure definition that supplies field accessors with no computational reduction or lemmas.
Claim. A ribbon syllable consists of a starting tick $t$ from the eight-tick clock, a direction flag $d$, an integer ledger bit $b$, and a gauge tag $g$ from the unit type.
background
The module records a placeholder mass-ribbon construction on the eight-tick clock as a narrative scaffold; RS derivations remain unformalised and the module is marked Model. Tick is the abbreviation Fin 8 for discrete time steps, while GaugeTag is the unit type equipped with trivial decidable equality and ordering instances. Upstream, the TimeEmergence Tick structure treats time as discrete ledger steps with no background manifold, ordered solely by index.
proof idea
The declaration is a direct structure definition introducing the four fields start of type Tick, dir of type Bool, bit of type Int, and tag of type GaugeTag. No lemmas or tactics are invoked; the body is empty beyond the field declarations.
why it matters
Ribbon supplies the element type for Word as List Ribbon and for the predicates cancels, inv, and neutralCommute. It occupies the position of the basic syllable in the eight-tick octave machinery (T7) within the Recognition Science mass model, though the module remains a scaffold pending formalisation of the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.