Distinction
plain-language theorem explainer
Distinction supplies the type of binary predicates on an arbitrary carrier K. Foundational work in Recognition Science cites it when establishing the existence of distinctions from any type. The definition is a direct abbreviation of the predicate type K to K to Prop.
Claim. A distinction predicate on a carrier set $K$ is any binary relation $K → K → Prop$.
background
The PrimitiveDistinction module defines the basic notion of distinction as a predicate. A distinction predicate on a carrier K is a binary predicate that detects whether two elements are distinguishable, with the canonical example being the equality test available on any type. This sits in the foundation layer imported from LogicAsFunctionalEquation, providing the starting point for comparison in the functional equation approach. Upstream results include the definition of K as phi to the 1/2 and the canonical arithmetic object, though the distinction type itself remains realization-independent.
proof idea
The declaration is a direct definition that equates Distinction K with the type of binary predicates on K. No lemmas are applied; it is an abbreviation.
why it matters
This definition is used to construct equalityDistinction and appears in the proof of the transcendental necessity of the axiom bundle A1-A3. It supplies the primitive distinction required by the Leibniz principle in the Recognition Science foundation, prior to the forcing chain T0-T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.