pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation

show as:
view Lean formalization →

The module formalizes the Law of Logic by introducing a comparison operator C on positive reals together with four Aristotelian constraints that encode well-posed comparison as a functional equation. Researchers deriving arithmetic or domain properties from logic cite it as the common interface. The module consists of definitions for the operator and its properties plus short lemmas relating them, relying on the imported d'Alembert inevitability result.

claimLet $C:\mathbb{R}_+\times\mathbb{R}_+\to\mathbb{R}$ be a comparison operator. The module defines the four Aristotelian constraints (identity, non-contradiction, excluded middle, scale invariance) that any such $C$ must satisfy for comparison to be well-posed, along with derived notions such as route independence and non-triviality.

background

The module imports Cost.FunctionalEquation (lemmas for the T5 cost uniqueness proof) and DAlembert.Inevitability (which proves the d'Alembert functional equation is the unique form for multiplicative consistency of a cost functional). The DOC_COMMENT states: "A comparison operator on positive reals takes two positive quantities and returns a real-valued cost of comparing them. The four Aristotelian constraints below are the structural content of comparison being a well-posed operation." Sibling definitions include ComparisonOperator, Identity, NonContradiction, ExcludedMiddle, ScaleInvariant, RouteIndependence, NonTrivial and SatisfiesLawsOfLogic.

proof idea

This is a definition module, no proofs. It assembles the comparison operator and the four constraints as named definitions, then records elementary implications among them (identity_implies_normalized, non_contradiction_and_scale_imply_reciprocal, excluded_middle_implies_continuous) as short lemmas.

why it matters in Recognition Science

This module supplies the Law of Logic definitions imported by ArithmeticFromLogic, DomainBootstrap, GeneralizedDAlembert, LogicRealization, MultiplicativeRecognizerL4 and PrimitiveDistinction. It therefore supplies the common object into which different Law-of-Logic settings are mapped and feeds the Universal Forcing program and the derivation of the Recognition Composition Law.

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)