MusicalIntervalStep
plain-language theorem explainer
MusicalIntervalStep aliases the natural numbers to act as the carrier recording interval steps for a musical realization of the forcing. It is referenced directly by musicCost, musicInterpret, and the musicRealization structure that supplies a LogicRealization instance. The declaration is a one-line abbreviation and carries no proof obligations.
Claim. The carrier type for musical interval steps is the set of natural numbers $N$.
background
The MusicRealization module supplies a lightweight carrier whose semantic reading is pitch-ratio stacking, with the forced arithmetic given by the iteration count of interval composition. MusicalIntervalStep is introduced as the type of these steps. It is then used to define musicCost (returning 0 on equality, 1 otherwise), musicInterpret (mapping LogicNat to the carrier), and musicRealization (the LogicRealization record with Carrier set to this type and compare set to musicCost).
proof idea
One-line abbreviation that sets the carrier to the natural numbers.
why it matters
The definition supplies the carrier for musicRealization, which implements the LogicRealization interface inside UniversalForcing. It is used by the musicCost family of results and by musicInterpret. The construction sits inside the musical realization of the forcing chain and supports the iteration-count arithmetic described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.