pith. sign in
module module high

IndisputableMonolith.Aesthetics.MusicalScale

show as:
view Lean formalization →

The MusicalScale module in the Aesthetics domain defines constants and relations for musical intervals using RS-native quantities. Researchers studying links between the phi-ladder and harmonic structures would cite these definitions. The module contains only definitions and no theorems or proofs.

claimThe module defines semitonesPerOctave as the integer count of semitones in one octave, semitoneRatio as the corresponding frequency multiplier, perfectFifth and justFifth as specific interval ratios, phi_fifth_power as $\phi^5$, twelve_from_phi as the derivation of the 12-tone division from $\phi$, and related quantities such as circle_of_fifths_closure and pythagoreanComma.

background

The module sits in the Aesthetics domain and imports IndisputableMonolith.Constants, whose sole documented content is the definition of the fundamental RS time quantum $\tau_0 = 1$ tick. It introduces a collection of named constants that translate musical intervals into expressions involving the golden ratio $\phi$ and the eight-tick octave structure from the forcing chain. The sibling definitions include semitonesPerOctave (explicitly documented as the number of semitones in an octave), semitoneRatio, perfectFifth, justFifth, majorThird, justMajorThird, octave, phi_fifth_power, twelve_from_phi, circle_of_fifths_closure, and pythagoreanComma.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete musical-scale objects that realize the eight-tick octave (T7) in an aesthetic setting. No downstream theorems are listed in the used_by block, so the definitions remain available for later aesthetic or harmonic extensions of the Recognition framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)