equalityDistinction
plain-language theorem explainer
The definition supplies the canonical distinction predicate on any type K as the negation of equality. It is cited by the observer-from-recognition theorems that derive primitive observers from the existence of distinguishable pairs. The definition is realized as a direct abbreviation of the disequilibrium relation.
Claim. For any carrier set $K$, the distinction predicate $D_K:K×K→Prop$ is defined by $D_K(x,y)⇔x≠y$.
background
A distinction predicate on a carrier $K$ is a binary predicate that detects whether two elements are distinguishable. The canonical example is the equality test, available on any type. This definition appears in the Foundation.PrimitiveDistinction module, which supplies the most primitive logical distinctions before any physical structure is imposed.
proof idea
The definition is a direct abbreviation that maps any pair to the proposition that the elements are unequal.
why it matters
This definition supplies the base case for NontrivialRecognition and the observer-from-recognition theorems, which show that any carrier admitting a nontrivial distinction forces the existence of a primitive observer. It anchors the pre-physical layer where distinctions precede measurement. The downstream certificates use it to derive that observer-dependence is forced at the first distinguishable event.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.