IsClosedBridge
plain-language theorem explainer
A closed SI bridge is a triple of positive conversion factors (tick, voxel, coherence-mass) that simultaneously match SI values of c, ℏ, and G to the RS-native predictions. Uniqueness and closed-form proofs for the tick length cite this predicate as the full calibration hypothesis. The body is a pure three-way conjunction of the matching constraints; no proof work.
Claim. A bridge $b=(a_T,a_L,a_M)$ of strictly positive conversion factors (seconds per tick, metres per voxel, kilograms per coherence-mass) is closed when it satisfies all three matching constraints at once: $c_{\mathrm{SI}}=c_{\mathrm{RS}}\cdot a_L/a_T$, $\hbar_{\mathrm{SI}}=\hbar_{\mathrm{RS}}\cdot a_M\cdot a_L^2/a_T$, and $G_{\mathrm{SI}}=G_{\mathrm{RS}}\cdot a_L^3/(a_M\cdot a_T^2)$.
background
The module formalises the SI 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 native bridge identity $G\cdot\pi\cdot\hbar=\lambda_{\mathrm{rec}}^2\cdot c^3$ at $\lambda_{\mathrm{rec}}=\ell_0=1$.
An SI bridge is a structure of three strictly positive conversion factors: $a_T$ (seconds per tick), $a_L$ (metres per voxel), $a_M$ (kilograms per coherence-mass). Matching the RS predictions against the SI anchors yields three constraints. Under SI-2019, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact definitions; $G_{\mathrm{SI}}$ is the CODATA anchor for this particular bridge.
The three named constraints are: c-constraint $c_{\mathrm{SI}}=c_{\mathrm{RS}}\cdot a_L/a_T$; ℏ-constraint $\hbar_{\mathrm{SI}}=\hbar_{\mathrm{RS}}\cdot a_M\cdot a_L^2/a_T$; G-constraint $G_{\mathrm{SI}}=G_{\mathrm{RS}}\cdot a_L^3/(a_M\cdot a_T^2)$.
proof idea
Definitional abbreviation only. The predicate is the conjunction of the three already-defined matching constraints (c, ℏ, and G) applied to the same bridge. No tactics, no lemmas, no algebraic work.
why it matters
This is the hypothesis package for the module's main algebraic identity and headline theorem. Downstream, $a_T^2=\pi\cdot\hbar_{\mathrm{SI}}\cdot G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ (and its square-root form $a_T=\sqrt{\pi}\cdot\tau_{\mathrm{Planck}}$) are proved under a closed bridge; the master statement then asserts that every closed bridge has $\tau_0=\sqrt{\pi}\cdot\tau_{\mathrm{Planck}}$. The certificate structure packages those clauses for export.
In framework terms this closes the SI conversion-map frontier once the dimensional anchor is supplied: the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ fix the dimensionless skeleton, and the three constraints uniquely determine the tick length. The module does not predict $G_{\mathrm{SI}}$; it only calibrates under the measured anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.