module module

`IndisputableMonolith.Foundation.MaximalForcing.RSAlphaUniverse`

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.Foundation.MaximalForcing.RealityClosure module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import

declarations in this module (12)

def Lalpha0 L37
def LalphaRS L43
def tighten_Lalpha0_LalphaRS L48
def isAlphaWindowClaim L56
def alphaUniverse L61
theorem forced_alphaWindow L69
theorem isAlphaWindowClaim_in_closure L76
def alphaForcedInvariant L82
theorem alphaUniverse_classifier L88
def alphaUniverseCert L97
theorem alphaWindow_independent_over_Lalpha0 L104
theorem tightening_Lalpha0_LalphaRS_effective L116