IndisputableMonolith.Foundation.PrimitiveDistinction
This module defines the distinction predicate, a binary relation on a carrier type that detects distinguishability, with equality as the canonical case. It is imported by modules constructing recognizers, observers, and logic realizations from recognition. The module supplies the basic definitions and instances without theorems.
claimA distinction predicate on carrier $K$ is a binary predicate $D:K×K→Prop$ detecting distinguishability, with the equality relation on any type as the standard instance.
background
The module introduces the primitive notion of distinction as the starting point for the Recognition Science derivation of logic from a functional equation. It imports LogicAsFunctionalEquation to place the predicate in the setting where logic emerges from recognition operations. The canonical example is equality, available on every type, serving as the model for any binary test that returns a single value on unordered pairs.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the distinction predicate that feeds IndisputableMonolith.Foundation.RecognizerInducesLogic (which shows recognizers induce a law-of-logic realization) and IndisputableMonolith.Foundation.ObserverFromRecognition (which shows non-trivial recognition forces an observer interface). It is also imported by the root IndisputableMonolith module and by MagnitudeOfMismatch and MultiplicativeRecognizerL4, supporting the T0-T8 forcing chain and the unification of recognition geometry with Aristotelian logic.
scope and limits
- Does not impose symmetry or other algebraic properties on the predicate.
- Does not connect distinction to the J-cost or phi-ladder constructions.
- Does not address continuous or infinite carriers beyond the type-theoretic setting.
- Does not prove any instance satisfies the recognition composition law.
used by (5)
depends on (1)
declarations in this module (15)
-
def
Distinction -
def
equalityDistinction -
theorem
equalityDistinction_irrefl -
theorem
equalityDistinction_symm -
def
equalityCost -
theorem
identity_from_equality -
theorem
non_contradiction_from_equality -
theorem
totality_from_function_type -
theorem
equality_cost_satisfies_definitional_conditions -
def
CompositionConsistency -
def
hammingCostOnReal -
theorem
composition_consistency_not_definitional -
theorem
from -
theorem
aristotelian_decomposition -
theorem
equality_cost_satisfies_definitional