c_SI_pos
plain-language theorem explainer
The lemma asserts that the SI-defined speed of light is strictly positive. Researchers constructing single-anchor calibrations from RS-native units to SI would cite it to guarantee that derived quantities such as meters_per_voxel remain positive. The claim is discharged by a one-line norm_num reduction on the explicit rational definition of c_SI.
Claim. $0 < 299792458$, where the right-hand side is the exact 2019 SI definition of the speed of light in meters per second.
background
The Single-Anchor SI Calibration module supplies a concrete protocol that converts RS-native tick/voxel/coh/act quantities into SI units using only one empirical scalar, seconds_per_tick. All other conversion factors are derived from the exact SI definitions of c and h. The local definition c_SI : ℝ := 299792458 is imported from ExternalAnchors and redeclared here for the calibration context.
proof idea
One-line wrapper that applies norm_num to the definition of c_SI, reducing the numerical inequality to a trivial fact.
why it matters
The result feeds externalCalibration_of_tau0_seconds, which builds the full ExternalCalibration record whose meters_per_voxel field is c_SI multiplied by the anchor. It supplies the positivity fact required by the single-anchor protocol described in the module doc, where c remains exactly 299792458 m/s while RS-native theory runs with c = 1. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.