pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof

show as:
view Lean formalization →

This module defines the operative positive-ratio comparison as a continuous nontrivial operator on positive reals obeying identity, symmetry, and scale invariance. Researchers tracing the direct path from mismatch magnitude to the Recognition Composition Law cite it when establishing canonical operator conditions. The module imports the parent LogicAsFunctionalEquation setup and exports the core definition plus supporting lemmas used by downstream canonicality and counterexample arguments.

claimA continuous nontrivial $C: (0,∞)×(0,∞)→ℝ$ is an operative positive-ratio comparison when it satisfies $C(x,x)=0$, $C(x,y)=-C(y,x)$, and $C(x,y)=C(λx,λy)$ for every $λ>0$.

background

The module belongs to the Foundation.LogicAsFunctionalEquation hierarchy and imports the base functional-equation machinery. It introduces the operative positive-ratio comparison, which encodes the magnitude of mismatch between positive ratios under the Recognition Composition Law. The parent module supplies the J-uniqueness (T5) and forcing-chain context (T0–T8) that motivate reading comparison operators as defect measures. The definition requires continuity, the identity condition, single-valued symmetry, and scale invariance on positive arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the operative positive-ratio comparison that feeds the canonicality argument, which states that once a comparison operator is read as a magnitude of mismatch the operator-level conditions become the canonical structural content of that reading. It also supports the quartic-log counterexample module. The definition fills the direct-proof step of the paper’s logic functional equation, connecting to the RCL and the eight-tick octave in the Recognition Science framework.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)