to_joules
plain-language theorem explainer
Physicists using Recognition Science models cite this definition when converting native coherence energies to SI joules for reporting. It accepts an ExternalCalibration record and a Coh value, returning their product with the joules_per_coh factor. The implementation is a direct scalar multiplication that serves as the explicit seam between RS-native units and laboratory measurements.
Claim. Given an external calibration record $cal$ and coherence energy $E$, the equivalent energy in joules is $E$ times $cal.joules_per_coh$.
background
This module supplies the explicit adapter for reporting RS-native quantities in SI units. The module documentation states that RS-native theory and measurement catalogs must not depend on CODATA numerals, with SI conversion occurring only through an explicit ExternalCalibration record supplied externally. The ExternalCalibration structure holds the conversion factors seconds_per_tick, meters_per_voxel, and joules_per_coh. Upstream, Constants.tick defines the fundamental RS time quantum as τ₀ = 1, and a parallel to_joules definition exists in RSNativeUnits for the Energy type.
proof idea
The definition implements the conversion by direct multiplication of the input coherence energy (cast to ℝ) by the joules_per_coh field of the supplied calibration record. It is a one-line wrapper that applies the external scaling factor.
why it matters
This definition supports downstream functions such as measure_to_joules, which applies the conversion to Measurement Coh objects while propagating scaled uncertainty. It realizes the required calibration seam in the RS framework, preserving independence of the native derivation (forcing chain T0-T8, Recognition Composition Law, ħ = φ^{-5}) from empirical SI reporting. It touches the question of how calibration constants are fixed without introducing circularity into the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.