to_kg
plain-language theorem explainer
Defines the conversion from RS-native mass (in coh/c²) to kilograms by scaling with the joules-per-coherence factor from an external calibration and dividing by the square of the SI speed of light. Physicists translating Recognition Science mass predictions to laboratory values would cite this definition. The implementation is a direct one-line algebraic expression with no lemmas or case analysis.
Claim. Let $cal$ be an external calibration supplying the energy of one coherence quantum in joules. For a mass $m$ expressed in coherence quanta per $c^2$, the mass in kilograms equals $m$ times joules_per_coh of $cal$, divided by $(299792458)^2$.
background
The RSNativeUnits module establishes a native measurement system with tick as the fundamental time quantum (one ledger posting interval), voxel as the corresponding length quantum, coh as the coherence energy quantum fixed at phi^{-5}, and act as the action quantum. Mass is introduced as an abbreviation for the real numbers, with values understood in units of coh/c² under the internal convention c=1. ExternalCalibration is the structure that supplies the three positive real conversion factors (seconds per tick, meters per voxel, joules per coh) needed to anchor RS quantities to SI units.
proof idea
This definition is a one-line wrapper that directly multiplies the input mass by the joules_per_coh field of the supplied ExternalCalibration and divides by the square of the numerical SI speed of light.
why it matters
The definition supplies the explicit SI bridge for mass within the RS-native unit system, allowing all derived quantities (energy, momentum, etc.) to remain internally consistent with c=1 and the phi-ladder while still permitting numerical comparison with experiment. It implements the module's stated policy that SI conversion is optional and explicit, supporting the broader claim that physics can be expressed entirely in tick/voxel/coh/act units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.