c_RS_pos

The SI Bridge Closure module fixes the unique conversion from Recognition Science native units to SI. In the native gauge one sets $\ell_0 = \tau_0 = 1$, so the speed of light is the pure number $c_{\mathrm{RS}} = \ell_0/\tau_0 = 1$. The companion native constants are $\hbar_{\mathrm{RS}} = \varphi^{-5}$ and $G_{\mathrm{RS}} = \varphi^5/\pi$, matching the primer values $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$.

Three positive conversion factors $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/coherence-mass) are constrained by matching the SI values of $c$, $\hbar$, and $G$. Positivity of each native constant is a prerequisite for those factors to be well-defined and positive. The local definition is simply c_RS := 1; the same native value appears in the propagation-speed ledger setting.

One-line tactic proof: unfold the definition $c_{\mathrm{RS}} = 1$, then norm_num closes $0 < 1$. No lemmas are required.

Positivity of the native speed of light is part of the structural SI-bridge package that closes the dimensional conversion map (module status: 0 sorry, unique calibration). It sits beside the companion facts $0 < \hbar_{\mathrm{RS}}$ and $0 < G_{\mathrm{RS}}$ and feeds any argument that multiplies or divides by $c_{\mathrm{RS}}$ when solving the three matching constraints $c_{\mathrm{SI}} = c_{\mathrm{RS}}, a_L/a_T$, $\hbar_{\mathrm{SI}} = \hbar_{\mathrm{RS}}, a_M a_L^2/a_T$, $G_{\mathrm{SI}} = G_{\mathrm{RS}}, a_L^3/(a_M a_T^2)$. Those constraints yield the closed form $a_T^2 = \pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$, i.e. $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$. The result is elementary but mandatory infrastructure for the uniqueness theorem of the bridge; it does not itself predict the SI value of $G$.