fifth
plain-language theorem explainer
The declaration supplies the frequency ratio of the perfect fifth as three halves. Music theorists and cosmologists working within Recognition Science cite it when deriving interval relations such as the Pythagorean comma or when linking ledger tension to dark energy predictions. It is introduced as a direct real-number assignment with no computation or further reduction.
Claim. The perfect fifth frequency ratio is defined as $3/2$.
background
The HarmonicModes module imports Mathlib and the Cost module and defines a family of musical intervals. The upstream CircleOfFifths.fifth carries the identical assignment together with the explicit remark that the ratio of musical semitones (12) to RS modes (8) is the perfect fifth. This placement embeds the classical interval inside the Recognition Science forcing chain, where T7 fixes the eight-tick octave and the Recognition Composition Law governs interval products.
proof idea
The definition is a direct assignment of the real number 3/2. It functions as a one-line wrapper that mirrors the upstream definition in CircleOfFifths.
why it matters
The definition is referenced by comma_small (which proves the Pythagorean comma is less than 1.02), by perfectFifth and semitoneRatio in MusicalScale, and by the dark-energy theorems constant_energy_density and rsPredictions that treat ledger tension as scale-independent. It thereby realizes the 12/8 bridge that connects music theory to the eight-tick octave (T7) and to the emergence of D = 3 spatial dimensions. No open scaffolding questions are closed by this definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.