c_constraint
plain-language theorem explainer
The c-constraint equates the SI speed of light to the RS-native value scaled by a bridge's length-to-time conversion ratio. Anyone closing the dimensional map from Recognition Science units to SI cites it as the first matching condition among the three SI anchors. It is a pure propositional definition of that matching equation, not a derived equality.
Claim. For a bridge $b$ with positive factors $a_T$ (seconds per tick) and $a_L$ (metres per voxel), the c-constraint asserts $c_{\mathrm{SI}} = c_{\mathrm{RS}} \cdot (a_L / a_T)$, where $c_{\mathrm{SI}}$ is the exact SI-2019 speed of light and $c_{\mathrm{RS}} = 1$ in RS-native units.
background
Recognition Science predicts dimensionless constants in a native gauge: $c_{\mathrm{RS}} = 1$, $\hbar_{\mathrm{RS}} = \varphi^{-5}$, $G_{\mathrm{RS}} = \varphi^5/\pi$. The SI bridge is a triple of strictly positive conversion factors $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/coherence-mass) that translate those predictions into laboratory units.
Matching the SI value of $c$ against the native prediction yields the first of three constraints. Under SI-2019, $c_{\mathrm{SI}} = 299792458,\mathrm{m/s}$ is an exact definition (external anchor), not a measurement. The module treats the bridge as a structure of three positive reals and packages each matching equation as a proposition on that structure.
Local setting: SI Bridge Closure proves that once the dimensional anchors are fixed, the tick, voxel, and coherence-mass factors are uniquely determined. The c-constraint is the length/time leg of that uniqueness argument.
proof idea
Definitional, not a proof. The body is the single equation $c_{\mathrm{SI}} = c_{\mathrm{RS}} \cdot (a_L / a_T)$ as a Prop on an SIBridge. Downstream lemmas unfold this definition and substitute $c_{\mathrm{RS}} = 1$ (via one_mul) to solve for $a_L$ in terms of $a_T$.
why it matters
This is the first of the three matching conditions that define a closed SI bridge (IsClosedBridge requires the c-, $\hbar$-, and $G$-constraints jointly). From it alone one obtains $a_L = c_{\mathrm{SI}} \cdot a_T$ (aL_eq_of_c_constraint). Combined with the $\hbar$-constraint it yields $a_M a_T = \hbar_{\mathrm{SI}} / (\hbar_{\mathrm{RS}} c_{\mathrm{SI}}^2)$; combined with the $G$-constraint it yields $a_T / a_M = G_{\mathrm{SI}} / (G_{\mathrm{RS}} c_{\mathrm{SI}}^3)$.
Those ratios feed the module's main closure: $a_T^2 = \pi , \hbar_{\mathrm{SI}} G_{\mathrm{SI}} / c_{\mathrm{SI}}^5$, i.e. $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$. The native values $c_{\mathrm{RS}} = 1$, $\hbar_{\mathrm{RS}} = \varphi^{-5}$, $G_{\mathrm{RS}} = \varphi^5/\pi$ are the RS-unit landmarks from the primer. The module closes the conversion map; it does not predict $G_{\mathrm{SI}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.