pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.GravitationalConstant

show as:
view Lean formalization →

This module defines Newton's gravitational constant G in Recognition Science native units as φ^5 / π. It substitutes the RS time quantum τ₀ = 1 tick together with ħ = φ^{-5} into the classical expression G = λ_rec² c³ / (π ħ). Researchers deriving gravitational effects from the discrete J-cost ledger would cite this value. The module acts as a definition hub that imports the base constants and the phi-forcing results, with no internal proofs.

claim$G = φ^5 / π$ in RS-native units where $c = 1$ and $ℏ = φ^{-5}$.

background

The module sits inside the constants domain and imports the RS time quantum τ₀ = 1 tick together with the PhiForcing module. PhiForcing establishes that φ is the unique self-similar fixed point of a discrete ledger equipped with J-cost, via the relation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). In this setting the classical gravitational formula is rewritten by setting the recognition length λ_rec = c = 1 and substituting the forced ħ = φ^{-5}.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the RS-native G that downstream siblings such as gravitational_constant_derived consume. It directly instantiates the framework constant G = φ^5 / π, which enters mass-ladder calculations and the eight-tick octave structure. No open scaffolding remains inside the module itself.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)