deltaOf
plain-language theorem explainer
deltaOf extracts the integer rung for a generator class and a primitive by applying the ribbon rung function directly to the primitive's word. Researchers modeling discrete mass ladders in Recognition Science would cite this when assigning levels to sector primitives on the phi-ladder. The definition is a direct one-line delegation to rungFrom, with an accompanying reflexivity example confirming invariance.
Claim. For a generator class $gen$ and a primitive $p$ whose word $w$ satisfies the normal-form condition, define $delta(gen, p) :=$ the rung integer extracted from $gen$ and $w$.
background
The module supplies placeholder witness records for ribbon-based mass ladders. Primitive is the structure consisting of a word together with the proof that the word equals its own normal form under Ribbons.normalForm. Local conventions treat these primitives as canonical generators whose rung values determine placement on the discrete phi-ladder for mass assignments. Upstream rung definitions appear in Compat.Constants (fixed value 1) and Engineering.AsteroidOreSpectroscopy (class-dependent values 0-4), while related structures such as UniversalForcingSelfReference.for record meta-realization properties that the rung extraction must eventually respect.
proof idea
One-line definition that applies Ribbons.rungFrom to the supplied generator class and the word field of the primitive. The accompanying example discharges the definitional equality by reflexivity.
why it matters
This definition supplies the rung extraction step required for mass-ladder constructions in the Masses domain. It directly supports the phi-ladder mass formula (yardstick times phi to the power of rung offset) and the eight-tick octave structure (T7) of the forcing chain. Although currently a documentation placeholder with no downstream uses, it closes the interface between ribbon words and discrete rung labels, leaving open the question of generator-independent rung invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.