semitoneRatio
plain-language theorem explainer
semitoneRatio supplies the equal-tempered frequency ratio for one semitone as 2 raised to the power 1/12. Researchers tracing the 12-tone scale to the golden ratio φ would reference it when constructing closure properties of the circle of fifths. The definition is a direct real-number exponentiation with no lemmas or hypotheses.
Claim. The frequency ratio for one semitone in equal temperament is defined by $2^{1/12}$.
background
The module Aesthetics.MusicalScale connects the Western 12-tone scale to φ by showing that 12 semitones per octave satisfy 2^{1/12} ≈ 1.0595 while the perfect fifth at 2^{7/12} ≈ 1.4983 lies close to 3/2. Upstream results define fifth as the constant 3/2 in both CircleOfFifths and HarmonicModes, with the explicit remark that the ratio of musical semitones (12) to RS modes (8) equals the perfect fifth. The local setting treats 12 as emerging from optimization of consonance, closure after n fifths, and φ-scaling via 12 ≈ φ^5 / log(3/2).
proof idea
The declaration is a direct definition that evaluates the real exponentiation 2^(1/12) with no tactic steps or lemma applications.
why it matters
This definition anchors the 12-tone division inside the Recognition framework by supplying the base unit that later yields the circle-of-fifths closure (3/2)^12 ≈ 2^7. It fills the module's claim that 12 arises from φ^5 scaling and the eight-tick octave structure, yet no downstream theorems currently consume it, leaving open its precise embedding into the T7 octave and the mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.