Chethan D V

Rhythm units

Period, frequency and bpm conversions, with Lean proofs of the time-scaling theorem.

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

Claims

ClaimLevelStatementEvidence
rhythm:FREQ-PERIOD-INVERSE v1.0.0 P Frequency and period are inverses: converting a period to a frequency and back returns the original period.
rhythm:FREQ-POSITIVE v1.0.0 P A positive period always has a positive frequency.
rhythm:BPM-HZ-INVERSE v1.0.0 P Beats per minute and hertz convert into each other without loss (bpm = 60 × f).
rhythm:MINUTES-AS-SECONDS v1.0.0 P A period of m minutes is the same rhythm as a period of 60 × m seconds.
rhythm:TIME-SCALING-PERIODIC v1.0.0 P If a signal repeats every T, the same signal sped up by a factor k repeats every T / k.
rhythm:TIME-SCALING-FREQUENCY v1.0.0 P Speeding time up by a factor k multiplies every frequency by k.
rhythm:SCALE-RATIO-INVARIANT v1.0.0 P Speeding time up by any non-zero factor leaves the ratio between any two frequencies unchanged.
rhythm:SPEEDUP-FOR v1.0.0 P For any non-zero starting frequency, speedup_for gives exactly the factor that turns it into the target frequency.
rhythm:TEN-MINUTES-HZ v1.0.0 P A rhythm with a 10-minute period has a frequency of exactly 1/600 Hz (about 1.67 mHz).
rhythm:TEN-MINUTES-SPED-UP-180 v1.0.0 P Sped up 180 times, a 10-minute rhythm has a frequency of exactly 0.3 Hz: one beat every 3⅓ seconds.
rhythm:IMPLEMENTATIONS-AGREE v1.0.0 T The Rust crate, the Python bindings and the WebAssembly bindings all match the exactly computed golden vectors to within a few units in the last place.
rhythm:INPUT-VALIDATION v1.0.0 T All three implementations reject inputs that are zero, negative or not finite, and results that would overflow.

Depends on

Used by

Posts about this repo

No posts about this repo yet.