nontrivial_recognition_forces_observer
plain-language theorem explainer
Non-trivial recognition on a carrier forces the existence of a primitive observer that separates at least one distinguished pair. Foundational work in Recognition Science cites this to establish that observer-like structure is forced directly by the first non-equality. The proof is a one-line wrapper that applies the interface-forcing theorem and renames the resulting interface as a primitive observer.
Claim. If a carrier $K$ admits non-trivial recognition (i.e., there exist distinguishable $x,y$ in $K$), then there exists a primitive observer $O$ for $K$ together with $x,y$ such that $O$ separates $x$ and $y$.
background
The module proves that non-trivial recognition forces an interface, identified as the primitive observer. NontrivialRecognition on $K$ means there exist $x,y$ with equalityDistinction $K$ $x$ $y$, i.e., at least one non-equality at the primitive floor. PrimitiveObserver is the abbreviation for PrimitiveInterface $K$, the minimal finite recognizer that turns a distinction into distinct observed outcomes. Separates $O$ $x$ $y$ holds when the observed values differ.
proof idea
The proof is a one-line wrapper that applies nontrivial_recognition_forces_interface $K$. That upstream theorem constructs the separating primitive interface from the non-triviality hypothesis; the present declaration simply renames the interface as a PrimitiveObserver.
why it matters
This supplies the observer-named form of the interface-forcing step and is invoked by the Observer-Forcing Theorem and by observerFromRecognitionCert. It fills the claim that observer-dependence is forced at the first distinction rather than added later, as stated in the module doc: 'It is forced at the first moment a distinction becomes an event.' The result supplies the pre-physical floor before upgrades in ObserverFormalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.