musicCost_self
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute costs between distinct interval steps.
- Does not derive the full T0-T8 forcing chain or physical constants.
- Does not address mass formulas or Berry thresholds.
formal statement (Lean)
24@[simp] theorem musicCost_self (a : MusicalIntervalStep) : musicCost a a = 0 := by
proof body
One-line wrapper that applies simp.
25 simp [musicCost]
26