music_arith_equiv_nat
plain-language theorem explainer
The musical realization of the law of logic yields a Peano arithmetic whose carrier set is equivalent to the inductively defined natural numbers forced by logic. Researchers tracing universal forcing from logic to arithmetic cite this to verify that interval-step models recover standard naturals. The definition is a direct one-line wrapper applying the orbit equivalence already present in the music realization.
Claim. Let $R$ be the musical realization of the law of logic. The carrier of the Peano arithmetic extracted from $R$ is equivalent to the natural numbers forced by the law of logic.
background
The module defines a lightweight musical realization whose carrier records interval steps. Pitch-ratio stacking supplies the semantics while the forced arithmetic counts iterations of interval composition. The arithmeticOf function extracts the forced arithmetic object from any logic realization. LogicNat is the inductive type whose identity constructor is the zero-cost multiplicative identity and whose step constructor adds one iteration of the generator, mirroring the orbit under repeated multiplication by that generator.
proof idea
The definition is a one-line wrapper that applies the orbit equivalence from the music realization to identify the Peano carrier with LogicNat.
why it matters
This equivalence confirms that the musical realization produces the standard natural numbers as its arithmetic carrier, supporting the universal forcing result that arithmetic objects extracted from distinct realizations coincide. It sits inside the MusicRealization submodule and closes a definitional bridge between interval-step models and the logic-forced naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.