equalityDistinction
The declaration supplies the most primitive distinction predicate on an arbitrary type K by declaring two elements distinguishable precisely when they fail to be equal. It is invoked by any construction that begins from the existence of distinguishable configurations, including the derivation of primitive observers and interfaces. The definition is a direct one-line abbreviation that unfolds immediately to the negation of equality.
claimFor any type $K$, the distinction predicate on $K$ is defined by $dist(x,y) := x ≠ y$.
background
In the PrimitiveDistinction module a Distinction on a carrier $K$ is any binary predicate $K → K → Prop$ that detects distinguishability between elements. The equalityDistinction supplies the canonical instance, available on every type without further structure or axioms. The module imports LogicAsFunctionalEquation, placing this predicate at the base layer before any arithmetic realization or functional equation is imposed.
proof idea
This is a direct definition: equalityDistinction K is the function sending any pair $x,y$ to the proposition $x ≠ y$. No lemmas or tactics are invoked; the body is the primitive disequality predicate itself.
why it matters in Recognition Science
This definition supplies the base case for NontrivialRecognition, which forces the existence of a PrimitiveInterface and PrimitiveObserver whenever at least two elements are distinguishable. It anchors the pre-physical observer theorem, showing that observer-dependence arises at the first moment a distinction becomes an event. The construction precedes the phi-ladder and J-cost structure in the forcing chain.
scope and limits
- Does not assume any algebraic or topological structure on the carrier K.
- Does not incorporate J-cost, phi-ladder, or forcing-chain data.
- Does not claim uniqueness among all possible distinction predicates.
- Does not extend the predicate beyond finite or discrete carriers.
formal statement (Lean)
65def equalityDistinction (K : Type*) : Distinction K :=
proof body
Definition body.
66 fun x y => x ≠ y
67
68/-- Reflexivity of the canonical distinction: an element is not distinct
69from itself. This is reflexivity of equality, a definitional fact of any
70type theory. -/