GaugeTag
plain-language theorem explainer
GaugeTag supplies a placeholder singleton type for labeling gauge properties inside the ribbon construction of the Recognition Science mass model. It is referenced when building Ribbon structures and the ringSeq generator on the eight-tick clock. Mass derivations cite it as the tag field that carries no additional structure. The implementation is a direct abbreviation to the unit type together with trivial derived instances for equality and ordering.
Claim. The gauge tag type is the singleton type, equipped with decidable equality that holds by reflexivity and with order relations that are constantly false for strict order and constantly true for non-strict order.
background
In Recognition Science, temporal progression occurs in discrete atomic units called ticks; the local module uses an eight-tick clock (Tick := Fin 8) as the period for ribbon syllables. The module itself is a narrative scaffold for the φ-ladder ribbon machinery, with masses intended to scale as φ^r modulated by charge Z, but the derivations remain unformalized and are treated as demo inputs. Upstream, Tick is introduced as a structure carrying a natural-number index and ordered by that index, representing the atomic unit of time with no background manifold.
proof idea
The declaration is a one-line type abbreviation to the unit type. It is followed by derived instances: Repr formats the tag as a literal string, DecidableEq returns true by reflexivity, LT is constantly false, and LE is constantly true. Parallel trivial instances are supplied for the product type that pairs the tag with Tick, Bool, and ℤ.
why it matters
GaugeTag supplies the tag field required by the Ribbon structure and the ringSeq generator that produces deterministic alternating patterns across the eight-tick clock. It occupies a placeholder slot in the mass-ribbon model, connecting to the T7 eight-tick octave of the forcing chain while the module awaits formalization of the φ-ladder mass formula. The declaration therefore marks an open scaffolding point between the discrete-time foundation and the intended RS-native mass derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.