pith. sign in
module module high

IndisputableMonolith.Constants.GravitationalConstant

show as:
view Lean formalization →

This module supplies the RS-native expression for Newton's gravitational constant. Researchers deriving mass ladders or gravitational relations from the phi-forcing chain cite it. The module reduces the general formula to phi^5 over pi once the time quantum and hbar are fixed from upstream definitions.

claim$G = phi^5 / pi$ in RS-native units, obtained from $G = lambda_rec^2 c^3 / (pi hbar)$ with $c=1$ and $hbar = phi^{-5}$.

background

The module belongs to the Constants domain and imports the base Constants module, which defines the RS time quantum tau_0 as 1 tick, together with the PhiForcing module. PhiForcing establishes that phi is forced by self-similarity in a discrete ledger with J-cost. The module doc states: Newton's gravitational constant G in RS-native units. G = lambda_rec squared times c cubed over pi hbar with lambda_rec = c = 1, hbar = phi to the minus 5. Thus G = phi^5 over pi.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the exact G value required by the Recognition Science constants set and the mass formula on the phi-ladder. It directly implements the G = phi^5 / pi landmark that follows from T5 J-uniqueness through T8 D=3 in the forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)