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