scale_free_comparison_factors_through_ratio
plain-language theorem explainer
Scale-invariant comparison operators on positive reals factor through the ratio of their arguments. Researchers deriving the Recognition Composition Law from scale-free logic cite this to reduce two-argument costs to a function of the positive ratio alone. The proof constructs the factor explicitly as ratioCost and applies the scale-invariance hypothesis by rescaling the second argument to unity.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator satisfying scale invariance: $C(λx, λy) = C(x,y)$ for all $λ,x,y > 0$. Then there exists $F : ℝ → ℝ$ such that $C(x,y) = F(x/y)$ for all $x,y > 0$.
background
A ComparisonOperator is a real-valued cost map on pairs of positive reals. ScaleInvariant requires the cost to be unchanged under simultaneous positive scaling of both arguments, so that it depends only on their ratio. ratioCost is the one-argument function obtained by fixing the second argument at 1. The module packages the universal property that any scale-invariant comparison on positive magnitudes factors through the ratio x/y.
proof idea
The proof refines the witness to ratioCost C. Scale invariance is applied to the triple (x, y, y^{-1}) to obtain C x y = C (y^{-1} x) (y^{-1} y). The algebraic identities y^{-1} x = x/y and y^{-1} y = 1 then reduce the right-hand side to C (x/y) 1, which equals ratioCost (x/y).
why it matters
This supplies the factorization step used by scale_free_counted_once_logic_forces_ratio_rcl to combine scale-free comparison with finite logical comparison and force the Recognition Composition Law on the derived cost. It realizes the module claim that positive ratios are the forced coordinates for scale-invariant comparison, a prerequisite for expressing the laws of logic on the multiplicative group ℝ₊ before reaching J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.