pith. machine review for the scientific record. sign in
def definition def or abbrev high

G_rs

show as:
view Lean formalization →

G_rs defines the gravitational constant in RS-native units as the fifth power of the golden ratio phi. Researchers deriving constants from the J-cost functional equation and phi-ladder cite this when showing G emerges algebraically from recognition geometry. The definition is a direct assignment that normalizes the fundamental mass scale to 1/phi^5 and sets unit curvature.

claimIn RS-native units the gravitational constant is given by $G = phi^5$, where $phi$ is the self-similar fixed point of the recognition cost function $J(x) = (x + x^{-1})/2 - 1$.

background

The module derives physical constants from the RS foundation via the Composition Law, which forces the J-cost $J(x) = 1/2(x + 1/x) - 1$, then the golden ratio phi as fixed point, D = 3, and the eight-tick period tau0 = 8. This yields c = 1, hbar = phi^{-5}, and G as the curvature extremum in recognition geometry. The doc-comment states G ~ l0^3/(tau0^2 M0) with M0 = 1/phi^5, reducing directly to phi^5 in native units. Upstream, Constants.G supplies the general form G = lambda_rec^2 c^3 / (pi hbar), which collapses to phi^5 once c = 1 and hbar = phi^{-5}.

proof idea

This is a one-line definition that directly assigns G_rs to phi_val raised to the integer power 5.

why it matters in Recognition Science

It supplies the base G = phi^5 expression used in all_constants_from_phi, which collects the full set of constants derived from phi. It feeds gravitational_constant_derived, which resolves C-002 by showing G = phi^5 / pi with no free parameters, and supports G_rs_eq together with G_pos. This realizes the Level 4 step in the module derivation chain where G arises from the holographic bound and ledger capacity.

scope and limits

Lean usage

theorem G_rs_eq : G_rs = phi_val ^ 5 := rfl

formal statement (Lean)

 146noncomputable def G_rs : ℝ := φ_val^(5 : ℤ)

proof body

Definition body.

 147
 148/-- G = φ^5 in RS-native units. -/

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.