pith. sign in
module module high

IndisputableMonolith.Constants.GravitationalConstant

show as:
view Lean formalization →

This module defines Newton's gravitational constant G in RS-native units as G = φ⁵ / π. Researchers deriving RS predictions for gravity and mass ladders would cite it to fix the coupling from the phi-forcing chain. The module is purely definitional, importing the base time quantum and the self-similarity argument that forces φ.

claim$G = \phi^5 / \pi$ where $\phi$ is the golden ratio forced by self-similarity in a discrete ledger with J-cost, $c=1$, and $\hbar = \phi^{-5}$.

background

The module belongs to the Constants domain. It imports the fundamental RS time quantum τ₀ = 1 tick and the PhiForcing module, whose doc states: "This module proves that φ is forced by self-similarity in a discrete ledger with J-cost."

Recognition Science expresses all constants from the T0–T8 forcing chain. With ħ fixed at φ^{-5} the Newtonian G follows at once as φ⁵ / π, consistent with the recognition composition law and the phi-ladder yardstick.

proof idea

This is a definition module, no proofs. It assembles the expression for G directly from the imported constants and the phi-forcing result.

why it matters in Recognition Science

The module supplies the RS-native value of G that enters mass formulas and gravitational dynamics downstream in the framework. It completes the constant derivation step that follows the phi-forcing argument and precedes applications of the eight-tick octave and D = 3.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)