module module

`IndisputableMonolith.Foundation.BiconditionalSelfNegation`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.GodelDissolution module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.OntologyPredicates module_import

declarations in this module (18)

def RSStab L69
def RSDiverge L72
def RSOutside L77
theorem stab_decidable L80
theorem diverge_impossible L85
theorem config_classification L93
structure SelfNegatingConfig L118
structure GeneralSelfNegatingPredicate L127
theorem no_self_negating_config L145
theorem no_general_self_negating_predicate L154
theorem no_self_negation_at_point L166
theorem self_negation_implies_false L176
structure ClassicalLogicAndUniqueMinimizerTheorem L202
theorem classical_logic_and_unique_minimizer_theorem L213
theorem complete_classical_logic_and_closure L224
structure GodelTargetClassPrerequisites L251
structure RsCategoricalDifferenceFromGodel L267
def rs_categorical_difference_from_godel L278