c_in_si
plain-language theorem explainer
The theorem states that the RS-native speed of light, fixed at unity in voxel per tick, converts exactly to the SI value 299792458 m/s for any external calibration. Researchers anchoring RS-native units to laboratory standards would cite this when verifying numerical agreement with measured constants. The proof is a one-line simplification that unfolds the conversion definition and applies the calibration's speed-consistency field.
Claim. Let $cal$ be an external calibration. The SI conversion of the RS-native speed of light (equal to 1 voxel per tick) satisfies $to_m_per_s(cal, c) = 299792458$.
background
The RS Native Units module defines a measurement system whose base standards are the tick (atomic time quantum) and voxel (spatial step light traverses in one tick). In these units the speed of light is fixed at unity, all dimensionless ratios are determined by the golden ratio alone, and SI conversion is supplied optionally through an ExternalCalibration structure containing seconds_per_tick, meters_per_voxel, and a speed_consistent field. The function to_m_per_s multiplies a velocity by the ratio meters_per_voxel over seconds_per_tick.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definition of to_m_per_s, substitutes the RS-native value of c (equal to 1), and applies the speed_consistent field of the supplied calibration to obtain the exact SI number 299792458.
why it matters
This result is invoked by the downstream theorem c_reports_exact in the SingleAnchor calibration module, which states that under a derived calibration certificate the RS speed of light reports exactly the SI value. It closes the loop between the native unit system (where c = 1) and laboratory standards, supporting the framework claim that all physics can be expressed in tick/voxel units with optional SI anchoring. It touches the fixed value of c in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.