to_joules
plain-language theorem explainer
The definition converts an energy value expressed in coherence quanta to joules by scaling with the joules_per_coh factor from an ExternalCalibration. Researchers bridging RS-native calculations to SI data would cite it when mapping ledger-based energies. The implementation is a direct multiplication by the calibration field.
Claim. Given an external calibration structure $cal$ and energy $E$ in coherence quanta, the value in joules is $E$ times the joules per coherence quantum of $cal$.
background
The RSNativeUnits module defines a native unit system with tick as the atomic time interval, voxel as the spatial step, and coherence quantum (coh) as the base energy unit equal to phi to the minus five. ExternalCalibration is the structure carrying explicit SI conversion factors, including joules_per_coh together with positivity conditions on the time and length factors. Energy is simply the real numbers, allowing direct arithmetic once the calibration is supplied.
proof idea
This is a one-line definition that multiplies the input Energy by the joules_per_coh component of the supplied ExternalCalibration.
why it matters
It supplies the energy leg of the optional SI bridge used by measure_to_joules and the sibling to_joules in the SI calibration module. The definition realizes the module's stated policy of keeping core physics in native units (c equals 1, phi-ladder scaling) while exposing a single explicit factor for experimental comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.