Distinction
Distinction K is the type of all binary predicates on an arbitrary carrier type K, supplying the most primitive notion of distinguishability in the Recognition Science foundation. Logicians and physicists formalizing the identity of indiscernibles cite it when grounding comparison before any metric or cost structure appears. The declaration is a direct type abbreviation with no further computation or lemmas required.
claimFor any type $K$, a distinction on $K$ is a binary predicate of type $K → K → Prop$.
background
In the PrimitiveDistinction module the declaration supplies the carrier type for predicates that detect whether two elements of $K$ are distinguishable. The canonical realization appears in the sibling equalityDistinction, which sets the predicate to inequality. This construction is realization-independent and precedes any arithmetic or forcing structure, matching the upstream canonical arithmetic object that treats initial Peano content as invariant across interpretations.
proof idea
The declaration is a one-line type abbreviation that directly aliases the function space $K → K → Prop$. No lemmas or tactics are invoked; the definition stands by itself as the primitive predicate type.
why it matters in Recognition Science
Distinction supplies the logical prerequisite for the axiom_bundle_transcendental theorem, which invokes Leibniz identity of indiscernibles to show that existence requires distinction and comparison. It is instantiated in equalityDistinction and appears in GammaRayBursts range checks. Within the framework it initiates the T0–T8 forcing chain by enabling the first comparison step before J-uniqueness, the phi fixed point, and the emergence of three spatial dimensions.
scope and limits
- Does not equip the carrier $K$ with any metric, order, or algebraic structure.
- Does not designate which predicate is used; a concrete instance such as equalityDistinction must be supplied separately.
- Does not address decidability, computability, or continuity of any predicate of this type.
formal statement (Lean)
60def Distinction (K : Type*) : Type _ := K → K → Prop
proof body
Definition body.
61
62/-- The canonical distinction induced by equality: two elements are
63distinct iff they are not equal. This is the most primitive distinction
64on any type and exists for every type without further structure. -/