ratio_factor_unique
plain-language theorem explainer
If two functions F and G both express the same comparison operator C through the ratio x/y for positive arguments, then F and G agree on every positive real. Researchers deriving scale-invariant physical laws from functional equations would cite this uniqueness result. The proof is a direct substitution of the unit element into the defining equations followed by symmetry and transitivity.
Claim. Let $C$ be a comparison operator. Suppose functions $F,G : (0,∞) → ℝ$ satisfy $C(x,y) = F(x/y)$ and $C(x,y) = G(x/y)$ for all $x>0$, $y>0$. Then $F(r) = G(r)$ for every $r>0$.
background
The module shows that scale-invariant comparison on positive magnitudes factors through the ratio $x/y$. A ComparisonOperator is an ℝ → ℝ → ℝ map obeying the four Aristotelian constraints that make comparison a well-posed operation. The derivedCost is obtained by fixing the second argument at the multiplicative identity, producing a function on positive ratios under scale invariance.
proof idea
One-line wrapper that applies the defining equations at the unit ratio: fix arbitrary positive r, substitute x = r and y = 1 into both hF and hG, then equate the results by symmetry and transitivity.
why it matters
The theorem secures uniqueness of the ratio factor inside the scale-free comparison setup, supporting sibling constructions such as ratioCost and positive_ratio_is_forced_by_scale_free_comparison. It reinforces the forcing of scale invariance at the level of positive ratios in the Recognition Science chain and aligns with the functional-equation treatment of constants such as G.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.