to_m_per_s
plain-language theorem explainer
The definition converts a velocity value in voxels per tick to meters per second by scaling with the ratio of meters per voxel to seconds per tick drawn from an external calibration structure. Researchers bridging Recognition Science native units to SI measurements cite it when establishing consistency of c = 1 with laboratory values. The implementation is a direct one-line multiplication by the calibration ratio.
Claim. For an external calibration structure with seconds per tick $τ_0 > 0$ and meters per voxel $ℓ_0 > 0$, the map sending velocity $v$ (in voxels per tick) to SI velocity is $v · (ℓ_0 / τ_0)$.
background
The RS-Native Measurement System module treats tick (τ₀) as the discrete ledger posting interval and voxel (ℓ₀) as the causal spatial step, with c = 1 in voxel/tick units. Velocity is the abbreviation for real numbers representing voxels per tick. ExternalCalibration is the structure supplying seconds_per_tick, meters_per_voxel, and joules_per_coh together with positivity proofs, allowing explicit mapping from ledger primitives to SI quantities.
proof idea
The definition is a one-line wrapper that multiplies the input velocity by the ratio of meters_per_voxel to seconds_per_tick taken from the calibration argument.
why it matters
This conversion feeds the theorem c_in_si establishing that the speed of light equals 299792458 m/s and the downstream result c_reports_exact showing that 1 voxel/tick reports exactly c_SI under derived calibration. It supplies the explicit bridge required by the framework where c = 1 holds in native units while supporting the phi-ladder scalings and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.