module module high

`IndisputableMonolith.Foundation.ObserverFromRecognition`

This module defines PrimitiveInterface as a map from carrier K to Fin n, the finite-resolution recognizer that serves as the pre-physical observer. Foundation researchers cite it when building the recognition lattice or showing that recognizers induce logic. The module supplies the core definitions and proves that the induced kernel is an equivalence relation.

claimA primitive interface on carrier $K$ is a map $r:K→ Fin n$ for finite $n$. Its kernel equivalence classes partition $K$ into distinguishable events; the interface is the pre-physical observer through which configurations become events.

background

The module sits in the Foundation layer and imports PrimitiveDistinction to supply the basic carrier and distinction structure. Its central object is PrimitiveInterface, a recognizer whose codomain is Fin n and therefore has finite resolution. Sibling definitions include PrimitiveObserver, the kernel predicates (kernel_refl, kernel_symm, kernel_trans, kernel_is_equivalence), NontrivialRecognition, Separates, and the pointInterface family that witnesses separation at a reference point.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the primitive recognizer that RecognitionLatticeFromRecognizer uses to form the first recognition lattice via kernel-equivalence classes and that RecognizerInducesLogic uses to realize the Law of Logic on the event space. It is imported directly by the root IndisputableMonolith module.

scope and limits

Does not claim the interface corresponds to a conscious observer.
Does not derive the resolution parameter n from the forcing chain.
Does not connect the interface to J-cost or the phi-ladder.
Does not assert that every finite-valued map arises from a physical process.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith module_import
IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer module_import
IndisputableMonolith.Foundation.RecognizerInducesLogic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveDistinction module_import

declarations in this module (17)

structure PrimitiveInterface L38
abbrev PrimitiveObserver L52
theorem kernel_refl L55
theorem kernel_symm L59
theorem kernel_trans L63
theorem kernel_is_equivalence L69
def NontrivialRecognition L80
def Separates L85
def pointInterface L91
theorem pointInterface_at_ref L99
theorem pointInterface_away L105
theorem pointInterface_separates L111
theorem nontrivial_recognition_forces_interface L129
theorem nontrivial_recognition_forces_observer L139
structure ObserverFromRecognitionCert L146
def observerFromRecognitionCert L155
theorem observerFromRecognitionCert_inhabited L159