tau0_predicted_seconds_pos
plain-language theorem explainer
The predicted fundamental tick duration in seconds is strictly positive. Anyone assembling the SI bridge closure certificate cites this positivity side-condition. The proof unfolds the closed form √π · τ_Planck and multiplies the positivity of √π by the already-proved positivity of Planck time.
Claim. The predicted tick duration in seconds is positive: $0 < \tau_0^{\mathrm{pred}}$, where $\tau_0^{\mathrm{pred}} = \sqrt{\pi}\,\tau_{\mathrm{Planck}}$ and $\tau_{\mathrm{Planck}}$ is the SI Planck time built from $c_{\mathrm{SI}}$, $\hbar_{\mathrm{SI}}$, and $G_{\mathrm{SI}}$.
background
The SIBridgeClosure module fixes the unique conversion map from RS-native units to SI once a dimensional anchor is supplied. RS predicts 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\pi\hbar=\lambda_{\mathrm{rec}}^2 c^3$ at $\lambda_{\mathrm{rec}}=1$. The bridge is three positive factors $a_T$ (sec/tick), $a_L$ (m/voxel), $a_M$ (kg/cohmass) constrained by matching $c$, $\hbar$, and $G$.
Under those constraints the module obtains $a_T^2=\pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$, i.e. $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$. The quantity tau0_predicted_seconds is exactly that closed form in seconds; the present lemma only records its positivity. Upstream, tau_Planck_pos already shows the SI Planck time is positive from the positivity of the CODATA/SI anchors.
proof idea
One-line term proof after unfolding. Expand tau0_predicted_seconds to $\sqrt{\pi}\cdot\tau_{\mathrm{Planck}}$. Apply mul_pos to the product of two positive reals: Real.sqrt_pos on Real.pi_pos gives $0<\sqrt{\pi}$, and tau_Planck_pos gives $0<\tau_{\mathrm{Planck}}$. No further algebraic work.
why it matters
Feeds the field tau0_predicted_positive of siBridgeClosureCert, the master certificate that the SI conversion map is uniquely determined and that $a_T=\sqrt{\pi},\tau_{\mathrm{Planck}}$. The module status is structural theorem (0 sorry): this positivity side-condition is required so the certificate can assert a well-formed positive tick in seconds. It sits downstream of the closed-form identity $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$ and of the RS-native constants $c_{\mathrm{RS}}=1$, $\hbar_{\mathrm{RS}}=\varphi^{-5}$, $G_{\mathrm{RS}}=\varphi^5/\pi$. It does not itself predict $G_{\mathrm{SI}}$; CODATA $G$ remains the external dimensional anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.