module module

`IndisputableMonolith.Foundation.LogicAsFunctionalEquation`

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

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

IndisputableMonolith.Foundation.ArithmeticFromLogic module_import
IndisputableMonolith.Foundation.DomainBootstrap module_import
IndisputableMonolith.Foundation.GeneralizedDAlembert module_import
IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof module_import
IndisputableMonolith.Foundation.LogicRealization module_import
IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 module_import
IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability module_import
IndisputableMonolith.Foundation.PrimitiveDistinction module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.Foundation.DAlembert.Inevitability module_import

declarations in this module (16)

abbrev ComparisonOperator L64
def derivedCost L69
def Identity L93
def NonContradiction L100
def ExcludedMiddle L108
def ScaleInvariant L116
def RouteIndependence L128
def NonTrivial L142
structure SatisfiesLawsOfLogic L149
theorem identity_implies_normalized L167
theorem non_contradiction_and_scale_imply_reciprocal L185
theorem excluded_middle_implies_continuous L214
theorem route_independence_implies_multiplicative_consistency L248
theorem laws_of_logic_imply_dalembert_hypotheses L270
theorem RCL_is_unique_functional_form_of_logic L309
theorem J_is_unique_cost_under_logic L340