strictMusicRealization
plain-language theorem explainer
Researchers in Recognition Science cite strictMusicRealization when building admissible instances for the four canonical domains in the universal forcing equivalence. It equips the set of positive real frequency ratios with ratio-derived comparison costs, multiplicative composition, the number 1 as identity, and the octave ratio as generator. The definition assembles the StrictLogicRealization structure by direct field assignment, with the nontriviality law discharged by a short calculation that the octave differs from unity.
Claim. Let $R = {x : ℝ | 0 < x}$ be the set of positive reals. The strict musical realization is the structure on carrier $R$ with cost values in ℕ, comparison given by the ratio cost function $r ↦ C(r,1)$, composition by multiplication of ratios, identity element 1, and generator the octave ratio 2, satisfying the identity, symmetry, and nontriviality laws.
background
FrequencyRatio is the subtype of positive real numbers. ratioCost is the comparison operator applied to a ratio and unity, drawn from PositiveRatioForcing. The octave generator is supplied as the ratio 2 from MusicalScale (with an alternative 8-tick definition in Constants) and serves as the fundamental evolution period in the forcing chain. This module supplies a domain-rich musical realization over positive frequency ratios in which comparison uses equality-cost on ratios; richer psychoacoustic dissonance costs can be substituted in later refinements.
proof idea
The definition populates the StrictLogicRealization fields directly: Carrier to FrequencyRatio, Cost to Nat, compare to ratioCost, compose to ratio multiplication, one to the positive unit, and generator to octave. Identity and non-contradiction laws are instantiated by ratioCost_self and ratioCost_symm. The nontrivial_law is proved by assuming octave equals the unit, extracting the underlying real value, applying norm_num to reach a contradiction, and simplifying the cost expression.
why it matters
This definition supplies the musical instance among the four canonical domains whose admissibility witnesses appear in AdmissibleClassCert and four_canonical_domains_admissible. It realizes the eight-tick octave generator from forcing-chain step T7 and feeds the quantified universal forcing theorem. Downstream it supports the arithmetic equivalence to LogicNat and the RichDomainCosts associativity and identity lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.