PrimitiveObserver
plain-language theorem explainer
PrimitiveObserver is an alias for the PrimitiveInterface structure on any carrier type K, identifying the finite-resolution recognizer as the minimal observer forced by recognition. Researchers deriving the pre-physical forcing order from non-trivial distinctions to spacetime would cite this naming step. The declaration is a direct one-line abbreviation carrying no additional proof obligations.
Claim. Let $K$ be a type. A primitive observer on $K$ is a structure consisting of a positive natural number $n$ together with a map $observe : K → Fin n$ that assigns each configuration a distinguishable outcome in a finite set.
background
PrimitiveInterface is the structure with fields $n : ℕ$, $hpos : 0 < n$, and $observe : K → Fin n$. Its kernel equates two elements of $K$ precisely when they map to the same observed value, supplying the pre-physical notion of indistinguishability. The module context states that non-trivial recognition forces such an interface and that this interface is the primitive observer: the minimal map through which a distinction registers as an event rather than an external measuring device.
proof idea
The declaration is a direct abbreviation that renames PrimitiveInterface to PrimitiveObserver. No lemmas are invoked and no tactics are applied; the body consists solely of the alias.
why it matters
The alias places the observer at the recognition-interface stage of the pre-temporal forcing order, before timeTick and physical light. It is referenced by the certificate ObserverFromRecognitionCert and by the theorems primitive_observer_before_time and primitive_observer_before_physical_light. The module doc-comment emphasizes that the observer is not external to recognition but is the interface structure recognition itself forces, closing the step from bare distinction to event structure in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.