equalityDistinction_symm
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.