FrequencyRatio
plain-language theorem explainer
FrequencyRatio is the type of positive real numbers used as the carrier for frequency ratios in the strict musical realization. It is referenced by admissible class constructions and by the definitions of specific intervals such as the octave and perfect fifth. The declaration is a direct subtype abbreviation with no lemmas or tactics required.
Claim. A positive frequency ratio is any real number $x$ satisfying $x > 0$.
background
The Strict/Music module supplies a domain-rich musical realization over positive frequency ratios. Comparison proceeds by equality cost in this strict pass; richer psychoacoustic dissonance costs remain available for later refinement. FrequencyRatio supplies the carrier set for all ratio definitions and cost functions that follow in the module.
proof idea
Direct subtype abbreviation to the positive reals; no lemmas or tactics are applied.
why it matters
The type anchors the Music realization inside the UniversalForcing chain and supplies the domain for music_admissible together with the concrete intervals octave, perfectFifth and perfectFourth. It therefore supports the strict equality-cost model before any extension to richer costs. The placement aligns with the Recognition Science program of building admissible domain realizations that feed the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.