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