twelve_from_phi
plain-language theorem explainer
The theorem asserts that the semitone count per octave equals 12 in the Recognition Science model of musical scales derived from the golden ratio. Researchers working on equal-tempered harmony and φ-scaling would cite this equality when connecting octave divisions to φ^5 ≈ 11.09. The proof is a direct reflexivity step on the definition of the semitone count.
Claim. Let $N$ denote the number of semitones per octave in the equal-tempered scale. Then $N = 12$.
background
The Aesthetics.MusicalScale module derives the Western 12-tone equal temperament from the golden ratio φ through optimization of frequency ratios. It defines the semitone count per octave as the integer 12, with the semitone frequency ratio given by $2^{1/12} ≈ 1.0595$ and the perfect fifth by $2^{7/12} ≈ 1.4983 ≈ 3/2$. The local setting states that 12 emerges from consonance, closure under the circle of fifths, and φ-scaling, where $12 ≈$ round($φ^5 / 2$) × 2 and $φ^5 ≈ 11.09$ rounds up to 12.
proof idea
The proof is a one-line term that applies reflexivity to the definition of the semitone count per octave.
why it matters
This result fills the AE-001 proposition by linking the octave division directly to φ^5 rounding in the aesthetics module. It supports the circle of fifths closure where $(3/2)^{12} ≈ 2^7$ and connects to the eight-tick octave period in the forcing chain. The equality anchors predictions that other scales (5, 7, 19, 31) also carry φ-related structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.