module module

`IndisputableMonolith.Foundation.MaximalForcing.RSHbarUniverse`

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 Lhbar0 L34
def LhbarRS L40
def tighten_Lhbar0_LhbarRS L45
def isHbarClaim L50
def hbarUniverse L55
theorem forced_hbar L64
theorem isHbarClaim_in_closure L71
def hbarForcedInvariant L77
theorem hbarUniverse_classifier L83
def hbarUniverseCert L92
theorem hbar_value_pos L98
theorem hbar_independent_over_Lhbar0 L103
theorem tightening_Lhbar0_LhbarRS_effective L117