gravitational_constant_derived
plain-language theorem explainer
Recognition Science fixes the gravitational constant at phi to the fifth over pi in native units. A physicist deriving G from the ledger geometry cites this to close the constant registry. The proof reduces to pairing the positivity result with reflexivity.
Claim. $0 < G_{rs} ∧ G_{rs} = φ^5 / π$, where $G_{rs}$ is obtained from $G = λ_{rec}^2 c^3 / (π ℏ)$ by setting $λ_{rec} = c = 1$ and $ℏ = φ^{-5}$ in RS units.
background
The module derives Newton's gravitational constant in RS-native units from recognition geometry. G_rs is defined as phi^5 over pi, following from G = λ_rec² c³ / (π ℏ) with λ_rec = c = 1 and ℏ = phi^{-5}. The upstream G_rs_pos theorem establishes positivity by showing the quotient of positive terms is positive.
proof idea
The proof is a one-line term that constructs the conjunction from G_rs_pos and reflexivity on the definition of G_rs.
why it matters
This declaration resolves the C-002 registry item by confirming the explicit form of G in the constants module. It supports downstream work in papers such as BekensteinFromLedger on holographic bounds. Within the framework it aligns with the derivation of constants from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.