ComparisonOperator
The type of maps assigning a real cost to any pair of positive quantities serves as the entry point for deriving the laws of logic from the Recognition functional equation. Researchers tracing the arithmetic-from-logic chain cite this definition as the root object. It is introduced by a direct type abbreviation with no additional computation required.
claimA comparison operator is any function $C : ℝ → ℝ → ℝ$ such that, for positive inputs, $C(x, y)$ returns the cost of comparing the quantities $x$ and $y$.
background
The module treats the emergence of logic as a consequence of a functional equation satisfied by cost functions. The basic object is a map that takes two positive real numbers and returns a real number interpreted as their comparison cost. This map is required to obey four structural constraints that encode the Aristotelian laws of logic.
proof idea
This declaration consists of a single-line type abbreviation that identifies the comparison operator with the function space from the reals to the reals to the reals. No lemmas are applied; the abbreviation simply names the type for use in subsequent statements.
why it matters in Recognition Science
The definition supplies the root type for the entire logic-as-functional-equation development. It is used to construct the generator of the laws of logic and to establish that the real numbers support logic. It also enters the analysis of continuous combiners that recover bilinearity under additional smoothness hypotheses. In the broader Recognition Science setting it realizes the cost map whose properties force the phi-ladder and the spatial dimension count.
scope and limits
- Does not enforce positivity of arguments in the type signature.
- Does not include the four Aristotelian constraints on the operator.
- Does not provide the derived cost obtained by fixing one argument.
- Does not assume any regularity such as continuity or differentiability.
formal statement (Lean)
64abbrev ComparisonOperator := ℝ → ℝ → ℝ
proof body
Definition body.
65
66/-- The cost function derived from a comparison operator by fixing the
67second argument at the multiplicative identity. Under scale invariance,
68this is well-defined on the multiplicative group of positive ratios. -/
used by (40)
-
generatorOfLawsOfLogic -
real_supports_logic -
ContinuousCombinerAnalysisInputs -
continuous_combiner_bilinear -
continuous_combiner_bilinear_classification -
continuous_combiner_finite_smoothness_to_top -
continuous_combiner_log_smoothness_bootstrap -
ContinuousCombinerMollifierFiniteSmoothness -
ContinuousCombinerPsiAffineCompletion -
continuous_combiner_psi_affine_forcing -
ContinuousCombinerSecondDerivativeInput -
ContinuousRouteIndependence -
laws_continuous_subsumes_polynomial -
laws_polynomial_implies_continuous -
log_aczel_data_of_laws -
polynomial_implies_continuous -
RCL_is_unique_functional_form_of_logic_continuous -
SatisfiesLawsOfLogicContinuous -
derivedCost -
ExcludedMiddle -
excluded_middle_implies_continuous -
Identity -
identity_implies_normalized -
J_is_unique_cost_under_logic -
laws_of_logic_imply_dalembert_hypotheses -
NonContradiction -
non_contradiction_and_scale_imply_reciprocal -
NonTrivial -
RCL_is_unique_functional_form_of_logic -
RouteIndependence