ratio_factor_unique
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any comparison operator or factor function.
- Does not extend the uniqueness statement to non-positive ratios or zero.
- Does not invoke the explicit form of the J-cost or the phi-ladder.
- Does not address the Recognition Composition Law or higher forcing steps.
formal statement (Lean)
38theorem ratio_factor_unique
39 (C : ComparisonOperator) (F G : ℝ → ℝ)
40 (hF : ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y))
41 (hG : ∀ x y : ℝ, 0 < x → 0 < y → C x y = G (x / y)) :
42 ∀ r : ℝ, 0 < r → F r = G r := by
proof body
Term-mode proof.
43 intro r hr
44 have hF' := hF r 1 hr one_pos
45 have hG' := hG r 1 hr one_pos
46 simpa using hF'.symm.trans hG'
47
48/-- The canonical factor obtained from scale invariance is exactly
49`derivedCost`. -/