identity_from_equality
The theorem shows that any equality-induced cost on a carrier type K with real weight returns zero on identical arguments. Logicians and physicists deriving Aristotelian laws from recognition costs cite it as the definitional identity condition (L1). The proof is a one-line wrapper that unfolds the cost definition and reduces via simplification to reflexivity of equality.
claimFor any type $K$ and real weight $w$, the equality-induced cost satisfies $C(x,x)=0$ for all $x$ in $K$, where $C$ is the cost function derived from the equality predicate on $K$.
background
In the PrimitiveDistinction module the equalityCost function assigns zero to identical pairs and a positive multiple of the supplied weight to distinct pairs. This construction sits inside the derivation of logic from functional equations on costs, as imported from LogicAsFunctionalEquation. Upstream cost definitions appear in MultiplicativeRecognizerL4.cost (derivedCost on positive ratios) and ObserverForcing.cost (J-cost of a recognition event).
proof idea
The proof is a one-line wrapper: introduce the arbitrary element, unfold equalityCost, and apply simp to reduce the claim to reflexivity of equality.
why it matters in Recognition Science
This supplies the identity component for equality_cost_satisfies_definitional_conditions, which packages the definitional Aristotelian conditions and feeds the Recognizer structure in RecognizerInducesLogic. It fills the (L1) slot in aristotelian_decomposition, showing that identity follows from reflexivity rather than an extra axiom. The result anchors the foundation layer before substantive conditions such as scale invariance or non-triviality are imposed.
scope and limits
- Does not compute equalityCost on distinct arguments.
- Does not apply to cost functions not induced by equality.
- Does not address continuity, scale invariance, or non-triviality.
- Does not claim uniqueness of the equality-induced cost among all possible costs.
formal statement (Lean)
104theorem identity_from_equality (K : Type*) (weight : ℝ) :
105 ∀ x : K, equalityCost K weight x x = 0 := by
proof body
Term-mode proof.
106 intro x
107 unfold equalityCost
108 simp
109
110/-- **(L2) Non-Contradiction, derived.** The equality-induced cost is
111symmetric in its arguments. This follows from the symmetric definition
112of equality: `x = y` iff `y = x`. -/