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

IndisputableMonolith.Masses.Ribbons

show as:
view Lean formalization →

The Ribbons module supplies axiom stubs and basic definitions for ribbon structures supporting mass ladder constructions in Recognition Science. It introduces Ribbon as the core object along with Tick, GaugeTag, Z_quark, Z_lepton and operations inv, cancels, neutralCommute, Word, ringSeq, rewriteOnce, normalForm. Researchers building sector models for particle masses via the phi-ladder would reference these stubs. The module consists entirely of definitions and axioms with no theorems or proofs.

claimThe module defines the ribbon structure $R$ together with inversion $R^{-1}$, cancellation, neutral commutation, word sequences, ring sequences, rewrite rules and normal forms for constructing mass ladders on the phi-ladder.

background

Recognition Science derives masses from the phi-ladder using the J-cost function $J(x) = (x + x^{-1})/2 - 1$ and defect distances. The Ribbons module introduces the basic objects needed for ribbon-based mass models: Tick as the discrete time unit, GaugeTag for sector labeling, Z_quark and Z_lepton for charge assignments, and Ribbon as the composite structure obeying the Recognition Composition Law. Supporting operations include inv for inversion, cancels for pairwise cancellation, neutralCommute for commutation relations, Word and ringSeq for sequence construction, rewriteOnce for reduction steps, and normalForm for canonical representatives. The module imports only Mathlib and serves as a dependency stub for the masses domain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the SectorPrimitive module, which supplies witness records for ribbon-based mass ladders as a documentation placeholder. It provides the axiom stubs required to support downstream mass derivations from the eight-tick octave and phi fixed point in the unified forcing chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (22)