ComparisonOperator
plain-language theorem explainer
A comparison operator is a map from pairs of positive reals to reals that returns the cost of comparing two quantities. Foundation researchers cite it when imposing the four Aristotelian constraints to obtain the Laws of Logic as functional equations. The declaration is a one-line type abbreviation with no further content.
Claim. A comparison operator is a function $C : (0,∞) × (0,∞) → ℝ$ that returns the real-valued cost of comparing two positive quantities.
background
In LogicAsFunctionalEquation the comparison operator is the primitive object on which the four Aristotelian conditions (identity, non-contradiction, excluded middle, scale invariance) are later imposed. The doc-comment states that these constraints encode the structural content of comparison as a well-posed operation. Upstream, the type appears together with multiplicative (J-automorphism preservation) and derivedCost (the cost induced by fixing the second argument at the multiplicative identity).
proof idea
The declaration is an abbreviation for the function type ℝ → ℝ → ℝ; no lemmas or tactics are applied.
why it matters
It supplies the domain for SatisfiesLawsOfLogic and therefore for generatorOfLawsOfLogic, which extracts an explicit non-trivial generator from the laws. It is also the input type for real_supports_logic and for the continuous-combiner analysis package in GeneralizedDAlembert. The definition therefore sits at the root of the chain that derives arithmetic from the Recognition functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.