G_RS_pos
plain-language theorem explainer
Positivity of the RS gravitational constant follows directly from its definition as phi raised to the coherence exponent divided by pi. Researchers verifying the algebraic consistency of Recognition Science constants would cite this result when assembling certified bundles of hbar, G, and kappa. The term-mode proof applies div_pos to the positive power of phi and the positive real pi.
Claim. $0 < G_{RS}$ where $G_{RS} = phi^5 / pi$ in RS-native units with coherence exponent fixed at 5.
background
The PlanckConstantFromRS module defines G_RS as phi raised to coherenceExponent divided by Real.pi, with coherenceExponent set to 5. This exponent is the unique value forced at D=3 by the Fibonacci route k_fib(D)=2^D - D =5 and the integration route k_int(D)=D+2=5, as shown in the upstream CoherenceExponentUniqueness result. The module certifies the RS-native constants hbar = phi^(-5), G = phi^5 / pi, and kappa = 8 phi^5 once k=5 is pinned.
proof idea
The proof is a one-line term wrapper that applies div_pos to (pow_pos phi_pos coherenceExponent) and Real.pi_pos.
why it matters
This result supplies the G_pos field required by the downstream planckConstantCert definition, which bundles the certified constants together with the Einstein relation. It completes the algebraic verification of G = phi^5 / pi after the coherence exponent is fixed at 5 by the upstream uniqueness theorem. In the framework this supports the derivation of constants from the eight-tick octave at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.