siBridgeClosureCert
plain-language theorem explainer
Packages the five proved clauses of the SI bridge calibration certificate into one inhabited record: under the c, ℏ, G matching constraints, a_T² equals π·ℏ_SI·G_SI/c_SI⁵, hence the tick duration is √π times the Planck time, with positivity of both times and the native Planck identity ℏ_RS·G_RS=1/π. Anyone citing SI-unit uniqueness of the RS conversion map uses this bundle. Construction is a pure structure instance wiring five already-proved lemmas.
Claim. There exists a verified SI-bridge calibration certificate whose five clauses assert: for every closed bridge $b$, $b.a_T^2 = \pi\,\hbar_{\mathrm{SI}}\,G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ and $b.a_T = \sqrt{\pi}\,\tau_{\mathrm{Planck}}$; moreover $\tau_{\mathrm{Planck}}>0$, the predicted $\tau_0$ in seconds is positive, and $\hbar_{\mathrm{RS}}\,G_{\mathrm{RS}}=1/\pi$.
background
The module closes the SI conversion map from RS-native units to SI. In native units the framework fixes the dimensionless triple $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^5/\pi$, together with the recognition/Planck identity $G\cdot\pi\cdot\hbar=\lambda_{\mathrm{rec}}^2\cdot c^3$ at $\lambda_{\mathrm{rec}}=\ell_0=1$.
The bridge is three positive conversion factors $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/coherence-mass) constrained by matching SI values of $c$, $\hbar$, $G$. Under SI-2019, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact; $G_{\mathrm{SI}}$ is the CODATA anchor. The certificate structure records uniqueness of this calibration, not a prediction of $G$.
Upstream, a_T_sq_eq is the main algebraic identity obtained by multiplying the $(a_M a_T)$ and $(a_T/a_M)$ helpers and using $\hbar_{\mathrm{RS}} G_{\mathrm{RS}}=1/\pi$. The headline closed form is $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$.
proof idea
Pure structure instance: each field of SIBridgeClosureCert is filled by an existing theorem. a_T_sq_determined is a_T_sq_eq; tau0_closed_form is tau0_eq_sqrt_pi_planck_time; tau_Planck_positive is tau_Planck_pos; tau0_predicted_positive is tau0_predicted_seconds_pos; planck_identity is hbar_RS_mul_G_RS. No new reasoning; the def only assembles the five proofs into one certificate value.
why it matters
This is the inhabited witness that the SI bridge closure is complete: once the dimensional anchor is supplied, tick, voxel, and coherence-mass factors are uniquely fixed, with the structural identity $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$. Downstream, siBridgeClosureCert_inhabited simply packages nonemptiness of the certificate type from this value.
In the Recognition framework the native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ are the RS-side input; the certificate shows the SI conversion map is then forced with no free parameters beyond the CODATA $G$ anchor. It closes the named open frontier of the dimensional bridge (module status: structural theorem, 0 sorry). It does not touch the forcing chain T0–T8 or the mass ladder; those live upstream of the unit conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.