semitonesPerOctave
plain-language theorem explainer
The definition fixes the number of semitones per octave at twelve for equal-tempered scales derived from the golden ratio. Researchers tracing phi-based musical structures in Recognition Science cite this constant when establishing scale sizes or closure properties in the circle of fifths. The declaration is a direct constant assignment that mirrors the upstream definition without additional computation.
Claim. Define the number of semitones in one octave to be twelve: $N = 12$.
background
The module develops the twelve-tone equal temperament scale as emerging from optimization with the golden ratio phi. It records that twelve semitones satisfy $2^{1/12} approx 1.0595$, the perfect fifth at seven semitones approximates $3/2$, and twelve arises as round(phi^5 / 2). The upstream definition in CircleOfFifths supplies the identical constant, documented as the number of semitones in an octave.
proof idea
The declaration is a one-line constant assignment that sets the value directly to twelve and reuses the upstream definition from the CircleOfFifths module.
why it matters
This constant anchors downstream theorems including scale_fibonacci, which equates pentatonic plus diatonic sizes to twelve, and twelve_from_phi, which identifies twelve with the rounded value of phi^5. It implements the AE-001 observation that twelve semitones optimize consonance and phi-scaling, connecting to the eight-tick octave period in the forcing chain. The module leaves open whether other scale cardinalities admit equally tight phi relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.