ratioCost_self
plain-language theorem explainer
The self-cost of any positive frequency ratio under the equality-based comparison is zero. Researchers formalizing strict realizations of logic in musical frequency spaces within Recognition Science cite this identity when establishing reflexive zero-cost properties. The proof is a one-line simp wrapper that unfolds the local definition of ratioCost.
Claim. For every positive frequency ratio $a$, the equality-based cost satisfies $ratioCost(a,a)=0$.
background
FrequencyRatio is the subtype of positive reals serving as carrier for frequency ratios. The local ratioCost on pairs of FrequencyRatio returns the natural number 0 precisely when the arguments are equal and 1 otherwise, implementing a strict equality comparison. This module supplies a domain-rich musical realization over positive frequency ratios; the comparison uses equality-cost on ratios for the strict pass, with richer psychoacoustic dissonance costs available for later refinement. The construction draws on the scale-invariant comparison framing from PositiveRatioForcing.
proof idea
The proof is a one-line simp wrapper that applies the definition of ratioCost, which returns 0 on identical arguments by direct case analysis.
why it matters
This zero-cost identity for reflexive comparisons supports the definition of strictMusicRealization as a StrictLogicRealization whose Carrier is FrequencyRatio and whose Cost is Nat. It contributes to the claim that music realizes a positive-ratio subrealization of logic, consistent with the Recognition Composition Law and the T0-T8 forcing chain. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.