musicInterpret
plain-language theorem explainer
The definition converts each LogicNat element, which encodes iteration counts in the multiplicative orbit forced by the Law of Logic, into a natural number serving as a musical interval step. Researchers building the musical realization of universal forcing would cite this map when translating logic-derived counts into the carrier for interval composition. The definition is a one-line wrapper that applies the forward iteration-count map toNat.
Claim. The map sends each element $n$ of the inductive type LogicNat to the natural number recording its iteration count under the step constructor, yielding an element of MusicalIntervalStep (defined as the type of natural numbers).
background
The MusicRealization module supplies a lightweight carrier for musical realizations whose semantic content is pitch-ratio stacking; the forced arithmetic reduces to counting compositions of the interval generator. MusicalIntervalStep is the abbreviation for the natural numbers that records these interval steps. LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step, mirroring the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator γ and containing 1. The upstream map toNat reads off the iteration count by sending identity to 0 and each step n to the successor of toNat n.
proof idea
The definition is a one-line wrapper that applies the toNat function from ArithmeticFromLogic directly to the input LogicNat value, returning the resulting natural number as the MusicalIntervalStep.
why it matters
This definition supplies the carrier translation required by the downstream musicRealization, which constructs a LogicRealization instance with Carrier set to MusicalIntervalStep, Cost set to Nat, and compare set to musicCost. It completes the bridge from the forced arithmetic of LogicNat into the discrete interval steps of the musical model, supporting the pitch-ratio stacking semantics in the foundation layer of the universal forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.