G_pos
plain-language theorem explainer
Positivity of the RS-native gravitational constant follows from its definition as φ^5 where φ is the golden ratio. Researchers deriving constants from the Recognition Science foundation cite this when confirming signs for G in the constant set. The proof is a one-line term-mode reduction that unfolds the definition and applies the power positivity lemma.
Claim. $G_{rs} > 0$ where $G_{rs} := φ^5$ and $φ = (1 + √5)/2$ is the golden ratio.
background
The ConstantDerivations module derives physical constants from the RS foundation using the composition law and J-cost function. G_rs is defined as φ^5 in RS-native units and emerges as the curvature extremum in recognition geometry, with the derivation involving the holographic bound and ledger capacity at mass scale M_0 = 1/φ^5. This builds on upstream results such as the G definition in Constants.GravitationalConstant (G_rs = φ^5 / π) and positivity lemmas for c and ħ.
proof idea
The term-mode proof unfolds G_rs to expose φ^5 and applies the lemma pow_pos to phi_pos, yielding the strict inequality directly.
why it matters
This result supports parent theorems including lambda_rec_pos and the Physical structure in Bridge.DataCore, which invoke G_pos under physical assumptions. It fills the G > 0 step in the constant derivation chain from the RS foundation (T5 J-uniqueness through T8 D = 3), ensuring positivity on the phi-ladder scaling for G = φ^5 / π in native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.