G_rs_pos
plain-language theorem explainer
The declaration proves that the RS-native gravitational constant is strictly positive. Researchers deriving the Bekenstein-Hawking entropy bound from ledger capacity on Z^3 cite it to confirm the sign of G before substituting into S = A/(4G hbar). The proof is a one-line term reduction that unfolds the local definition of G_rs and applies the positivity of phi to the fifth power.
Claim. $0 < G$ where $G = G_{rs} = phi^5$ in RS natural units.
background
The BekensteinFromLedger module derives the entropy bound S = A/(4G hbar) from the simplicial ledger on Z^3, using D = 3 from the forcing chain and the relation G hbar = 1. G_rs is defined in the module as phi^5. Upstream results supply the positivity of phi and the broader gravitational constant derivation G = phi^5 / pi in some contexts, but the local definition here omits the pi factor for the natural-unit ledger argument.
proof idea
The term-mode proof unfolds G_rs to expose phi^5, then applies the lemma pow_pos to the hypothesis phi_pos.
why it matters
This result feeds the gravitational_constant_derived theorem that resolves C-002 by fixing G from phi and pi with no free parameters. It supports the module's main line to bekenstein_hawking_from_rs, where positivity of G combines with hbar_rs_pos to give G hbar = 1 and thus S_BH = A/4. The step closes a prerequisite for the holographic bound in the RS ledger geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.