semitonesPerOctave
plain-language theorem explainer
The definition fixes the number of semitones per octave at the constant 12. Music theorists and scale constructors cite it when deriving the 5 + 7 = 12 Fibonacci relation or when approximating φ^5 ≈ 11.09. The declaration is a direct constant assignment marked with the simp attribute.
Claim. The number of semitones per octave is defined to be the natural number 12.
background
In the CircleOfFifths module the constant is introduced after importing HarmonicModes and the MusicalScale module. The upstream definition states that this is the number of semitones in an octave and associates the semitone frequency ratio 2^{1/12}. The local setting therefore treats 12 as the fixed division of the octave for all subsequent circle-of-fifths and mode calculations.
proof idea
The declaration is a direct definition that assigns the literal value 12 and attaches the simp attribute so that the constant unfolds automatically in downstream simplifications.
why it matters
It supplies the base count for theorems such as scale_fibonacci (pentatonicSize + diatonicSize = semitonesPerOctave) and twelve_from_phi (linking the count to φ^5). Within the Recognition framework the definition anchors the twelve-tone division to the eight-tick octave structure and enables derivations of the circle of fifths, the Pythagorean comma, and the twelve-fifths-to-seven-octaves relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.