ratioCost_symm
plain-language theorem explainer
The equality-based cost on positive frequency ratios is symmetric. Researchers constructing strict musical realizations of logic cite this to confirm the comparison operator is symmetric under input swap. The proof splits into cases on whether the ratios coincide, substitutes when equal, and simplifies the definition to one in the unequal case.
Claim. Let $a, b > 0$ be positive reals. Define the cost $c(a,b)$ to be $0$ if $a = b$ and $1$ otherwise. Then $c(a,b) = c(b,a)$.
background
FrequencyRatio is the subtype of positive reals, used here to represent frequency ratios. The local ratioCost returns the natural number 0 on equal inputs and 1 otherwise, implementing a strict equality comparison. The module develops a domain-rich musical realization over these ratios, with the equality cost serving as the comparison; richer psychoacoustic dissonance costs can replace it later.
proof idea
The tactic proof applies by_cases on a = b. The equal case substitutes and simplifies directly via the definition. The unequal case introduces the symmetric inequality and simplifies both sides of the cost definition to 1.
why it matters
This symmetry is invoked by strictMusicRealization to equip the StrictLogicRealization with a symmetric compare operation on FrequencyRatio carriers. It completes the musical realization step inside the strict forcing chain, ensuring the cost satisfies the symmetry needed for the Recognition Composition Law and the subsequent octave stacking that forces the eight-tick period and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.