fifth
plain-language theorem explainer
The fifth supplies the just perfect fifth ratio as the real number 3/2. Music theorists and Recognition Science researchers cite it to realize the 12/8 bridge between semitones and the eight RS modes per octave. The declaration is a direct noncomputable assignment with no lemmas or computation.
Claim. The perfect fifth frequency ratio is defined to be the real number $3/2$.
background
The CircleOfFifths module links musical intervals to Recognition Science by importing HarmonicModes and establishing the 12/8 bridge. Recognition Science uses eight modes per octave (T7 landmark) while conventional music employs twelve semitones; their ratio equals the just fifth. Upstream structures include the J-cost from PhiForcingDerived.of and the modes Finset from Galerkin2D.modes, which supply the discrete octave partitioning.
proof idea
This is a direct definition that assigns the constant 3/2. No tactics or lemmas are invoked; the body is a primitive real-number literal.
why it matters
The definition feeds the parent results comma_small, perfectFifth, and semitoneRatio in MusicalScale, plus rsPredictions in DarkEnergy. It realizes the T7 eight-tick octave by equating 12/8 to 3/2 and supplies the interval used in ledger-tension arguments for constant dark-energy density. It closes the music-to-phi-ladder link without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.