ratioCost_eq_derivedCost
plain-language theorem explainer
Scale-invariant comparison on positive reals reduces to a cost that depends only on the ratio of the two arguments. The theorem equates the ratioCost extraction with the derivedCost obtained by fixing the second argument at the multiplicative identity 1. Researchers modeling forced comparisons in Recognition Science cite the equivalence when collapsing general operators to their scale-free form. The proof is immediate reflexivity on the identical lambda definitions.
Claim. For any comparison operator $C : (0,∞) × (0,∞) → ℝ$, the ratio-derived cost equals the derived cost: $r ↦ C(r,1)$ obtained from scale invariance coincides with the function that fixes the second argument at the multiplicative identity.
background
The module shows that scale-invariant comparison on positive magnitudes factors through the ratio $x/y$. A ComparisonOperator is a map ℝ → ℝ → ℝ obeying the four Aristotelian constraints that make comparison a well-posed operation. Both ratioCost and derivedCost are defined identically as the map sending $r$ to $C(r,1)$, rendering the cost well-defined on the multiplicative group of positive ratios (see upstream derivedCost definition in LogicAsFunctionalEquation).
proof idea
The proof is a one-line wrapper that applies reflexivity; the two functions are definitionally identical by their shared lambda expression fun r => C r 1.
why it matters
The declaration unifies the ratio-based and derived-cost notations inside PositiveRatioForcing, confirming that the canonical factor extracted from scale invariance is exactly derivedCost. It directly supports the module claim that positive ratios are forced by scale-free comparison and aligns with the Recognition Science forcing chain (T5 J-uniqueness through T8 D=3). No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.