module module

`IndisputableMonolith.RRF.Foundation.Gravity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

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

IndisputableMonolith.RRF.Foundation module_import

declarations in this module (22)

structure SpatialLedger L26
def vacuumLedger L37
def massiveLedger L45
def massFromSpatialLedger L55
theorem mass_nonneg L58
theorem vacuum_has_zero_mass L61
structure LocalStrain L66
def strainFromLedger L73
theorem vacuum_has_zero_strain L79
structure ScalarCurvature L87
def curvatureFromStrain L92
theorem gravity_is_ledger_curvature L97
def G_Newton L107
def newtonGravity L110
def ledgerGravity L113
theorem ledger_equals_newton L117
structure LedgerDeadlock L123
def schwarzschildRadius L132
structure InsideSchwarzschild L135
structure GravityLedgerCorrespondence L144
def gravity_ledger_consistent L154
theorem gravity_interpretation_valid L161