to_hertz
plain-language theorem explainer
Frequency expressed in inverse ticks converts to hertz by dividing the input value by the seconds-per-tick factor supplied in the external calibration record. Researchers comparing Recognition Science spectra or decay rates to laboratory data would apply this scaling when reporting results in SI units. The definition performs a single real division that inherits positivity from the calibration structure.
Claim. The map sending frequency value $f$ (in inverse ticks) and calibration record $cal$ to the equivalent frequency in hertz is given by $f / cal.seconds_per_tick$, where $cal.seconds_per_tick$ denotes the real number of seconds per native time quantum.
background
The module establishes a Recognition-Science-native unit system whose base standards are the tick (one discrete ledger interval) and the voxel (distance light travels in one tick). Frequency is introduced simply as the real numbers, with the understanding that it counts cycles per tick. ExternalCalibration is the structure that supplies the three conversion factors needed to reach SI: seconds per tick, meters per voxel, and joules per coherence quantum, each accompanied by a positivity proof.
proof idea
The definition is a one-line wrapper that extracts the seconds_per_tick field from the supplied calibration record and performs ordinary real division on the frequency argument.
why it matters
The conversion completes the optional SI interface described in the module documentation, allowing any RS-native frequency (including those arising from the phi-ladder or J-cost calculations) to be expressed in hertz while the internal relations c=1 and phi-based scaling remain untouched. It therefore supports direct numerical comparison with experimental frequencies without altering the ledger primitives or the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.