hbar_RS_pos
plain-language theorem explainer
hbar_RS_pos proves the RS-native reduced Planck constant is strictly positive. Derivations of certified constants in the Recognition Science framework cite it when confirming signs before applying the Einstein relation or Planck certification. The proof is a one-line term that chains positivity under natural exponentiation with positivity under inversion, using the base phi and coherence exponent 5.
Claim. $0 < hbar_{RS}$ where $hbar_{RS} = phi^{-5}$ in RS-native units.
background
The PlanckConstantFromRS module expresses the reduced Planck constant as $hbar_{RS} = phi^{-5}$ once the coherence exponent is fixed at 5. Module documentation states that k=5 is forced at D=3 by the Fibonacci route $k_{fib}(D)=2^D-D$ and the integration route $k_{int}(D)=D+2$. Upstream, coherenceExponent is defined as the natural number 5 in both Constants and this module, while phi_pos supplies the positivity of the golden-ratio base used in the exponentiation.
proof idea
The proof is a direct term-mode expression: inv_pos.mpr applied to pow_pos phi_pos coherenceExponent. It invokes the lemma that a positive real base raised to a natural-number power remains positive, then the lemma that the reciprocal of a positive real is positive.
why it matters
This positivity supplies the hbar_pos field required by planckConstantCert to certify the full set of RS constants. It closes the algebraic derivation of $hbar = phi^{-5}$ after CoherenceExponentUniqueness pins the exponent, consistent with the T7 eight-tick octave and T8 D=3 steps of the forcing chain. The module reports zero sorrys, completing this constant block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.