_music_ok
plain-language theorem explainer
The definition establishes an equivalence showing that the Peano carrier extracted from the arithmetic of the strict musical realization matches the natural numbers forced by the Law of Logic. Researchers auditing domain-specific strict realizations in the Universal Forcing framework would cite it to confirm arithmetic consistency across domains. It proceeds as a direct one-line wrapper applying the orbit equivalence from the lightweight conversion of the music structure.
Claim. Let $R$ be the strict realization of music with frequency ratios as carrier and octave stacking as composition. The carrier of the Peano arithmetic derived from $R$ is equivalent to the inductive natural numbers generated by the Law of Logic.
background
StrictLogicRealization is a structure with Carrier type, Cost type (with zero), compare function, and compose operation, encoding a strict Law-of-Logic realization without supplied orbit. The strictMusicRealization sets Carrier to FrequencyRatio, Cost to Nat, and compose to multiplication of positive reals, using octave stacking as generator. The arith function extracts forced arithmetic from the lightweight version of any such realization. LogicNat is the inductive type with constructors identity and step; as stated in its definition, 'identity represents the zero-cost element (the multiplicative identity in the orbit). step represents one more iteration of the generator. The two-constructor structure mirrors the orbit {1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1.' This declaration appears in the AxiomAudit module, which supplies an audit surface for the strict, domain-rich Universal Forcing completion pass.
proof idea
This is a one-line wrapper that applies the orbitEquivLogicNat equivalence obtained from the toLightweight conversion of the strict music realization.
why it matters
This definition verifies that the musical realization using octave stacking satisfies the arithmetic equivalence required by the strict Universal Forcing framework. It forms part of the AxiomAudit collection that checks multiple domains against the core LogicNat structure. In the Recognition Science setting, it supports the emergence of arithmetic from the Law of Logic as described in the forcing chain, without introducing additional hypotheses. No specific open questions are addressed here, but it contributes to closing the strict realization pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.