a_T_eq
plain-language theorem explainer
Under a closed SI bridge (c, ℏ, G constraints matched), the seconds-per-tick factor equals √(π ℏ_SI G_SI / c_SI⁵). Calibration and Planck-time comparisons cite this identity. Proof: take the nonnegative square root of the already-proved squared form.
Claim. Let $b$ be an SI bridge (positive factors $a_T$, $a_L$, $a_M$ converting ticks, voxels, and coherence-mass into seconds, metres, and kilograms). If $b$ satisfies the three matching constraints for $c$, $\hbar$, and $G$, then $a_T = \sqrt{\pi \, \hbar_{\mathrm{SI}} \, G_{\mathrm{SI}} / c_{\mathrm{SI}}^5}$.
background
The SI Bridge Closure module fixes the unique conversion 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$, together with the native identity $G\pi\hbar=\lambda_{\mathrm{rec}}^2 c^3$ at $\lambda_{\mathrm{rec}}=1$. The bridge is three positive scales: $a_T$ (seconds per tick), $a_L$ (metres per voxel), $a_M$ (kilograms per coherence-mass).
Closure means the three SI-matching constraints hold: $c_{\mathrm{SI}}=c_{\mathrm{RS}},a_L/a_T$, $\hbar_{\mathrm{SI}}=\hbar_{\mathrm{RS}},a_M a_L^2/a_T$, and $G_{\mathrm{SI}}=G_{\mathrm{RS}},a_L^3/(a_M a_T^2)$. Here $c_{\mathrm{SI}}$ and $\hbar_{\mathrm{SI}}$ are exact SI-2019 anchors; $G_{\mathrm{SI}}$ is the CODATA measurement that pins this bridge.
The upstream main algebraic identity already gives $a_T^2=\pi,\hbar_{\mathrm{SI}},G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ by multiplying the helper products $(a_M a_T)\cdot(a_T/a_M)$ and using $\hbar_{\mathrm{RS}}G_{\mathrm{RS}}=1/\pi$. This declaration extracts the positive root.
proof idea
Invoke the squared identity: under a closed bridge, $a_T^2=\pi,\hbar_{\mathrm{SI}},G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$. Positivity of the tick factor supplies $0\le a_T$, so $\sqrt{a_T^2}=a_T$. Rewrite the goal by replacing $a_T$ with that square root and substitute the squared identity. No further constraint algebra is needed; the work is pure real-analysis bookkeeping on the nonnegative root.
why it matters
This is the last algebraic step before the module headline: $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$ under the calibrated bridge. The downstream theorem rewrites the present identity against the definition of Planck time and factors $\sqrt{\pi}$ out front.
In the Recognition framework the result closes the SI conversion frontier: once the dimensional anchor $G_{\mathrm{SI}}$ is supplied, the tick (and then voxel and coherence-mass) factors are uniquely fixed. It realises the native RS constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ as a concrete map into laboratory units, without predicting the measured value of $G$ itself. Structural status is full: zero sorry, zero RS-internal axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.