siBridgeClosureCert_inhabited
plain-language theorem explainer
The SI bridge calibration certificate is inhabited: a concrete witness packages uniqueness of the tick conversion, the closed form τ₀ = √π · τ_Planck, positivity checks, and the native Planck identity. Anyone citing SI-unit closure of the RS dimensional bridge can point here. The proof is a one-line term that exhibits the prebuilt certificate record.
Claim. The type of SI bridge calibration certificates is nonempty: there exists a record whose clauses assert that every closed SI bridge $b$ satisfies $b.a_T^2 = \pi \, \hbar_{\mathrm{SI}} G_{\mathrm{SI}} / c_{\mathrm{SI}}^5$ and $b.a_T = \sqrt{\pi}\,\tau_{\mathrm{Planck}}$, together with $\tau_{\mathrm{Planck}} > 0$, predicted $\tau_0 > 0$, and the native identity $\hbar_{\mathrm{RS}} G_{\mathrm{RS}}$ matching the recognition/Planck bridge.
background
This module closes the SI conversion map from RS-native units to SI. In RS-native units the framework fixes the dimensionless triple $c_{\mathrm{RS}} = 1$, $\hbar_{\mathrm{RS}} = \varphi^{-5}$, $G_{\mathrm{RS}} = \varphi^5/\pi$, with the recognition/Planck identity $G\pi\hbar = \lambda_{\mathrm{rec}}^2 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 $c$, $\hbar$, $G$ between gauges. Under SI-2019, $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact; $G_{\mathrm{SI}}$ is the CODATA anchor. The certificate structure packages five clauses: uniqueness of $a_T^2$, the closed form $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$, positivity of Planck time and of calibrated $\tau_0$, and the native Planck identity.
Upstream, siBridgeClosureCert is the concrete record filling those fields with the proved identities $a_T^2$ uniqueness, $\tau_0$ closed form, and positivity lemmas.
proof idea
One-line term proof. The goal is Nonempty SIBridgeClosureCert. The witness is the already-constructed definition siBridgeClosureCert, introduced via anonymous constructor ⟨siBridgeClosureCert⟩. No further rewriting: inhabitance follows immediately from the packaged certificate whose fields are the module's main uniqueness and positivity theorems.
why it matters
This is the inhabitance seal on the SI bridge closure certificate: the structural theorem that the dimensional conversion map is uniquely determined once the SI anchor is supplied. Module status is structural (0 sorry, 0 RS-internal axiom). It packages the main results $a_T^2 = \pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ and $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$, tying the RS-native constants $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^5/\pi$ to SI units.
No downstream dependents are recorded yet; the declaration exists so external consumers can require Nonempty SIBridgeClosureCert rather than name individual lemmas. It does not predict $G_{\mathrm{SI}}$; it only closes uniqueness of the calibration given that measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.