MusicalInterval
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.