ratioCost_symm
plain-language theorem explainer
Symmetry of the equality-based cost on positive frequency ratios. Researchers constructing strict logic realizations in musical structures cite this to confirm the compare operation is symmetric. The proof proceeds by case analysis on equality of the ratios, with direct simplification in each branch.
Claim. For positive frequency ratios $a, b > 0$, the cost of comparing $a$ to $b$ equals the cost of comparing $b$ to $a$, where the cost equals 0 on equality and 1 otherwise.
background
FrequencyRatio is the subtype of positive reals serving as carrier for the musical realization. The local ratioCost returns the natural number 0 when its two arguments coincide and 1 otherwise, implementing a strict equality comparison. The module supplies a domain-rich musical realization over positive frequency ratios with equality-cost on ratios for this strict pass; richer psychoacoustic costs may be substituted later.
proof idea
Case analysis on whether the two ratios are equal. When equal, substitution followed by simplification using the definition of ratioCost yields the result. When unequal, the symmetric inequality is recorded and simplification again confirms the costs are identical.
why it matters
The symmetry is invoked by strictMusicRealization, which builds a StrictLogicRealization whose compare field is exactly this ratioCost. It thereby supplies an invariance property required for the musical carrier to realize the underlying logic. The result sits inside the UniversalForcing.Strict.Music development and supports the broader forcing chain by ensuring the cost function respects the necessary symmetry for positive-ratio comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.