ratioCost
The definition extracts a unary cost function from any binary comparison operator C by evaluating it at the second argument fixed to the multiplicative identity 1. Workers on scale-invariant comparisons in functional logic would reference this construction when reducing two-place costs to functions of positive ratios alone. The implementation is a direct one-line abstraction that applies C to the input ratio and unity.
claimFor a comparison operator $C : (0,∞) × (0,∞) → ℝ$, the ratio-derived cost is the map $r ↦ C(r,1)$.
background
A ComparisonOperator is an abbreviation for a map from pairs of positive reals to reals that satisfies the four Aristotelian constraints on comparison as a well-posed operation. The module PositiveRatioForcing establishes that scale-invariant comparisons on positive magnitudes factor through the ratio x/y, packaging this as a reusable property. Upstream, the ComparisonOperator definition supplies the structural content of comparison being well-posed.
proof idea
This is a one-line definition that applies the comparison operator C to the pair consisting of the input ratio r and the multiplicative identity 1.
why it matters in Recognition Science
This definition supplies the canonical factor used in the theorem scale_free_comparison_factors_through_ratio, which shows that scale-invariant comparison factors through the positive ratio. It also appears in the equality ratioCost_eq_derivedCost establishing equivalence to the derived cost. Within the Recognition framework it supports the forcing of positive ratios as the natural coordinates for scale-free comparisons, aligning with the universal property that J-costs and defects reduce to functions on ratios in the T5-T6 steps of the forcing chain.
scope and limits
- Does not impose scale invariance on the comparison operator.
- Does not specify the four Aristotelian constraints satisfied by ComparisonOperator.
- Does not extend to non-positive reals.
- Does not compute explicit numerical costs for particular comparisons.
Lean usage
example (C : ComparisonOperator) (r : ℝ) : ratioCost C r = C r 1 := rflformal statement (Lean)
16@[simp] def ratioCost (C : ComparisonOperator) : ℝ → ℝ :=
proof body
Definition body.
17 fun r => C r 1
18
19/-- Scale-invariant comparison factors through the positive ratio `x / y`. -/