pith. sign in
module module high

IndisputableMonolith.Gravity.ZeroParameterGravity

show as:
view Lean formalization →

The module derives the Einstein gravitational coupling as exactly κ = 8φ⁵ from the J-cost ledger and forced D = 3. Researchers modeling emergent gravity or zero-parameter unification cite it to link the phi-ladder to Newtonian limits. It assembles targeted lemmas from Cost and DimensionForcing imports into closed-form expressions, positivity results, and ledger-to-gravity implications.

claimThe Einstein gravitational coupling satisfies \( \kappa = 8 \phi^5 \), where \( \phi \) is the self-similar fixed point forced by the Recognition Composition Law.

background

The module operates in the Gravity domain and imports the RS time quantum τ₀ = 1 tick, the Cost framework for J-cost and defectDist, LawOfExistence (x exists ⟺ defect(x) = 0), and DimensionForcing (D = 3 is forced by the RS framework). These supply the phi-ladder mass formula and eight-tick octave used to construct gravitational potential and coupling without free parameters.

Upstream results establish the ledger as the sole source: Constants fixes τ₀, while DimensionForcing supplies the topological and self-similar arguments that pin spatial dimension at three. The module then defines kappa_rs directly from the cost function and derives its properties.

proof idea

The module structures its content as a chain of definitions and lemmas rather than a single proof. It begins with kappa_rs from the J-cost, proves the closed form kappa_rs_closed_form via algebraic reduction on the phi-ladder, then establishes kappa_pos, kappa_ne_zero, and equivalence_principle_automatic. Further lemmas show gravity_from_ledger implies the eight-tick structure and kappa bounds.

why it matters in Recognition Science

This module supplies the derived κ = 8φ⁵ that SpacetimeEmergence imports to force the full Lorentzian metric, causal structure, and arrow of time. It directly realizes the DOC_COMMENT claim that the RS prediction for the Einstein coupling is derived rather than assumed, connecting T8 dimension forcing and the Recognition Composition Law to classical gravity.

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)