rsModesPerOctave
plain-language theorem explainer
Recognition Science sets the number of modes per octave to 8 to align musical intervals with the eight-tick octave period. Music theorists extending the framework to harmonic structures cite this constant when relating semitone counts to fifth ratios. The definition is a direct constant assignment with no lemmas or computation required.
Claim. Define the number of recognition modes per octave to be the natural number 8.
background
The CircleOfFifths module imports HarmonicModes and introduces rsModesPerOctave alongside semitonesPerOctave and fifth. This constant implements the eight-tick octave (period 2^3) from the forcing chain T7. The local setting treats musical intervals as instances of the Recognition Composition Law, with the Pythagorean comma arising as the discrepancy between 12 fifths and 7 octaves.
proof idea
The declaration is a direct constant definition that assigns the value 8. No tactics or upstream lemmas are invoked; the body is simply the numeral 8.
why it matters
This definition supplies the modal count required by modes_eq_8 and twelve_eight_ratio_is_fifth. It instantiates T7 of the unified forcing chain inside music theory, enabling the ratio (semitonesPerOctave : ℝ) / 8 = fifth and the subsequent comma calculations. The placement closes the link between the phi-ladder and equal-temperament approximations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.