pith. sign in
module module high

IndisputableMonolith.Gravity.ZeroParameterGravity

show as:
view Lean formalization →

This module derives the Einstein gravitational coupling as κ = 8φ⁵ from Recognition Science without free parameters. Physicists studying unification or quantum gravity would cite it for replacing G with a forced constant. The argument assembles results on J-cost defects, existence via zero defect, and D = 3 to obtain gravitational potential from the phi-ladder.

claimThe Einstein gravitational coupling in RS units satisfies $\kappa = 8\phi^5$.

background

The module sits in the Gravity domain and imports Constants (τ₀ = 1 tick), Cost (J-cost and Recognition Composition Law), LawOfExistence (x exists iff defect(x) = 0), and DimensionForcing (D = 3 forced by four arguments). These supply the ledger defects and phi-ladder on which gravitational potential is built. The module doc-comment states the RS prediction for the Einstein gravitational coupling: κ = 8φ⁵, derived not assumed.

proof idea

The module consists of a sequence of theorems (kappa_rs, gravitational_potential, gravity_from_ledger, etc.). Each applies upstream lemmas from LawOfExistence and DimensionForcing via short algebraic reductions or one-line wrappers that invoke the Recognition Composition Law to express the coupling in terms of φ.

why it matters in Recognition Science

This module supplies the gravitational sector required by the downstream SpacetimeEmergence module, which forces the full Lorentzian geometry from J-cost. It realizes the T8 step (D = 3) in the forcing chain and supplies the derived coupling that enters the Einstein equations, closing a free parameter in the RS framework.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (12)