fourthInterval
The fourth interval is formalized as the musical interval carrying ratio 4/3. Analysts of harmonic modes in the Recognition framework cite this definition when assembling interval lattices from the J-cost. The construction is a direct application of the MusicalInterval structure to the pre-established ratio and its positivity witness.
claimThe fourth interval is the musical interval whose ratio equals $4/3$.
background
MusicalInterval is the structure whose fields are a real ratio and a proof that the ratio is positive. Its jcost method applies the J-cost function to the ratio. The fourth ratio is the constant 4/3, whose positivity follows from direct numerical normalization.
proof idea
The definition is a one-line wrapper that invokes the MusicalInterval constructor on the fourth ratio and the fourth_pos theorem.
why it matters in Recognition Science
This entry populates the set of basic intervals used to define harmonic modes. It supplies a concrete case for the J-cost evaluation in music-theoretic contexts. The module catalogs similar intervals such as the octave and fifth, but no further theorems yet depend on this specific definition.
scope and limits
- Does not establish relations to other intervals such as the fifth.
- Does not evaluate the J-cost of the interval.
- Does not address superparticular properties beyond the ratio.
formal statement (Lean)
113noncomputable def fourthInterval : MusicalInterval :=
proof body
Definition body.
114 ⟨fourth, fourth_pos⟩
115