to_meters
plain-language theorem explainer
This definition supplies the explicit map from a voxel quantity in the RS-native lattice to a real number of meters, using an externally provided calibration record. Researchers mapping recognition-based simulations to laboratory length scales would cite it when reporting native results in SI. The implementation reduces to a direct scalar multiplication after casting the voxel to real.
Claim. Let $cal$ be an external calibration record and $L$ a voxel quantity. Then $to_meters(cal, L) := L · cal.meters_per_voxel$, where the voxel value is interpreted as a real number.
background
The module supplies the explicit seam for reporting RS-native quantities in SI units while keeping the core theory free of CODATA numerals. ExternalCalibration is the structure holding seconds_per_tick, meters_per_voxel, and joules_per_coherence_quantum, all supplied from outside. Voxel is the abbreviation for Quantity VoxelUnit, the native length measure on the recognition lattice. The upstream definition in Constants.RSNativeUnits.to_meters performs the analogous conversion for the Length type.
proof idea
One-line definition that casts the voxel quantity to real and multiplies by the meters_per_voxel field of the calibration.
why it matters
It supplies the length-conversion bridge that measure_to_meters in the same module applies to Measurement Voxel objects. The construction preserves the framework rule that native theory and measurement catalogs remain independent of external constants, consistent with the separation of RS-native units from SI reporting. It touches the open question of how the calibration values themselves are fixed from recognition principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.