equalityCost
plain-language theorem explainer
equalityCost constructs the baseline cost on any type K that returns zero precisely when its arguments are equal and a fixed positive weight otherwise. Recognition Science work on primitive distinctions cites this to isolate the three definitional Aristotelian conditions before imposing the substantive composition law. The body is a direct conditional on Leibniz equality, so identity and symmetry hold by reflexivity and symmetry of = with no further lemmas.
Claim. Let $K$ be any type and $w > 0$ a real weight. The equality-induced cost $C : K → K → ℝ$ is defined by $C(x,y) = 0$ if $x = y$ and $C(x,y) = w$ otherwise.
background
In the PrimitiveDistinction module costs are tested against the four Aristotelian conditions: Identity (vanishes on the diagonal), Non-Contradiction (symmetry), Totality (total function), and Composition Consistency (compatibility with the carrier multiplication via the Recognition Composition Law). The upstream Identity definition from LogicAsFunctionalEquation states that comparing a thing with itself costs zero, the mathematical counterpart of A = A. This definition supplies the canonical example in which the first three conditions hold automatically from the equality predicate alone, without reference to any group structure or J-cost functional.
proof idea
The definition is a one-line case distinction on equality: return zero on the diagonal, otherwise the supplied weight. No lemmas are invoked; the body directly encodes the intended semantics.
why it matters
This definition supplies the running example for the Aristotelian decomposition theorem, which packages the three definitional conditions (L1–L3a) and demonstrates that composition consistency fails. It is invoked by equality_cost_satisfies_definitional_conditions, by the magnitude-of-mismatch results that separate single-valued costs from asymmetric ones, and by hammingCostOnReal. In the Recognition framework it isolates the point at which the forcing chain must add structure beyond bare equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 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."