G_rs_pos
plain-language theorem explainer
Physicists deriving Newton's gravitational constant from the Recognition Science phi-ladder cite this result to confirm its positivity. It shows that the expression phi to the fifth over pi is positive in native units. The term-mode proof unfolds the definition then applies the division positivity lemma with power positivity and pi positivity.
Claim. In RS-native units, the gravitational constant satisfies $0 < phi^5 / pi$.
background
The GravitationalConstant module formalizes the derivation of Newton's gravitational constant from the Recognition Science ledger geometry. With the recognition wavelength set to 1, the speed of light to 1, and the Planck constant to phi to the minus 5, the constant reduces to phi to the fifth over pi. This matches the general expression lambda squared times c cubed over pi times hbar specialized to these units.
proof idea
The proof first unfolds the definition of the RS gravitational constant. It then applies the division positivity lemma to reduce the claim to two separate inequalities. The first follows from the power positivity lemma applied to phi positivity at exponent 5. The second is the standard positivity of pi.
why it matters
This theorem is a direct input to the resolution of registry item C-002 in the sibling theorem that conjoins positivity with the definitional equality. It is also referenced in the BekensteinFromLedger paper for ledger-based derivations. The positivity confirms that the constant derived from the Recognition Composition Law and the eight-tick octave carries the expected sign with no free parameters after fixing the spatial dimensions to 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.