Pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation

show as:
view Lean formalization →

The module defines the comparison operator on positive reals and the four Aristotelian constraints that encode logical comparison as a cost functional. Researchers tracing the Recognition Science forcing chain from logic to the d'Alembert equation cite it as the interface layer. The module consists of definitions together with elementary implications between the laws.

claimLet $C:\mathbb{R}_+\times\mathbb{R}_+\to\mathbb{R}$ be a comparison operator. The Aristotelian laws require $C(x,x)=0$, mutual exclusion of contradictory costs, exhaustive coverage of alternatives, and invariance under positive scaling of both arguments.

background

The module imports functional-equation helpers from Cost.FunctionalEquation and the uniqueness result from DAlembert.Inevitability, which establishes that the d'Alembert equation is the unique form compatible with multiplicative consistency of any cost functional. The central object is the comparison operator $C$, equipped with derived cost and the named laws Identity, NonContradiction, ExcludedMiddle, ScaleInvariant, RouteIndependence and NonTrivial. These laws are collected under the predicate SatisfiesLawsOfLogic.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the common interface for the Law of Logic and are imported by ArithmeticFromLogic, DomainBootstrap, GeneralizedDAlembert, LogicRealization, MultiplicativeRecognizerL4 and PrimitiveDistinction. They thereby anchor the translation from logical constraints to the Recognition Composition Law and the T5 uniqueness step in the forcing chain.

scope and limits

used by (8)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)