ScaleInvariant
plain-language theorem explainer
ScaleInvariant defines the property that a comparison operator C on positive reals obeys C(λx, λy) = C(x, y) for all λ, x, y > 0. Researchers deriving functional equations from the laws of logic cite it as the step that converts two-argument costs into functions of ratios alone. The definition is the direct encoding of scale-free comparison with no additional lemmas required.
Claim. A comparison operator $C : ℝ → ℝ → ℝ$ is scale-invariant when $C(λx, λy) = C(x, y)$ for all $x, y, λ > 0$.
background
ComparisonOperator is the abbreviation ℝ → ℝ → ℝ for a map that assigns a real cost to comparing two positive quantities; the four Aristotelian constraints are imposed on such maps. The module develops these constraints as functional equations on the multiplicative group ℝ₊, with scale invariance supplying the bridge that makes the derived cost (obtained by fixing the second argument at 1) depend only on the ratio. Upstream results include the definition of derivedCost and the LedgerFactorization structure that calibrates the J-cost on positive ratios.
proof idea
This is the direct definition of the scale-invariance property as the stated forall condition on positive reals; no lemmas or tactics are applied.
why it matters
ScaleInvariant is a required field in the structure SatisfiesLawsOfLogic and its continuous variant SatisfiesLawsOfLogicContinuous; it also supplies the scale_free component of MagnitudeOfMismatch. The definition enables the translation lemmas that convert the laws into statements about the one-argument cost function, including non_contradiction_and_scale_imply_reciprocal. It is the explicit realization of the scale-free character of logical comparison in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.