hbar_RS_pos
plain-language theorem explainer
The RS-native reduced Planck constant is strictly positive: ℏ_RS = φ^{-5} > 0. Anyone discharging nonzero denominators in the SI bridge (a_M·a_T products, the a_T² identity, Planck-constant certificates) cites this. The proof unfolds the definition and applies positivity of the quotient 1/φ^5 from positivity of φ^5.
Claim. In RS-native units, the reduced Planck constant satisfies $0 < \hbar_{\mathrm{RS}}$, where $\hbar_{\mathrm{RS}} := 1/\varphi^5$ and $\varphi$ is the golden-ratio fixed point.
background
The SI Bridge Closure module fixes the unique calibration map from RS-native units to SI. In the native gauge the framework 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\cdot\pi\cdot\hbar=\lambda_{\mathrm{rec}}^2\cdot c^3$ at $\lambda_{\mathrm{rec}}=\ell_0=1$.
Here $\hbar_{\mathrm{RS}}$ is defined as $1/\varphi^5$ (written with a natural-number power so ring tactics apply without real powers). The golden ratio $\varphi$ is positive by the forcing chain (T6), so $\varphi^5>0$ is immediate from pow_pos. The companion Physics module records the same constant as $(\varphi^{\mathrm{coherenceExponent}})^{-1}$ with the same positivity claim.
Positivity is not decorative: every SI constraint that divides by $\hbar_{\mathrm{RS}}$ (the $\hbar$-matching constraint that determines $a_M a_T$, and the closed-bridge identity for $a_T^2$) needs a strict lower bound to obtain nonzero denominators.
proof idea
One-line term proof after unfolding. Expand $\hbar_{\mathrm{RS}}$ to $1/\varphi^5$, then apply div_pos to the pair $0<1$ and $0<\varphi^5$. The second factor is the sibling lemma phi_pow_5_pos, itself pow_pos phi_pos 5. No case splits or field rewriting beyond the definition.
why it matters
This is the positivity half of the RS-native Planck constant that the SI bridge treats as an exact prediction ($\hbar=\varphi^{-5}$ in native units; primer landmark). Downstream, aM_aT_eq_of_c_hbar invokes it as ne_of_gt hbar_RS_pos to clear the denominator when solving the $c$+$\hbar$ constraints for $a_M\cdot a_T=\hbar_{\mathrm{SI}}/(\hbar_{\mathrm{RS}},c_{\mathrm{SI}}^2)$. That identity is then multiplied into the main algebraic closure a_T_sq_eq, which yields $a_T^2=\pi,\hbar_{\mathrm{SI}},G_{\mathrm{SI}}/c_{\mathrm{SI}}^5$ (i.e. $\tau_0=\sqrt{\pi},\tau_{\mathrm{Planck}}$) under a closed bridge.
The Physics twin planckConstantCert packages the same positivity into the certificate record (hbar_pos := hbar_RS_pos). Without this lemma the conversion factors are not known to be well-defined reals, so the uniqueness claim of the SI bridge would stall at a division-by-zero obligation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.