semitonesPerOctave
The declaration fixes the semitone count per octave at twelve inside the Recognition Science model of equal-tempered scales. Researchers deriving Fibonacci-like scale sizes or circle-of-fifths closure from φ would cite this constant when linking 5 + 7 = 12 or when approximating φ^5. The definition is a direct numeric assignment with no computation or hypotheses.
claimThe number of semitones in one octave is defined to be twelve: $12$.
background
The module Aesthetics.MusicalScale develops the Western 12-tone equal-temperament scale from the golden ratio φ. It records that twelve semitones yield the frequency ratio 2^(1/12) ≈ 1.0595, that seven semitones approximate the perfect fifth 3/2, and that twelve steps close the circle of fifths because (3/2)^12 ≈ 2^7. The upstream definition in MusicTheory.CircleOfFifths supplies the identical constant, ensuring the value is shared between the music-theory and aesthetics layers.
proof idea
The definition is a direct assignment of the natural number twelve. It functions as a one-line wrapper that supplies the constant to all downstream theorems.
why it matters in Recognition Science
This constant anchors the φ-derived derivation of the twelve-tone scale. It is invoked by the theorem twelve_from_phi to recover the approximation 12 ≈ φ^5 and by scale_fibonacci to obtain the Fibonacci relation 5 + 7 = 12. The module situates the value inside the optimization of consonance and closure under φ-scaling, consistent with the eight-tick octave structure of the Recognition framework.
scope and limits
- Does not derive the integer twelve from the forcing chain or J-uniqueness.
- Does not prove that twelve is the unique optimal scale size.
- Does not treat alternative scale cardinalities such as 5, 7, 19 or 31.
Lean usage
theorem twelve_from_phi : semitonesPerOctave = 12 := rflformal statement (Lean)
40def semitonesPerOctave : ℕ := 12
proof body
Definition body.
41
42/-- Semitone frequency ratio: 2^(1/12). -/