equalityDistinction_irrefl
plain-language theorem explainer
The theorem shows that the canonical distinction on any type K is irreflexive, so no element equals itself under that relation. Researchers constructing the logic foundation of Recognition Science cite it when deriving distinction properties directly from type theory. The proof is a short term-mode reduction that applies the defining hypothesis to reflexivity of equality.
Claim. For any type $K$ and every element $x$ of $K$, $x$ is not distinct from itself under the equality distinction.
background
The PrimitiveDistinction module introduces the equality distinction as the canonical relation on a type, where distinction between elements holds exactly when they fail to be equal. This sits inside the Recognition Science foundation that begins from a single functional equation and treats distinction as a primitive for building logic. Upstream results include the canonical arithmetic object (ArithmeticOf.canonical) that supplies an initial Peano structure independent of realization, together with the dimensionless bridge ratio $K = phi^{1/2}$ (Constants.K) used across the framework.
proof idea
The proof runs in term mode. It introduces an arbitrary element $x$ together with the hypothesis that equality distinction holds for $x$ with itself, then applies that hypothesis directly to the reflexivity proof rfl of $x = x$.
why it matters
This anchors irreflexivity of the distinction relation at the base layer, guaranteeing consistency with ordinary type theory before any physical constants or forcing chain steps are introduced. It supports sibling constructions such as symmetry of distinction and non-contradiction from equality that appear in the same module. No open scaffolding questions are addressed here; the result is treated as definitional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.