IndisputableMonolith.MusicTheory.CircleOfFifths
The CircleOfFifths module formalizes the musical circle of fifths inside Recognition Science by fixing 12 semitones and 8 modes per octave and defining the fifth interval together with its comma defects. Researchers working on harmonic embeddings of the eight-tick octave or on RS-derived scales would cite these definitions when linking T7 to concrete pitch systems. The module is built as a sequence of constant definitions followed by elementary lemmas that verify interval arithmetic and sign of the pythagorean comma.
claimThe module introduces the constants semitonesPerOctave = 12, rsModesPerOctave = 8 and the fifth interval $f$ satisfying the relation twelve_eight_ratio_is_fifth together with the positive defect pythagorean_comma = $(3/2)^{12}/2^{7} > 0$.
background
This module sits inside the MusicTheory domain and imports HarmonicModes, which supplies the underlying mode-counting structure tied to the eight-tick octave of Recognition Science. It adopts the J-cost function from the parent framework to measure interval defects and uses the phi-ladder to place musical ratios on the same scale as physical constants. The local setting therefore treats the octave as the period-8 recognition unit (T7) and the fifth as the generator whose twelve-fold repetition produces a small positive overshoot relative to seven octaves.
proof idea
This is a definition module, no proofs. It consists of constant declarations for semitonesPerOctave, rsModesPerOctave and fifth, followed by direct algebraic lemmas (twelve_eight_ratio_is_fifth, pythagorean_comma_positive, twelve_fifths_overshoot) that are discharged by arithmetic simplification and the imported HarmonicModes facts.
why it matters in Recognition Science
The module supplies the concrete musical realization of the eight-tick octave (T7) and thereby feeds any downstream theorem that embeds harmonic modes into the Recognition Science forcing chain. It closes the gap between the abstract period-8 structure and the observed 12-semitone, 8-mode Western scale while keeping the pythagorean comma positive and small, consistent with the alpha-band constants of the framework.
scope and limits
- Does not derive the value 12 or 8 from the J-equation without the HarmonicModes import.
- Does not treat equal-tempered or other non-Pythagorean tunings.
- Does not prove closure of the circle under modulation in all keys.
- Does not connect the fifth cost to the fine-structure constant band.
depends on (1)
declarations in this module (13)
-
def
semitonesPerOctave -
def
rsModesPerOctave -
def
fifth -
theorem
twelve_eight_ratio_is_fifth -
theorem
semitones_eq_12 -
theorem
modes_eq_8 -
theorem
pythagorean_comma_positive -
theorem
pythagorean_comma_small -
theorem
seven_fifths_close_to_four_octaves -
theorem
twelve_fifths_overshoot -
theorem
fifth_cost_lt_octave_cost -
theorem
twelve_divides_lcm_structure -
theorem
fifth_fourth_product