canonical_scale_invariance
plain-language theorem explainer
Any comparison operator satisfying the magnitude-of-mismatch conditions is scale-invariant. Researchers deriving the laws of logic from the Recognition Science functional equation cite this to obtain the scale-free property required for the Aristotelian constraints. The proof is a direct field projection from the MagnitudeOfMismatch structure.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies the magnitude-of-mismatch conditions (trivial value at exact match, symmetry under pair interchange, continuous determinability, scale-free comparison, and nontriviality), then $C$ is scale-invariant: $C(λx, λy) = C(x,y)$ for all $x,y,λ > 0$.
background
The module formalizes the canonicality step by showing that a magnitude-of-mismatch reading of comparison implies the structural conditions of LogicAsFunctionalEquation. A ComparisonOperator is a map ℝ → ℝ → ℝ that assigns a real cost to any pair of positive quantities. MagnitudeOfMismatch C is the structure whose fields are Identity C, NonContradiction C, ExcludedMiddle C, ScaleInvariant C, and NonTrivial C. ScaleInvariant C is the predicate ∀ x y lam, 0 < x → 0 < y → 0 < lam → C (lam * x) (lam * y) = C x y, which encodes that cost depends only on the ratio.
proof idea
The proof is a one-line term that extracts the scale_free field of the hypothesis hM : MagnitudeOfMismatch C.
why it matters
The result supplies the scale_invariant component needed to assemble SatisfiesLawsOfLogic from the mismatch package. It closes the canonicality bridge in the LogicAsFunctionalEquation development, ensuring the comparison operator is compatible with the J-cost and the multiplicative group structure used throughout the Recognition Science forcing chain. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.