IndisputableMonolith.Foundation.ObserverFromRecognition
Defines a primitive interface: a finite-valued map from a carrier of configurations to Fin n, the pre-physical form of an observer. Configurations become distinguishable events only through this map. Downstream lattice and logic modules import it to build the recognition quotient and Law-of-Logic realization. The module is definitional: interfaces, kernel equivalence, separation, and point interfaces, with short proofs of the equivalence laws.
claimA primitive interface on a carrier $K$ is a map $r : K \to \mathrm{Fin}\, n$ (finite resolution). Its kernel $k \sim k'$ iff $r(k) = r(k')$ is an equivalence relation. Nontrivial recognition and separation axioms ensure the interface distinguishes at least two classes. Point interfaces pick a reference configuration and separate it from the rest.
background
Recognition Science treats observation as structural, not mental: a recognizer is any map that turns configurations into finitely many distinguishable events. This module sits on PrimitiveDistinction and introduces the finite-resolution form of that idea.
A primitive interface is a function $r : K \to \mathrm{Fin}, n$. The kernel relation (same image under $r$) is the indistinguishability relation of Recognition Geometry. The module proves it is an equivalence (reflexive, symmetric, transitive) and packages nontriviality and separation conditions so that the quotient is not a singleton.
Point interfaces specialize to a reference configuration: the interface that marks "at the reference" versus "away," giving the minimal two-class observer used later to seed lattices.
proof idea
Definition module with short supporting lemmas. PrimitiveInterface and PrimitiveObserver are structure/defs. The kernel laws (refl, symm, trans, is_equivalence) are direct from equality on Fin n. NontrivialRecognition and Separates are Prop bundles. pointInterface and its at_ref / away / separates lemmas are constructive instances showing a reference point yields a separating two-valued interface. No deep tactic proof; mostly definitional unfolding and eq.refl-style reasoning.
why it matters in Recognition Science
Feeds three foundation parents. RecognitionLatticeFromRecognizer turns the kernel-equivalence classes of such a recognizer into the first recognition lattice (pre-spatial quotient). RecognizerInducesLogic uses the same map to generate a Law-of-Logic realization on the event space. RecognitionCore aggregates this layer as the T0/T4 recognizer and indistinguishability quotient in the forcing chain.
Without a finite-valued interface, the lattice and logic-unification claims have no carrier map to quotient. This is the pre-physical observer: the map through which configurations become events, not a mind. It anchors the geometry-to-logic bridge in the companion paper on recognition geometry and logic unification.
scope and limits
- Does not construct a physical spacetime lattice or metric; only the pre-spatial kernel quotient setup.
- Does not force the codomain size n or identify Fin n with measurement outcomes in SI units.
- Does not prove completeness of the signature; that lives in RecognitionCore downstream.
- Does not derive J-cost, phi, or eight-tick structure; those are later forcing-chain steps.
- Does not model consciousness or agency; observer here is purely a finite-valued map.
used by (3)
depends on (1)
declarations in this module (17)
-
structure
PrimitiveInterface -
abbrev
PrimitiveObserver -
theorem
kernel_refl -
theorem
kernel_symm -
theorem
kernel_trans -
theorem
kernel_is_equivalence -
def
NontrivialRecognition -
def
Separates -
def
pointInterface -
theorem
pointInterface_at_ref -
theorem
pointInterface_away -
theorem
pointInterface_separates -
theorem
nontrivial_recognition_forces_interface -
theorem
nontrivial_recognition_forces_observer -
structure
ObserverFromRecognitionCert -
def
observerFromRecognitionCert -
theorem
observerFromRecognitionCert_inhabited