semitones_eq_12
plain-language theorem explainer
The declaration asserts that the semitone count per octave equals twelve in the CircleOfFifths module. Music theorists extending Recognition Science to harmonic structures would reference this equality when fixing the twelve-tone division for mode and fifth calculations. The proof is a direct reflexivity step that follows from the constant definition of the quantity.
Claim. The number of semitones in an octave equals 12.
background
The CircleOfFifths module imports HarmonicModes and defines semitonesPerOctave as the natural number 12, matching the upstream definition in MusicalScale that counts semitones in an octave. This assignment fixes the standard division used for interval ratios and mode structures. The theorem simply records the equality to this constant.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of semitonesPerOctave as 12.
why it matters
This equality anchors the twelve-tone scale inside the music-theory layer of Recognition Science and supports later statements on fifths and modes within the same module. It aligns with the eight-tick octave from the forcing chain (T7) but does not derive the number from the J-function or phi-ladder. No downstream theorems cite it directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.