MusicalInterval
The structure packages a positive real ratio with its positivity witness and attaches the Recognition Science J-cost function. Music theorists formalizing harmonic modes cite it when instantiating concrete intervals such as the fifth or octave. The definition is a direct one-line wrapper that applies Jcost to the stored ratio field.
claimA musical interval is a pair $(r, p)$ where $r$ is a positive real number and $p$ is a proof that $0 < r$, equipped with the cost map sending the pair to $J(r) = (r + r^{-1})/2 - 1$.
background
The HarmonicModes module imports the Cost module and builds musical intervals as typed positive reals. Jcost is the function $J(x) = (x + x^{-1})/2 - 1$ that satisfies the Recognition Composition Law and arises from the T5 uniqueness step in the forcing chain. The structure supplies a uniform container so that concrete ratios can be packaged once and reused for cost calculations.
proof idea
The structure declaration introduces the ratio field and its positivity witness. The jcost method is a one-line wrapper that projects the ratio field and applies the Jcost function imported from the Cost module.
why it matters in Recognition Science
This structure supplies the common type for the seven standard interval definitions in the module, including octaveInterval, fifthInterval, fourthInterval, majorThirdInterval, minorThirdInterval, tritoneInterval, and unisonInterval. It embeds music theory into the Recognition framework by attaching J-cost, which traces to T5 J-uniqueness and the eight-tick octave. The definition thereby supports cost computations that may connect to the phi-ladder and alpha-band constants.
scope and limits
- Does not restrict ratios to rationals or superparticular forms.
- Does not evaluate the numerical value of J-cost.
- Does not derive ratios from the phi fixed point.
- Does not connect ratios to pitch classes or timbre.
formal statement (Lean)
97structure MusicalInterval where
98 ratio : ℝ
99 ratio_pos : 0 < ratio
100
101noncomputable def MusicalInterval.jcost (i : MusicalInterval) : ℝ :=
proof body
Definition body.
102 Jcost i.ratio
103