equalityDistinction_symm
Symmetry of the canonical distinction asserts that for any type K and elements x, y in K, distinguishability holds in one order exactly when it holds in the other. This follows directly from the built-in symmetry of equality. The proof is a compact term-mode construction that unfolds the predicate and applies equality symmetry in each direction of the biconditional.
claimFor any type $K$, the canonical distinction predicate $D_K$ satisfies $D_K(x,y)leftrightarrow D_K(y,x)$ for all $x,y$ in $K$, where $D_K$ is the distinction induced by the negation of equality.
background
The PrimitiveDistinction module defines the equality-induced distinction predicate on an arbitrary type K. This predicate supplies the starting point for equality costs, irreflexivity, and consistency statements in the logic-as-functional-equation setting. The module imports Mathlib and LogicAsFunctionalEquation to access basic equality properties and recognition primitives.
proof idea
The proof is a term-mode wrapper. It introduces x and y, unfolds equalityDistinction, and supplies the biconditional by pairing the two implications, each obtained by applying symmetry to the equality hypothesis.
why it matters in Recognition Science
The result secures order-independence of the basic distinction, a prerequisite for the equality-induced cost defined later in the same module. It belongs to the initial layer of the Recognition Science foundation before the J-uniqueness step and the phi-ladder constructions. No direct users are recorded yet, but the property is required for any symmetric cost or composition law built on distinctions.
scope and limits
- Does not establish irreflexivity of the distinction.
- Does not connect the predicate to J-cost or the phi fixed point.
- Does not quantify over specific realizations or arithmetic objects.
- Does not address the Recognition Composition Law or higher-order distinctions.
formal statement (Lean)
79theorem equalityDistinction_symm (K : Type*) :
80 ∀ x y : K, equalityDistinction K x y ↔ equalityDistinction K y x := by
proof body
Term-mode proof.
81 intro x y
82 unfold equalityDistinction
83 exact ⟨fun h heq => h heq.symm, fun h heq => h heq.symm⟩
84
85/-! ## The Equality-Induced Cost -/
86
87/-- The **canonical cost induced by equality**: assigns 0 to identical
88pairs and a positive weight to distinct pairs. This is a function on
89pairs whose form is determined entirely by the equality predicate. -/