module module

`IndisputableMonolith.Foundation.LogicFromCost`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.OntologyPredicates module_import
IndisputableMonolith.Foundation.PreLogicalCost module_import

declarations in this module (19)

structure PropConfig L70
def prop_cost L79
def IsStable L82
def IsUnstable L85
structure ContradictionConfig L100
def contradiction_cost L114
theorem contradiction_positive_cost L127
def IsLogicalContradiction L152
theorem logical_contradiction_impossible L162
theorem zero_cost_contradiction_forbidden L173
structure ConsistentConfig L182
def consistent_cost L191
theorem consistent_zero_cost_possible L197
theorem consistent_minimum_cost L204
theorem logic_from_cost L221
theorem why_logic_is_real L256
theorem prelogical_boolean_fragment L268
theorem mp_from_cost_and_logic L291
theorem logic_from_cost_summary L319