IndisputableMonolith.Foundation.PrimitiveDistinction
The PrimitiveDistinction module introduces the distinction predicate as the basic binary relation on a carrier type that flags distinguishable elements. It is cited by the root framework module and by layers that derive symmetry and composition rules from recognition. The module supplies the equality instance together with its elementary properties and serves as the entry point before cost functions or forcing steps appear.
claimLet $K$ be a type. A distinction predicate on $K$ is a binary predicate $D:K→K→Prop$ that returns true precisely when its arguments are distinguishable. The canonical case is the equality predicate on $K$.
background
The module sits at the base of the foundation layer and imports the functional-equation treatment of logic. It defines the distinction predicate together with the equality instance and records its immediate consequences: irreflexivity, symmetry, and the passage from equality to identity and non-contradiction statements. These objects supply the raw material for later modules that convert single-valued predication into symmetry of a comparison operator.
proof idea
This is a definition module. It declares the distinction predicate, instantiates it with equality, and proves the standard properties of equality (irreflexivity, symmetry) by direct application of the corresponding Mathlib lemmas.
why it matters in Recognition Science
The module feeds the root IndisputableMonolith declaration and the MagnitudeOfMismatch layer that encodes non-contradiction as symmetry of the comparison operator. It also supplies the primitive predicate used by RecognizerInducesLogic and ObserverFromRecognition when they lift recognition to an interface. The construction therefore anchors the entire T0-to-T8 forcing chain at the level of distinguishable pairs.
scope and limits
- Does not introduce the J-cost function or the recognition composition law.
- Does not treat the phi-ladder, mass formula, or physical constants.
- Does not address observer interfaces or the eight-tick octave.
- Does not prove any step of the unified forcing chain beyond the predicate itself.
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