canonical_identity
plain-language theorem explainer
Any comparison operator satisfying the magnitude-of-mismatch conditions yields the identity property that self-comparison costs zero. Researchers encoding Aristotelian logic inside Recognition Science cite this when confirming that mismatch magnitude forces the structural axioms. The proof is a direct field projection from the hypothesis structure.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ satisfies the magnitude-of-mismatch interpretation, then $C(x,x)=0$ for all $x>0$.
background
The module formalises the canonicality step for the logic encoding: once a comparison operator is read as magnitude of mismatch, its operator-level conditions become the canonical content of that reading. A comparison operator returns a real-valued cost for comparing two positive quantities. The magnitude-of-mismatch structure packages five properties whose first field is precisely the identity condition.
proof idea
The proof is a one-line term that extracts the trivial_at_match field from the magnitude-of-mismatch hypothesis.
why it matters
The declaration supplies one direction of the canonicality implication inside the logic-as-functional-equation module. It shows that the mismatch-magnitude reading forces the zero self-cost axiom used in the Aristotelian encoding. The surrounding module verifies that these conditions are the structural content of the reading; the paper supplies the philosophical justification. It precedes derivations of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.