module module

`IndisputableMonolith.Foundation.LogicAsFunctionalEquationLogic`

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.Cost.JcostLogic module_import
IndisputableMonolith.Foundation.LogicAsFunctionalEquation module_import

declarations in this module (14)

abbrev ComparisonOperatorL L31
def derivedCostL L34
def transportComparison L39
def IdentityL L44
def NonContradictionL L48
def ScaleInvariantL L52
def NonTrivialL L57
structure SatisfiesLawsOfLogicL L63
theorem identityL_to_real L73
theorem nonContradictionL_to_real L83
theorem scaleInvariantL_to_real L93
theorem nonTrivialL_to_real L111
theorem lawsL_to_real L127
theorem RCL_is_unique_functional_form_of_logicL L133