SIBridge
plain-language theorem explainer
The SI bridge is the triple of strictly positive conversion factors from RS-native units into SI: seconds per tick, metres per voxel, and kilograms per coherence-mass. Anyone closing the dimensional map from the RS predictions c=1, ℏ=φ⁻⁵, G=φ⁵/π to laboratory c, ℏ, G cites this carrier. It is a plain structure definition (fields plus positivity witnesses), not a proved claim.
Claim. An SI bridge is a triple of strictly positive reals $(a_T, a_L, a_M)$, where $a_T$ is the number of seconds per tick, $a_L$ the number of metres per voxel, and $a_M$ the number of kilograms per coherence-mass.
background
Recognition Science works in a native gauge where the tick $\tau_0$ and voxel $\ell_0$ are set to 1, so $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, and $G_{\mathrm{RS}}=\varphi^5/\pi$. Laboratory comparison needs a dimensional bridge: three conversion factors that turn those native units into SI seconds, metres, and kilograms.
This module formalises that bridge and proves its uniqueness once the SI values of $c$, $\hbar$, and $G$ are matched. Under SI-2019, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact definitions; $G_{\mathrm{SI}}$ is the CODATA anchor. The three matching constraints are $c_{\mathrm{SI}}=c_{\mathrm{RS}},a_L/a_T$, $\hbar_{\mathrm{SI}}=\hbar_{\mathrm{RS}},a_M a_L^2/a_T$, and $G_{\mathrm{SI}}=G_{\mathrm{RS}},a_L^3/(a_M a_T^2)$.
Upstream constants supply the native tick and voxel (both 1 in RS units) and the certified real values used for $\varphi$-powers. The structure itself only packages the three positive factors; the constraints and uniqueness theorems live on top of it.
proof idea
No proof body: this is a structure declaration. It introduces three real fields (seconds per tick, metres per voxel, kilograms per coherence-mass) together with three positivity hypotheses. Downstream lemmas unfold the fields and use the positivity witnesses to discharge nonzero denominators when rearranging the $c$, $\hbar$, and $G$ constraints.
why it matters
This structure is the data carrier for the entire SI-bridge closure. Every constraint and uniqueness theorem in the module takes an SI bridge as its first argument: the $c$-constraint, the $\hbar$- and $G$-constraints, the derived identities $a_L=c_{\mathrm{SI}} a_T$ and $a_M a_T=\hbar_{\mathrm{SI}}/(\hbar_{\mathrm{RS}} c_{\mathrm{SI}}^2)$, and the main algebraic result $a_T^2=\pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ (equivalently $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$).
In the Recognition framework this closes the named open frontier of the dimensional bridge: once the dimensional anchor is supplied, the three conversion factors are uniquely determined. It does not invent new physics constants; it packages the map from the RS-native triple $(c,\hbar,G)=(1,\varphi^{-5},\varphi^5/\pi)$ into SI so that the uniqueness theorems can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.