c_SI
plain-language theorem explainer
The definition records the exact SI speed of light as 299792458 meters per second. Calibration protocols that convert RS-native tick and voxel quantities to laboratory units cite this anchor to fix the spatial scale from the internal c equals 1. It enters by direct numerical assignment of the 2019 SI exact value.
Claim. The speed of light in vacuum is defined as $c = 299792458$ m/s.
background
The Single-Anchor SI Calibration module supplies a concrete protocol for expressing RS-native results in SI units. RS theory runs internally with c set to 1 in tick and voxel units, so one empirical scalar (seconds per tick) is supplied while meters per voxel follows from the SI definition of c. This definition records that exact value directly. Upstream anchors in ExternalAnchors and Cosmology modules record the identical numerical constant to maintain cross-module consistency. The module doc states that meters_per_voxel is fixed by the SI definition of c as 299792458 m/s.
proof idea
The declaration is a direct definition that binds the real number c_SI to the integer 299792458. No lemmas or tactics are applied; the value is the hardcoded exact SI constant.
why it matters
The constant closes the calibration seam between RS-native units and SI reporting. It is referenced by the SICalibrationCert structure and by positivity and consistency theorems in Cosmology.SIConversion. Within the Recognition framework it supplies the external numerical value for c while the internal theory enforces c equals 1, linking the forcing chain to laboratory measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.