equality_cost_satisfies_definitional_conditions
plain-language theorem explainer
Equality cost on an arbitrary type K with real weight meets the identity, symmetry, and totality axioms for a cost function solely from the equality relation. Foundation researchers in Recognition Science cite this result when verifying that the primitive distinction cost satisfies the definitional Aristotelian conditions before addressing the substantive composition law. The proof is a term-mode packaging of three upstream lemmas establishing each condition separately.
Claim. For any type $K$ and real number $w$, the equality-induced cost function satisfies: for all $x$ in $K$, cost$(x,x)=0$; for all $x,y$ in $K$, cost$(x,y)=$cost$(y,x)$; and for all $x,y$ in $K$ there exists real $c$ such that cost$(x,y)=c$.
background
In the PrimitiveDistinction module the equalityCost is the cost induced directly from the equality predicate on carrier $K$, scaled by the real weight parameter. The three packaged conditions are the definitional Aristotelian requirements: identity (zero self-cost), non-contradiction (symmetry), and totality (real-valued output). This sits in the foundation layer before the Recognition Composition Law (the d'Alembert equation on positive reals) is imposed via the Composition class in CostAxioms.
proof idea
The proof is a term-mode one-liner that constructs the conjunction by applying the three lemmas identity_from_equality, non_contradiction_from_equality, and totality_from_function_type to the parameters $K$ and weight.
why it matters
This theorem packages the definitional conditions (L1, L2, L3a) for the equality cost, serving as a prerequisite for the substantive Composition Consistency condition discussed immediately after in the module. It feeds into later developments of the cost axioms in the Recognition framework, where the full set including the d'Alembert equation forces the J-function form. No open questions are touched here as it is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.