phi_pow_5_pos

Recognition Science fixes the dimensionless native constants $c_{\mathrm{RS}} = 1$, $\hbar_{\mathrm{RS}} = \varphi^{-5}$, and $G_{\mathrm{RS}} = \varphi^5/\pi$. Here $\varphi$ is the unique positive self-similar fixed point of the J-cost (forcing chain T6), and the $\pm 5$ exponents encode the native Planck bridge under the eight-tick octave and $D=3$ (T7, T8).

The module SIBridgeClosure closes the unique calibration from those RS-native units to SI. It introduces three positive conversion factors $a_T$, $a_L$, $a_M$ constrained by matching $c$, $\hbar$, and $G$, and proves uniqueness of the tick length once the dimensional anchor is supplied.

Before $\hbar_{\mathrm{RS}}$ and $G_{\mathrm{RS}}$ can be treated as positive reals (or cancelled in the identity $\hbar_{\mathrm{RS}}\cdot G_{\mathrm{RS}} = 1/\pi$), one needs the elementary fact that $\varphi^5 > 0$.

One-line wrapper. Apply Mathlib's pow_pos to the existing lemma phi_pos ($\varphi > 0$) at natural exponent 5. No further arithmetic is required.

Local parent results are hbar_RS_pos ($0 < \hbar_{\mathrm{RS}}$ via division by $\varphi^5$), G_RS_pos ($0 < G_{\mathrm{RS}}$ via $\varphi^5/\pi$), and hbar_RS_mul_G_RS (the native Planck identity $\hbar_{\mathrm{RS}}\cdot G_{\mathrm{RS}} = 1/\pi$, which cancels $\varphi^5$ after a non-zero check). Those positivity and cancellation facts underwrite the SI conversion constraints and the closed form $a_T^2 = \pi,\hbar_{\mathrm{SI}} G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$, i.e. $\tau_0 = \sqrt{\pi},\tau_{\mathrm{Planck}}$. The declaration is pure arithmetic scaffolding inside the structural SI-bridge closure; it does not itself predict SI values of $G$.