magnitude_of_mismatch_forced
plain-language theorem explainer
A comparison operator C from any carrier K to costs is single-valued on unordered pairs exactly when it is symmetric. Researchers encoding Aristotelian non-contradiction inside the Recognition Science functional-equation derivation cite this equivalence when fixing the magnitude-of-mismatch reading. The proof is a one-line wrapper that applies the already-proved equivalence between single-valuedness and symmetry.
Claim. For any types $K$ and $Cost$, and any map $C:K→K→Cost$, there exists $f:Sym_2 K→Cost$ such that $C(x,y)=f(s(x,y))$ for all $x,y$ if and only if $C(x,y)=C(y,x)$ for all $x,y∈K$.
background
The module shows that symmetry of a comparison operator is forced by single-valued predication on unordered pairs. SingleValuedOnUnorderedPair is the property that $C$ factors through the type $Sym_2 K$ of unordered pairs, so the cost assigned to a pair is independent of presentation order. This encodes the Aristotelian (L2) Non-Contradiction condition inside the Logic-as-Functional-Equation setting.
proof idea
The proof is a one-line wrapper that applies the equivalence singleValued_iff_symmetric to the operator C.
why it matters
The result eliminates interpretive freedom in the magnitude-of-mismatch encoding by showing symmetry is required by single-valuedness rather than optional. It supplies the pair_symmetric field of the MagnitudeOfMismatch structure and thereby supports the rigidity claim that the logic-to-physics map is unique once single-valued predication is imposed. In the broader framework it aligns with the forcing chain that derives all structure from the functional equation without additional choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.