ratioCost
plain-language theorem explainer
ratioCost maps equal positive frequency ratios to cost 0 and unequal ones to cost 1. Researchers building strict musical realizations cite it as the base equality comparison operator. The definition is a direct conditional on whether the two ratios coincide.
Claim. For positive frequency ratios $a, b > 0$, the ratio cost is defined by $ratioCost(a, b) = 0$ if $a = b$ and $1$ otherwise.
background
The Music module supplies a domain-rich realization of musical structures over positive frequency ratios. FrequencyRatio is the subtype of positive reals. The module states that comparison uses equality-cost on ratios for this strict pass, with room for later psychoacoustic dissonance refinement.
proof idea
Direct definition by case split: return 0 when the two FrequencyRatio arguments are equal, else 1. No lemmas or tactics are applied.
why it matters
It supplies the compare field inside strictMusicRealization, a StrictLogicRealization with FrequencyRatio carrier and Nat cost. This enables ratioCost_self, ratioCost_symm, and music_arith_equiv_logicNat. It realizes the strict music subrealization step preparatory to octave stacking under the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.