Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveDistinction

show as:
view Lean formalization →

Defines distinction predicates on a carrier as the primitive binary relation that detects distinguishability. Equality is the canonical case, with short lemmas recovering identity, non-contradiction, and totality, plus an equality cost and a composition-consistency interface. Foundation modules on recognizers, observers, and mismatch magnitude import it as the shared starting point. The content is mostly definitional with elementary Prop lemmas.

claimA distinction predicate on a carrier $K$ is a binary predicate detecting whether two elements are distinguishable. The canonical instance is equality: $D(x,y)$ holds iff $x=y$. From it one obtains identity, non-contradiction, totality of the comparison, an equality cost on $\mathbb{R}$, and a composition-consistency condition that is not purely definitional.

background

Recognition Science treats logic as forced structure on comparison, not as an external axiom set. Before recognizers or the Logic functional equation can act, one needs a primitive that says when two values on a carrier are the same or not. This module supplies that primitive: a distinction predicate on $K$, with equality as the default instance available on any type.

The surrounding Foundation layer (imported from Logic-as-functional-equation) already frames Aristotelian conditions as properties of a comparison operator. Here those conditions are recovered in the equality case: irreflexivity failure becomes identity, symmetry of mismatch becomes non-contradiction, and function-typed comparison gives totality. An equality cost and a Hamming-style real cost appear as numeric lifts of the same predicate.

Composition consistency is stated as a separate interface rather than a free consequence of the type of distinction, marking the boundary between definitional structure and substantive recognition hypotheses used later.

proof idea

This is primarily a definition module. Distinction and equality-distinction are introduced as predicates; irreflexivity and symmetry of equality-distinction are immediate Prop lemmas. Identity, non-contradiction, and totality are one-step specializations of those equality facts and of the function type of the comparator. Equality-cost definitional conditions are checked by unfolding. Composition consistency is packaged as a named hypothesis-shaped structure; a companion lemma records that it is not automatic from the distinction signature alone. No deep tactic proof is required.

why it matters in Recognition Science

Every later Foundation path that turns recognition into logic needs a shared notion of distinguishability. Magnitude-of-mismatch imports this to treat single-valued comparison on unordered pairs and to force symmetry of the comparison operator as non-contradiction. Recognizer-induces-logic and the multiplicative-recognizer (L4) development use the distinction and composition-consistency interfaces when showing that a recognizer on an event space yields a Law-of-Logic realization, with (L4) either assumed or derived under multiplicativity. Observer-from-recognition builds the next step: non-trivial recognition forces an interface, read as a primitive observer. In the forcing chain this sits below J-uniqueness and the RCL, fixing the logical substrate on which cost and self-similarity later act.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (16)