module module

`IndisputableMonolith.Foundation.MaximalForcing.RSSelectionExample`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.MaximalForcing.RSPhiUniverse module_import

declarations in this module (18)

def psi L32
theorem psi_golden L35
theorem psi_ne_phi L41
def Lgolden L50
def tighten_Lgolden_LphiGold L55
theorem isPhi_not_forced_over_Lgolden L63
def positivitySelection L69
theorem isPhi_selected_over_Lgolden L76
theorem positivity_promotes_selected_to_forced L83
def trivialClaim L97
def positiveClaim L103
theorem trivialClaim_forced L107
theorem positiveClaim_independent L110
def triUniverse L128
def positiveIndepWitness L134
theorem triUniverse_classifier L154
def triUniverseCert L166
theorem all_three_branches_realized L173