NontrivialRecognition
plain-language theorem explainer
Nontrivial recognition on a carrier type K means the existence of at least one pair of elements x and y in K that fail to be equal. Foundational work in Recognition Science cites this as the minimal condition that forces a primitive observer interface downstream. The definition is a direct existential statement over the canonical equality distinction predicate.
Claim. A type $K$ admits nontrivial recognition when there exist $x, y : K$ such that $x$ is not equal to $y$, where the distinction is the canonical predicate induced by equality on any type.
background
The ObserverFromRecognition module establishes the pre-physical floor by showing that any non-trivial distinction forces a primitive interface, which functions as the minimal observer. The equalityDistinction predicate on a carrier $K$ is defined directly as the function sending pairs to the proposition $x ≠ y$; this is the most primitive distinction available in type theory without added structure. The module imports PrimitiveDistinction for this predicate and Constants for the dimensionless bridge ratio $K = ϕ^{1/2}$, though the parameter $K$ here denotes the carrier type itself. The local theoretical setting is that once a carrier admits even one such distinction, a finite-valued recognizer separating the pair must exist.
proof idea
The declaration is a direct definition whose body is the existential statement over equalityDistinction K x y. No lemmas or tactics are applied; the body simply unfolds the primitive distinction predicate.
why it matters
This definition is the input hypothesis for the theorem nontrivial_recognition_forces_interface, which states that non-trivial recognition forces a primitive observer, and for the compact certificate ObserverFromRecognitionCert. It supplies the base step in the chain from distinction to observer before the upgrade to finite-resolution recognizers in later modules. In the Recognition Science framework it marks the transition from raw carrier to the first observer-like structure, feeding directly into lattice constructions and the pre-physical observer theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.