modes_eq_8
plain-language theorem explainer
Recognition Science fixes the number of modes per octave at eight via the eight-tick octave structure. Modal theorists or phi-ladder analysts would cite this when deriving scale families from the Recognition Composition Law and T7. The proof is a one-line reflexivity on the definition of rsModesPerOctave.
Claim. In the Recognition Science framework the number of modes per octave equals eight: $rsModesPerOctave = 8$.
background
The CircleOfFifths module encodes octave and fifth relations inside the Recognition Science music theory layer, importing HarmonicModes for the underlying scale definitions. rsModesPerOctave is the RS-native count of modes, set by the T7 eight-tick octave (period $2^3$). Upstream results supply parallel eight-element or seven-element enumerations (kinship systems, plot families, ore classes) that illustrate the same octal pattern across domains.
proof idea
The proof is a one-line reflexivity that applies rfl directly to the definition of rsModesPerOctave.
why it matters
The equality anchors the music-theoretic sector to the eight-tick octave landmark (T7) in the forcing chain. It supplies the modal count required for downstream phi-ladder constructions such as ModalPreferenceFromPhi and the Circle of Fifths relations. No used-by edges are recorded, leaving open whether further theorems will invoke it for comma calculations or temperament derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.