non_contradiction_from_equality
plain-language theorem explainer
The equality-induced cost on any carrier set K is symmetric under argument interchange. Recognition theorists cite it as the derived non-contradiction property (L2) that holds automatically for the primitive mismatch measure. The proof is a direct term construction that unfolds the definition and splits on equality of the arguments, using reflexivity when equal and symmetry of negation when unequal.
Claim. Let $K$ be any type and $w$ a real number. Let $C:K→ K→ℝ$ be defined by $C(x,y)=0$ if $x=y$ and $C(x,y)=w$ otherwise. Then $C(x,y)=C(y,x)$ for all $x,y∈K$.
background
In the PrimitiveDistinction module the equalityCost function is the canonical cost induced by equality: it assigns zero to identical pairs and the supplied weight to distinct pairs. Its form is fixed entirely by the equality predicate on the carrier. The module frames this construction inside the derivation of logic from recognition costs, importing LogicAsFunctionalEquation to treat costs as functional equations on configurations.
proof idea
The proof is a term-mode construction. It introduces the pair of elements, unfolds equalityCost, performs case analysis on whether the arguments are equal, substitutes to obtain reflexivity in the equal case, and in the unequal case invokes symmetry of the negated equality predicate followed by simplification to equate both sides to the weight.
why it matters
This supplies the Non-Contradiction (L2) leg of the Aristotelian decomposition. It is invoked directly in equalityCost_singleValued to establish that the cost factors through unordered pairs, and in equality_cost_satisfies_definitional_conditions to package the three definitional conditions (Identity, Non-Contradiction, Totality). In the Recognition framework it shows that non-contradiction follows from the symmetry of equality with no further axioms, closing one definitional step before the substantive conditions (excluded middle, scale invariance) are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Point-free relations recovered from a parallel pair of frame operators
"Definition 4.10 (Open locale map): f_! ⊣ f^{-1} satisfying Frobenius reciprocity f_!(U ∧ f^{-1}(V)) = f_!(U) ∧ V. … Proposition 6.4: the cones _,_ are parallel (proof uses Frobenius reciprocity for t and s_! ⊣ s^{-1})."
-
Geometry rebuilt as a quotient of what measurements can distinguish
"Definition 4 (Indistinguishability): c_1 ∼_R c_2 iff R(c_1) = R(c_2), an equivalence relation on C induced by equality in E."