IndisputableMonolith.Foundation.PrimitiveDistinction
The module introduces the distinction predicate as the primitive binary relation detecting distinguishability on a carrier type, with equality as the canonical case. It is imported by five downstream foundation modules that build recognition geometry and logic unification from this starting point. The module supplies only definitions and elementary properties of the predicate and its equality instance.
claimA distinction predicate on a carrier $K$ is a binary predicate $D:K→ K→Prop$ such that $D(x,y)$ holds precisely when $x$ and $y$ are distinguishable; the equality relation supplies the canonical instance $D(x,y)↔(x=y)$.
background
The module sits at the base of the Recognition Science foundation layer and imports only Mathlib together with LogicAsFunctionalEquation. Its central object is the Distinction predicate, defined as any binary predicate on a carrier that registers distinguishability, with equalityDistinction serving as the universal example available on every type. Sibling declarations then record that this predicate is irreflexive in the equality case, symmetric, and satisfies basic cost and consistency conditions that later modules lift to recognizers.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the primitive distinction predicate required by every subsequent foundation block. It is imported directly by IndisputableMonolith (root forcing-chain surface), MagnitudeOfMismatch (symmetry from single-valued predication), MultiplicativeRecognizerL4 (composition consistency), ObserverFromRecognition (interface as primitive observer), and RecognizerInducesLogic (recognizer-to-logic realization). These modules in turn realize the T0–T8 forcing chain and the Recognition Composition Law.
scope and limits
- Does not introduce any recognizer or composition law.
- Does not derive physical constants, dimensions, or the phi-ladder.
- Does not prove any instance of the master forcing-chain theorem.
- Does not address observer emergence or magnitude-of-mismatch symmetry.
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