MagnitudeOfMismatch
plain-language theorem explainer
MagnitudeOfMismatch packages the five structural conditions on a comparison operator C that together encode its reading as a magnitude-of-mismatch cost. Researchers deriving the Aristotelian laws from the Recognition functional equation cite this structure when converting the mismatch interpretation into the operative positive-ratio comparison. The declaration is a pure structure definition whose fields directly record the upstream predicates Identity, NonContradiction, ExcludedMiddle, ScaleInvariant and NonTrivial.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Then $C$ satisfies the magnitude-of-mismatch interpretation when $C(x,x)=0$ for all $x>0$, $C(x,y)=C(y,x)$, $C$ is continuous on the positive quadrant, $C$ is scale-invariant, and $C$ is nontrivial.
background
The module formalises the canonicality step of the Recognition Science derivation: once a comparison operator is read as magnitude of mismatch, its operator-level conditions become the canonical structural content of that reading. ComparisonOperator is the type of maps from pairs of positive reals to reals that assign a real-valued cost to each comparison. The upstream predicates supply the precise content: Identity requires zero self-cost, NonContradiction requires reciprocal symmetry, ExcludedMiddle requires continuity on the positive quadrant, ScaleInvariant requires dependence only on the ratio, and NonTrivial supplies the remaining structural constraint.
proof idea
The declaration is a structure definition. Its five fields are exactly the applications of the upstream predicates Identity, NonContradiction, ExcludedMiddle, ScaleInvariant and NonTrivial to the given operator C. No lemmas or tactics are applied; the structure simply records simultaneous satisfaction of the five conditions.
why it matters
MagnitudeOfMismatch is the hypothesis used by every canonical theorem in the module, including canonical_identity, canonical_non_contradiction, canonical_excluded_middle, canonical_scale_invariance and the composite canonicality_of_encoding that recovers SatisfiesLawsOfLogic. It therefore closes the canonicality step that converts the mismatch reading into the operative structure required for the Recognition Composition Law. The paper proposition that this reading is the correct Aristotelian content remains external to the formalisation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.