to_meters
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive or compute the meters_per_voxel value from RS axioms.
- Does not propagate uncertainty beyond the supplied scaleUncertainty helper.
- Does not extend to time, energy, or other unit conversions.
- Does not embed any specific numerical calibration constants.
formal statement (Lean)
28@[simp] noncomputable def to_meters (cal : ExternalCalibration) (L : Voxel) : ℝ :=
proof body
Definition body.
29 (L : ℝ) * cal.meters_per_voxel
30