module module

`IndisputableMonolith.Foundation.MaximalForcing.RSGravityUniverse`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.MaximalForcing.RealityClosure module_import

declarations in this module (13)

def Lgrav0 L34
def LgravRS L40
def tighten_Lgrav0_LgravRS L45
def isKappaClaim L50
def gravUniverse L55
theorem forced_kappa L63
theorem isKappaClaim_in_closure L70
def gravForcedInvariant L76
theorem gravUniverse_classifier L82
def gravUniverseCert L91
theorem kappa_value_pos L97
theorem kappa_independent_over_Lgrav0 L102
theorem tightening_Lgrav0_LgravRS_effective L115