c_SI
The definition assigns the exact 2019 SI value to the speed of light in vacuum. Metrologists and cosmologists reference it for converting between native units and measured quantities. Implementation occurs through direct numerical assignment without further reduction.
claimThe speed of light in vacuum equals $c = 299792458$ m/s, the exact value fixed by the 2019 SI redefinition.
background
This module serves as the quarantined repository for all empirical calibration data entering from external sources. The core Recognition Science derivation proceeds from the Recognition Composition Law without reference to measured constants. The present definition supplies the SI value of the speed of light for use in conversion routines and calibration certificates. In RS-native units the speed equals the ratio of fundamental length to fundamental time, with the numerical SI value obtained by calibration.
proof idea
The declaration consists of a direct noncomputable assignment of the integer 299792458 to the real number representing the speed of light.
why it matters in Recognition Science
This anchor feeds the positivity lemma and the SI calibration certificate in Cosmology.SIConversion. It maintains separation between the pure cost-first derivation and laboratory comparison. The value supports the eight-tick octave and dimensional analysis within the T0 to T8 forcing chain.
scope and limits
- Does not compute the value from the Recognition Composition Law.
- Does not enter the cost-first core modules.
- Does not include measurement uncertainty.
- Does not define related constants such as Planck's constant.
formal statement (Lean)
67@[simp]
68noncomputable def c_SI : ℝ := 299792458
proof body
Definition body.
69
70/-- **EXTERNAL ANCHOR**: Reduced Planck constant (exact, SI 2019 definition).
71 ℏ = 1.054571817... × 10⁻³⁴ J·s -/