to_meters
plain-language theorem explainer
The definition converts a length expressed in voxels to meters by scaling with the meters-per-voxel factor supplied in an external calibration structure. Researchers translating Recognition Science native lengths into SI units for experimental comparison would cite it. The implementation is a direct multiplication by the calibration constant.
Claim. Let $cal$ be an external calibration structure supplying a positive meters-per-voxel factor $m$. For a length $L$ given in voxels the converted value equals $L$ times $m$.
background
The module establishes an RS-native unit system whose base standards are the ledger primitives: tick (one discrete posting interval, denoted τ₀) and voxel (one causal spatial step, the distance light travels in one tick). Derived quanta include the coherence quantum with energy φ⁻⁵ and the action quantum ħ equal to that energy times τ₀. All dimensionless ratios are fixed by φ alone, with c set to unity in voxel-per-tick units and lengths organized on the φ-ladder for natural scaling of masses, energies, times, and lengths. External calibration is a structure that maps these native units to SI by recording seconds per tick, meters per voxel, and joules per coherence quantum, each required to be positive. Length is the abbreviation for the real numbers when used to represent voxel counts.
proof idea
The definition is a one-line wrapper that multiplies the input length value by the meters_per_voxel field extracted from the supplied external calibration structure.
why it matters
It supplies the explicit SI length conversion that downstream measurement functions such as measure_to_meters rely on, thereby closing the optional anchoring path from native voxel counts to laboratory units. The declaration sits inside the RS-native constants module whose module documentation emphasizes that SI conversion remains external and optional while the core ledger primitives and φ-ladder remain the fixed standards. It directly supports the framework landmark that c equals 1 in voxel/tick units and that all physics can be expressed without external anchoring until calibration is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.