module module

`IndisputableMonolith.Foundation.MaximalForcing.RSMassLadderUniverse`

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.Foundation.PhiForcing module_import

declarations in this module (12)

def ladderMass L34
def Lmass0 L38
def isLadderRatioClaim L44
def isYardstickClaim L49
def massUniverse L54
theorem forced_ladderRatio L61
def yardstickIndepWitness L71
theorem yardstick_independent L83
theorem massUniverse_classifier L89
def massUniverseCert L101
theorem massUniverse_trichotomy L107
theorem mass_scaling_forced_yardstick_free L115