SIBridgeClosureCert
plain-language theorem explainer
Certificate packing five clauses that close the SI conversion map: any bridge matching c, ℏ, G has squared tick factor fixed as π ℏ_SI G_SI / c_SI⁵, hence a_T = √π · τ_Planck, with positivity and the native Planck identity ℏ_RS G_RS = 1/π. Anyone citing uniqueness of the tick-to-seconds calibration uses this bundle. It is a pure structure; the verified instance fills each field from prior lemmas.
Claim. A certificate asserting: for every SI bridge (positive factors $a_T$, $a_L$, $a_M$) that satisfies the three matching constraints against SI $c$, $\hbar$, $G$, one has $a_T^2 = \pi \, \hbar_{\mathrm{SI}} G_{\mathrm{SI}} / c_{\mathrm{SI}}^5$ and therefore $a_T = \sqrt{\pi}\,\tau_{\mathrm{Planck}}$; that $\tau_{\mathrm{Planck}} > 0$ and the calibrated $\tau_0$ in seconds is positive; and that the RS-native identity $\hbar_{\mathrm{RS}} G_{\mathrm{RS}} = 1/\pi$ holds.
background
Recognition Science predicts the dimensionless triple $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^5/\pi$ in native units, together with the bridge identity $G\pi\hbar=\lambda_{\mathrm{rec}}^2 c^3$ at $\lambda_{\mathrm{rec}}=\ell_0=1$. Laboratory display needs three positive conversion factors: $a_T$ (seconds per tick), $a_L$ (metres per voxel), $a_M$ (kilograms per coherence-mass).
Matching against SI values yields the 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)$. Under SI-2019, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact definitions; $G_{\mathrm{SI}}$ is the single CODATA anchor. A closed bridge is one that meets all three constraints.
This module's structural theorem is that those constraints uniquely fix $a_T^2=\pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$, i.e. $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$, with no further free dimensionless parameter.
proof idea
No proof body: this is a certificate structure. Each field is a named Prop that a later instance must supply. The verified witness siBridgeClosureCert assigns: squared-factor uniqueness from a_T_sq_eq; closed form from tau0_eq_sqrt_pi_planck_time; positivity from tau_Planck_pos and tau0_predicted_seconds_pos; native identity from hbar_RS_mul_G_RS. Inhabitation is then the one-line ⟨siBridgeClosureCert⟩.
why it matters
Closes the named open frontier of the dimensional bridge: once the SI anchor $G_{\mathrm{SI}}$ is supplied, tick, voxel, and coherence-mass factors are uniquely determined. Downstream, siBridgeClosureCert is the concrete verified instance, and siBridgeClosureCert_inhabited records that the certificate type is nonempty.
Framework landmarks: RS-native $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ (primer constants), and the Planck identity $\hbar_{\mathrm{RS}} G_{\mathrm{RS}}=1/\pi$ that forces the $\sqrt{\pi}$ factor in $\tau_0$. The certificate makes explicit that the theory carries zero free dimensionless SI parameters and only one dimensional display anchor, as any pure-number theory must when mapped to laboratory units. It does not claim a first-principles prediction of the numerical value of $G$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.