IndisputableMonolith.MusicTheory.Rhythm
The MusicTheory.Rhythm module translates the eight-tick octave from Recognition Science into concrete musical definitions for tempos and subdivisions. It supplies Tempo instances at 120, 150, and 75 BPM together with frequency relations such as beat-is-2Hz and eighth-notes-per-measure. Researchers modeling discrete time in auditory physics or quantum-inspired music would cite these to anchor T7 in audible rhythms. The module consists entirely of definitions and direct equalities.
claimThe module defines $ticksPerCycle : ℕ$, $eight_{ticks}_{from}_{dimension}$ linking 8 ticks to $D=3$, the type $Tempo$, and instances $tempo_{120}$, $tempo_{150}$, $tempo_{75}$ satisfying $tempo_{120}·beat = 2$ Hz together with $eighth_{notes}_{per}_{measure}$ and $subdivisionLevels$.
background
Recognition Science places the eight-tick octave at T7 of the forcing chain, with period $2^3$ derived from spatial dimension $D=3$. This module sits in the MusicTheory subdomain and imports only Mathlib. It introduces $Tempo$ as a structure carrying beats-per-minute, concrete values $tempo_{120}$, $tempo_{150}$, $tempo_{75}$, and supporting lemmas that map each to frequency (e.g., $tempo_{120}·beat = 2$ Hz, $tempo_{150}·quarter_{triplet} = mode4$). $ticksPerCycle$ and $eight_{ticks}{from}{dimension}$ make the link to the upstream eight-tick structure explicit, while $subdivisionLevels$ organizes the rhythmic hierarchy.
proof idea
This is a definition module, no proofs. It consists of type definitions for Tempo, direct instance declarations for the three tempos, and simple equality lemmas that record the frequency and subdivision relations.
why it matters in Recognition Science
The module supplies the rhythmic layer that interprets T7 of the UnifiedForcingChain, providing the concrete objects needed to apply the eight-tick octave in auditory or discrete-time models. It feeds any downstream construction that requires musical realizations of the phi-ladder or RCL in the time domain.
scope and limits
- Does not derive the eight-tick count from the forcing chain.
- Does not prove any statements about harmony or consonance.
- Does not connect rhythms to mass formulas or the alpha band.
- Does not treat polyrhythms or continuous tempo variation.
declarations in this module (17)
-
def
ticksPerCycle -
theorem
eight_ticks_from_dimension -
theorem
eighth_notes_per_measure -
structure
Tempo -
def
tempo_120 -
def
tempo_150 -
def
tempo_75 -
theorem
tempo_120_beat_is_2Hz -
theorem
tempo_120_eighth_note_is_16Hz -
theorem
tempo_150_quarter_triplet_is_mode4 -
theorem
tempo_75_sixteenth_note_is_mode1 -
def
subdivisionLevels -
theorem
subdivision_is_binary -
def
swingRatio_triplet -
def
swingRatio_moderate -
theorem
swing_triplet_is_octave_ratio -
theorem
swing_moderate_is_fifth