Ribbon
plain-language theorem explainer
Ribbon defines the four-field syllable on the eight-tick clock that serves as the atomic unit for words in the masses module. Mass and ledger modelers cite it when building sequences that must satisfy the downstream cancellation and commutation predicates. The declaration is a direct structure definition that introduces the fields with no computational content or lemmas.
Claim. A ribbon syllable is a 4-tuple consisting of a starting tick $s$ in the 8-cycle, a direction $d$ (boolean), an integer bit $b$, and a natural-number tag $t$.
background
Recognition Science places physical quantities on discrete φ-tiers with the eight-tick octave fixed by T7 of the unified forcing chain. The IntegrationGap.A definition sets the active edge count per tick to 1, yielding the identity φ^(A − gap) · φ^gap = φ at D = 3. LedgerFactorization.of supplies the calibration of the J-cost on (ℝ₊, ×), while NucleosynthesisTiers.of and SimplicialLedger.EdgeLengthFromPsi.is embed the discrete ticks into nuclear densities and Regge-type edge lengths.
proof idea
This is a structure definition that directly declares the four fields start : Fin 8, dir : Bool, bit : Int, tag : Nat. No lemmas are invoked and no tactics are used; the declaration simply introduces the type.
why it matters
The structure supplies the syllables whose lists become the Word type and feed the cancels, inv, and neutralCommute predicates in the parent Ribbons module. It realizes the T7 eight-tick clock and supports ledger additivity required by the φ-ladder mass formulas. Downstream doc-comments note that swapping preserves additivity provided start ticks differ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.