canonical_non_contradiction
plain-language theorem explainer
If a comparison operator on positive reals satisfies the magnitude-of-mismatch conditions, then its cost function is symmetric under argument swap. Researchers formalizing the Recognition Science encoding of Aristotelian logic cite this when confirming that the mismatch package yields the non-contradiction axiom. 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 interpretation (trivial at equality, symmetric pairs, determinate continuity, scale invariance, and nontriviality), then $C$ obeys non-contradiction: $C(x,y) = C(y,x)$ for all $x,y > 0$.
background
The Canonicality module formalizes the paper's canonicality step by reading comparison operators as magnitudes of mismatch. ComparisonOperator is the type ℝ → ℝ → ℝ assigning a real cost to pairs of positive quantities. NonContradiction is the predicate ∀ x y : ℝ, 0 < x → 0 < y → C x y = C y x, expressing reciprocal symmetry of the cost.
proof idea
The proof is a one-line term that projects the pair_symmetric field from the MagnitudeOfMismatch hypothesis hM.
why it matters
This result shows that the magnitude-of-mismatch package directly entails non-contradiction, confirming one direction of the canonicality equivalence in the logic encoding. It belongs to the module that verifies the operator conditions match the structural content of the mismatch reading, supporting the Recognition Science claim that the J-cost functional equation yields the expected Aristotelian properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.