ratioCost_decidable
The definition supplies a decidable instance for equality between positive frequency ratios. Researchers establishing strict realizations of universal forcing in the music domain cite it to obtain excluded middle for ratio costs. The implementation is a direct appeal to classical decidability on the underlying real numbers.
claimFor positive real numbers $a, b > 0$, the predicate $a = b$ is decidable.
background
FrequencyRatio is the subtype of positive reals, serving as the carrier for music-domain costs. The Rich Domain Cost Theorems module supplies the concrete content for five domains (Music, Biology, Narrative, Ethics, Metaphysical) that were previously declared only as placeholders with excluded_middle_law := True. This definition discharges the decidability requirement for the music domain's ratio costs, ensuring the strict realization carries non-trivial logical structure.
proof idea
One-line wrapper that applies Classical.dec to equality on the subtype of positive reals.
why it matters in Recognition Science
This declaration completes the excluded-middle component for music-domain ratio costs, as required by the module design that replaces placeholder laws with first-class statements. It sits alongside the zero-cost, associativity, and invariance results in the same file and supports any downstream claim that the music realization is law-bearing. In the broader framework it ensures the forcing chain's logical operations remain decidable when realized in the music domain.
scope and limits
- Does not establish zero cost if and only if equality.
- Does not treat composition or invariance laws.
- Does not extend to Biology, Narrative, Ethics, or Metaphysical domains.
- Does not derive any numerical cost values or triangle inequalities.
formal statement (Lean)
52def ratioCost_decidable (a b : FrequencyRatio) :
53 Decidable (a = b) := Classical.dec _
proof body
Definition body.
54