tau_Planck_pos
plain-language theorem explainer
The SI Planck time built from the external anchors ℏ, G, and c is strictly positive. Anyone using the closed-form tick conversion τ₀ = √π · τ_Planck needs this fact to keep a_T in the positive reals. The argument is a short positivity chase: square root of a positive quotient of positive SI constants.
Claim. The SI Planck time $\tau_{\mathrm{Planck}} := \sqrt{\hbar_{\mathrm{SI}}\, G_{\mathrm{SI}} / c_{\mathrm{SI}}^{5}}$ satisfies $0 < \tau_{\mathrm{Planck}}$.
background
The SI Bridge Closure module fixes the unique calibration map from RS-native units to SI. RS predicts the dimensionless triple $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^{5}/\pi$. Matching against the SI values of $c$, $\hbar$, and $G$ determines three positive conversion factors $a_T$ (sec/tick), $a_L$ (m/voxel), and $a_M$ (kg/cohmass).
Under those constraints the module obtains $a_T^{2} = \pi,\hbar_{\mathrm{SI}},G_{\mathrm{SI}}/c_{\mathrm{SI}}^{5}$, equivalently $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$. Here $\tau_{\mathrm{Planck}}$ is the ordinary SI Planck time $\sqrt{\hbar G/c^{5}}$, assembled from the external anchors: $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ (exact under SI-2019) and $G_{\mathrm{SI}}$ (CODATA measurement).
Upstream positivity lemmas already record $0<c_{\mathrm{SI}}$, $0<\hbar_{\mathrm{SI}}$, and $0<G_{\mathrm{SI}}$ by direct numerical evaluation of those anchors.
proof idea
Unfold $\tau_{\mathrm{Planck}}$ to $\sqrt{\hbar_{\mathrm{SI}},G_{\mathrm{SI}}/c_{\mathrm{SI}}^{5}}$. Apply Real.sqrt_pos to reduce to positivity of the radicand. Split the quotient with div_pos: the numerator is the product of the upstream facts $0<\hbar_{\mathrm{SI}}$ and $0<G_{\mathrm{SI}}$; the denominator is $c_{\mathrm{SI}}^{5}$, positive by pow_pos on $0<c_{\mathrm{SI}}$. Term-mode, no nontrivial algebra.
why it matters
Positivity of $\tau_{\mathrm{Planck}}$ is a leaf obligation in the SI-bridge closure certificate: siBridgeClosureCert records it as tau_Planck_positive, alongside the closed form $a_T=\sqrt{\pi},\tau_{\mathrm{Planck}}$ and the native Planck identity $\hbar_{\mathrm{RS}},G_{\mathrm{RS}}$ matching. It is also the direct input to tau0_predicted_seconds_pos, which multiplies $\sqrt{\pi}$ by $\tau_{\mathrm{Planck}}$ to show the predicted tick length in seconds is positive.
In the broader framework this sits under the dimensional bridge, not the forcing chain T0–T8. The RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$ are already fixed; this lemma only guarantees that the SI-side Planck yardstick used to read them out is a positive real. It does not predict $G_{\mathrm{SI}}$; it consumes the CODATA anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.