Pith. sign in
def

c_SI

definition
show as:
module
IndisputableMonolith.Foundation.SIBridgeClosure
domain
Foundation
line
90 · github
papers citing
none yet

plain-language theorem explainer

The SI speed of light is fixed at the exact integer 299792458 m/s under the 2019 SI redefinition. Anyone matching RS-native predictions (c_RS = 1) to laboratory units cites this external anchor in the dimensional bridge. It is a bare numeric definition with no proof obligations.

Claim. The SI speed of light is the exact constant $c_{\mathrm{SI}} = 299792458\,\mathrm{m/s}$ (SI 2019 definition).

background

The module SIBridgeClosure closes the conversion map from Recognition Science native units to SI. In RS-native units the framework predicts the dimensionless triple $c_{\mathrm{RS}} = 1$, $\hbar_{\mathrm{RS}} = \varphi^{-5}$, $G_{\mathrm{RS}} = \varphi^{5}/\pi$, together with the bridge identity $G\cdot\pi\cdot\hbar = \lambda_{\mathrm{rec}}^{2}\cdot c^{3}$ at $\lambda_{\mathrm{rec}} = 1$.

The SI bridge is three positive conversion factors $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/cohmass) constrained by matching those predictions to the SI values of $c$, $\hbar$, and $G$. Under SI-2019 conventions, $c$ and $\hbar$ are exact definitions; $G$ is the CODATA anchor. This constant supplies the SI side of the $c$-constraint $c_{\mathrm{SI}} = c_{\mathrm{RS}}\cdot a_L/a_T$.

proof idea

Bare numeric definition: the real literal 299792458, matching the exact SI-2019 value of the speed of light in metres per second. No lemmas, tactics, or algebraic reduction.

why it matters

This external anchor enters every SI-bridge identity in the module, in particular the uniqueness formula $a_T^{2} = \pi\cdot\hbar_{\mathrm{SI}}\cdot G_{\mathrm{SI}}/c_{\mathrm{SI}}^{5}$ (equivalently $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$). Downstream consumers include positivity lemmas, the calibrated tick square (with variable $G$ input), injectivity of that calibration in the supplied $G$, and SI-conversion certificates in cosmology. It imports the SI definition so the dimensional bridge closes uniquely once $G$ is supplied; it does not predict $c$ from RS axioms. Framework landmark: native $c_{\mathrm{RS}} = 1$ is matched against this SI value.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.