Pitch math

Equal temperament, cents and octave folding, with a Lean proof that octave folding is unique.

Repository
pitch-math on GitHub
Cite
doi:10.5281/zenodo.24035856 (all versions, via Zenodo)
Layer
Layer 0
Licence
Apache-2.0
Status
released

Claims

ClaimLevelStatementEvidence
pitch:ET-A4 v1.0.0 P In equal temperament, MIDI note 69 (A4) is 440 Hz.
pitch:ET-OCTAVE v1.0.0 P Twelve equal-tempered semitones up doubles the frequency: midiToHz(m + 12) = 2 · midiToHz(m) for every real m.
pitch:CENTS-OCTAVE v1.0.0 P An octave is 1200 cents: cents(f, 2f) = 1200 for every f > 0.
pitch:CENTS-ADDITIVE v1.0.0 P Cents add up: for a, b, c > 0, the interval from a to c is the interval from a to b plus the interval from b to c.
pitch:OCTAVE-FOLD-UNIQUE v1.0.0 P For every f > 0 and a > 0 there is exactly one integer n with a ≤ f·2^n < 2a, so folding a frequency into an octave is well defined.
pitch:OCTAVE-TRANSPOSE-RATIOS v1.0.0 P Moving two frequencies by the same number of octaves leaves their ratio unchanged.
pitch:HARMONIC-OCTAVE-IFF-POW2 v1.0.0 P For f0 > 0, the N-th harmonic N·f0 is a whole number of octaves above f0 (2^k·f0 for some natural k) exactly when N is a power of two.
pitch:TEN-MINUTE-RHYTHM-PITCH v1.0.0 P A rhythm with a 10-minute (600 s) period, raised 18 octaves, is exactly 32768/75 Hz: (1/600)·2^18 = 32768/75 ≈ 436.91 Hz.
pitch:ET-FORMULA v1.0.0 T midi_to_hz(m) computes a4·2^((m − 69)/12) and hz_to_midi computes 69 + 12·log2(hz/440), within 1e-12 relative of the reference implementation, and they invert each other.
pitch:ET-LOW-NOTES v1.0.0 T With A4 = 440 Hz, the equal-tempered notes E0, A0, E1 and F1 (MIDI 16, 21, 28, 29) are 20.6017, 27.5, 41.2034 and 43.6535 Hz, which round to the two-decimal values 20.60, 27.50, 41.20 and 43.65 Hz quoted in the project's earlier draft.
  • Uses: pitch:ET-FORMULA@1
pitch:NOTE-NAMES v1.0.0 T note_name spells notes with sharps and numbers octaves with C4 = MIDI 60 (69 → A4, 61 → C#4, 0 → C-1); nearest_note returns the nearest note and an offset in [-50, 50) cents, rounding exact halves up.
pitch:OCTAVE-FOLD-EXACT v1.0.0 T octave_fold(hz, low) returns the unique n of pitch:OCTAVE-FOLD-UNIQUE and hz·2^n, and low ≤ hz·2^n < 2·low holds exactly in floating point, including at exact powers of two and at the ends of the f64 range.
  • Uses: pitch:OCTAVE-FOLD-UNIQUE@1
pitch:TEN-MINUTE-RHYTHM-NOTE v1.0.0 T A 10-minute rhythm (1/600 Hz) folds into [220, 440) Hz after exactly 18 octaves, at 436.907 Hz, which is the note A4 minus 12.21 cents.
  • Uses: pitch:TEN-MINUTE-RHYTHM-PITCH@1pitch:OCTAVE-FOLD-UNIQUE@1
pitch:CIRCADIAN-RHYTHM-NOTE v1.0.0 T A 24-hour rhythm (1/86400 Hz) folds into [220, 440) Hz after exactly 25 octaves, at 388.36 Hz (262144/675 Hz), which is the note G4 minus 16.12 cents.
  • Uses: pitch:OCTAVE-FOLD-UNIQUE@1
pitch:INPUT-VALIDATION v2.0.0 T Every function rejects frequencies that are zero, negative, NaN or infinite, harmonic numbers below 1, a fold octave outside the normal f64 range, and results that overflow or underflow; Python raises ValueError and JavaScript throws an Error. In JavaScript the whole-number arguments of note_name, octave_transpose, harmonic and is_octave_harmonic must be whole numbers of at least -2^63 and less than 2^63 (the largest is 2^63 - 1024), so a fraction, NaN, an infinity or a number outside that range throws instead of being truncated or wrapped.

Depends on

Used by

Posts about this repo

No posts about this repo yet.