pith. machine review for the scientific record. sign in
module module low

IndisputableMonolith.Masses.Ribbons.Word

show as:
view Lean formalization →

This module defines a word as a list of ribbon syllables in the masses domain. It supplies the basic sequence type for ribbon constructions used in mass derivations. The module is purely definitional with no proofs or theorems.

claimA word is a finite list of ribbon syllables, written $w = [s_1, s_2, ..., s_n]$ where each $s_i$ is a syllable drawn from the ribbon structure.

background

The module sits inside the masses domain of Recognition Science and imports Mathlib for list primitives. It introduces the Word type as a list of syllables, with the sibling Ribbon module supplying the syllable elements. The setting treats words as the sequence objects that compose into ribbon-based mass formulas on the phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Word definition that feeds mass ribbon constructions and the phi-ladder mass formulas. It supports the representation of sequences required by downstream theorems in the masses domain that connect to the unified forcing chain and the eight-tick octave.

scope and limits

declarations in this module (2)