musicCost_self
plain-language theorem explainer
The theorem establishes that the cost of any musical interval step compared to itself is zero. Researchers verifying zero-cost self-comparisons in the interval-step carrier of the Recognition Science music realization would cite it. The proof is a one-line simp wrapper that unfolds the musicCost definition to the equality case.
Claim. For every natural number $a$, the music cost satisfies $musicCost(a,a)=0$.
background
The MusicRealization module supplies a lightweight carrier for interval steps under the universal forcing. MusicalIntervalStep is defined as the type of natural numbers, with the semantic reading of pitch-ratio stacking whose arithmetic counts interval compositions. The function musicCost is defined by cases: it returns 0 precisely when the two arguments are equal and 1 otherwise.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of musicCost, reducing the goal directly to the reflexive case of equality.
why it matters
This theorem supplies the zero-cost self-comparison required by the downstream musicRealization definition, which instantiates LogicRealization with MusicalIntervalStep as carrier and musicCost as compare. It thereby closes the zero element of the cost structure inside the musical realization of the forcing chain, consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.