Pith. sign in
module module high

IndisputableMonolith.Constants.GravitationalConstant

show as:
view Lean formalization →

The module defines Newton's gravitational constant G in RS-native units as phi^5 over pi after fixing c to 1 and hbar to phi to the minus five. Researchers deriving gravitational effects from the self-similar ledger cite this definition when working with the phi-ladder mass formula. The module is a definition collection that imports the base constants and the phi-forcing result to assemble the expression.

claimIn RS-native units with $c=1$ and $\hbar=\phi^{-5}$, Newton's constant satisfies $G=\phi^5/\pi$.

background

The module belongs to the Constants domain and imports the base RS time quantum tau_0 equals one tick. It also imports the PhiForcing module, whose doc-comment states that phi is forced by self-similarity in a discrete ledger with J-cost.

The local theoretical setting uses the Recognition Composition Law to fix phi as the self-similar fixed point (T5-T6) and the eight-tick octave to reach D equals 3. The module doc-comment then substitutes the native values to obtain the explicit form for G.

proof idea

This is a definition module, no proofs. It declares the main object G_rs together with its positivity statement and the derived expression.

why it matters in Recognition Science

This module supplies the RS-native value of G that enters the mass formula yardstick times phi to the power of rung minus eight plus gap. It realizes the framework landmark G equals phi^5 over pi stated in the module doc-comment and supports derivations that rely on the phi-ladder and the unified forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)