pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof

show as:
view Lean formalization →

This module defines operative positive-ratio comparisons as continuous nontrivial operators on positive reals that obey identity, symmetric single-valued comparison, and scale invariance. It supplies the direct-proof foundation for the logic functional equation and is cited by researchers tracing the Recognition Composition Law without extra hypotheses. The module consists of definitions and basic closure properties that downstream modules import directly.

claimAn operative positive-ratio comparison is a continuous nontrivial function $C: (0,∞)×(0,∞)→ℝ$ satisfying $C(x,x)=0$, $C(x,y)=C(y,x)$, single-valuedness, and scale invariance $C(λx,λy)=C(x,y)$ for all $λ>0$.

background

The module imports LogicAsFunctionalEquation and works entirely inside the positive-ratio setting. It introduces the operative positive-ratio comparison to encode magnitude of mismatch under the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). This matches the framework's emphasis on scale-invariant comparison operators that descend to ratio-based costs, as used in the phi-ladder and T5 J-uniqueness step.

proof idea

This is a definition module, no proofs. It states the OperativePositiveRatioComparison definition, records the sibling properties operative_descends_to_ratio and operative_derived_cost_symmetric, and assembles them into operative_to_laws_of_logic and rcl_direct_theorem.

why it matters in Recognition Science

The module supplies the direct structural content for the logic functional equation and is imported by Canonicality (which verifies the magnitude-of-mismatch reading) and by QuarticLogCounterexample (which exhibits C(x,y)=(log(x/y))^4). It therefore closes the paper's canonicality step at the level of positive-ratio operators before the full forcing chain or D=3 is invoked.

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)