musicCost_symm
plain-language theorem explainer
The theorem establishes symmetry of the music cost on natural-number interval steps. Workers on the musical model inside the universal forcing chain cite it to confirm the compare operation satisfies the required symmetry for a LogicRealization. The proof proceeds by case split on equality of the steps, followed by direct simplification against the definition of musicCost.
Claim. For natural numbers $a$ and $b$, let $c(a,b)$ be $0$ if $a=b$ and $1$ otherwise. Then $c(a,b)=c(b,a)$.
background
The MusicRealization module supplies a lightweight carrier for interval steps whose semantics are pitch-ratio stacking and whose arithmetic counts interval compositions. MusicalIntervalStep is defined as the type of natural numbers. The function musicCost returns 0 on identical steps and 1 on distinct steps, supplying the compare operation for the subsequent LogicRealization.
proof idea
Case analysis on whether the two steps are equal. When equal, substitution reduces both sides to the zero case of musicCost. When unequal, the symmetric inequality is recorded and simplification maps both sides to the constant 1.
why it matters
Symmetry is a prerequisite for the musicRealization definition that builds a LogicRealization with Carrier equal to MusicalIntervalStep and compare equal to musicCost. The result therefore sits inside the musical realization of the forcing chain and supports the Recognition Composition Law at the level of interval arithmetic. It does not touch the J-uniqueness or eight-tick octave steps directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.