twelve_eight_ratio_is_fifth
plain-language theorem explainer
The ratio of twelve semitones per octave to eight recognition modes per octave equals the perfect fifth frequency ratio of three halves. Music theorists applying Recognition Science to harmonic structure would cite this equality to anchor the circle of fifths. The proof is a one-line wrapper that reduces the numeric identity via simplification and normalization.
Claim. Let $s$ denote the number of semitones per octave and $m$ the number of recognition modes per octave. Then $s/m = 3/2$, where the perfect fifth is the frequency ratio $3/2$.
background
In the CircleOfFifths module, semitonesPerOctave is defined as the constant 12 and rsModesPerOctave as the constant 8. The fifth is defined as the real number 3/2. An upstream definition in MusicalScale supplies the same semitonesPerOctave value together with the semitone frequency ratio $2^{1/12}$. A parallel definition in HarmonicModes repeats the fifth as 3/2. The module comment identifies the ratio 12/8 as the central bridge that equates the two octave divisions to the perfect fifth.
proof idea
This is a one-line wrapper that applies the simp tactic to unfold the three constants, followed by norm_num to confirm the arithmetic identity 12/8 = 3/2.
why it matters
The theorem supplies the explicit numerical link required by the Circle of Fifths construction in Recognition Science music theory. It feeds downstream statements on the Pythagorean comma and mode counting that appear later in the same module. The equality aligns with the eight-tick octave (T7) of the forcing chain and the recognition composition law that governs self-similar frequency ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.