positive_ratio_is_forced_by_scale_free_comparison
plain-language theorem explainer
Scale-invariant comparison operators on positive reals factor through the ratio x/y, yielding a cost function F on positive ratios. Researchers working on the Recognition Science foundation would cite this when reducing two-argument costs to one-argument functions on the multiplicative group. The proof is a direct application of the factorization theorem that establishes the existence of such an F.
Claim. If $C$ is a comparison operator on positive reals that is scale-invariant, then there exists a function $F : ℝ → ℝ$ such that for all positive $x, y$, $C(x, y) = F(x/y)$.
background
ComparisonOperator is an abbreviation for a map from pairs of positive reals to reals that returns the cost of comparing two quantities. ScaleInvariant requires that this cost is unchanged under simultaneous positive scaling of both arguments, so the cost depends only on the ratio of the two quantities. The module packages the fact that any such scale-invariant comparison on positive magnitudes factors through the ratio x/y as a reusable universal property.
proof idea
This is a one-line wrapper that applies the theorem scale_free_comparison_factors_through_ratio to the given comparison operator and scale-invariance hypothesis.
why it matters
This declaration supplies a searchable alias for the core factorization result inside the LogicAsFunctionalEquation module. It supports reduction of logical constraints to functions on the multiplicative group of positive ratios, a step that precedes the forcing chain from T0 onward. The result is used to express the four Aristotelian constraints as conditions on a single function of the ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.