inv
plain-language theorem explainer
The inv definition supplies the inverse operation on a Ribbon by flipping its direction Boolean and negating its integer bit while preserving start and tag. Workers on ribbon sequences, gauge equivalence, or mass-ladder constructions cite it when composing syllables or verifying cancellation. The implementation is a one-line record update with no lemmas or tactics.
Claim. Let $r$ be a ribbon with start tick, direction $d$ (Boolean), ledger bit $b$ (integer), and gauge tag. Then $r^{-1}$ is the ribbon identical to $r$ except that its direction is the negation of $d$ and its bit is $-b$.
background
Ribbon is the structure that models a syllable on the eight-tick clock: it carries a start field of type Tick (the fundamental RS time quantum with value 1), a Boolean direction, an integer bit intended to be ±1, and a gauge tag. The Masses.Ribbons module records this as a narrative scaffold for φ-ladder ribbon machinery; the file is classified as Model and downstream code treats its objects as demo inputs rather than fully formalised RS derivations. Upstream, the tick definition from Constants fixes the time quantum, while the for structure from UniversalForcingSelfReference supplies the meta-realization context in which ribbon operations are expected to live.
proof idea
This is a direct definition that constructs the inverse ribbon via record-update syntax, negating the direction field and negating the bit field. No lemmas are invoked; the construction simply reuses the Ribbon structure fields.
why it matters
The definition feeds the inversion operation into downstream results including toComplex_inv (which shows the complex representation commutes with inversion), the left- and right-inverse theorems for RecognitionAutomorphism in RecogGeom.Symmetry, and closure arguments in Navier-Stokes and EulerInstantiation. It supplies the concrete inverse needed for the ribbon model that appears in mass formulas and gauge-equivalence steps of the Recognition Science framework, sitting inside the eight-tick octave and φ-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.