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