recognizer_forces_observer
plain-language theorem explainer
Non-trivial recognition forces a primitive observer: a finite interface on the event space. This is the public Recognition Core citation name for that forcing fact at the T0/T4 recognizer layer. The declaration is a one-line abbreviation re-exporting the upstream Observer-from-Recognition certificate (forcing theorem plus kernel-equivalence).
Claim. Non-trivial recognition forces a primitive observer (a finite interface) on the event space. The public name is the certificate package asserting that a non-trivial recognizer induces such an observer, together with the fact that the recognizer kernel is an equivalence relation.
background
Recognition Core is the public aggregator at the T0/T4 layer of the forcing chain: the recognizer, its indistinguishability quotient, the full recognition signature, and the completeness condition under which the signature determines physically relevant states. The module's standing claim is that a single Boolean observable is atomic, not complete; physical content is carried by the admitted recognizer family.
A recognizer is an admitted family of recognition acts on an event space. Its kernel classes are the indistinguishability quotient (gauge as absence of a distinguishing act). The upstream certificate this name points to states: "the primitive observer is forced by non-trivial recognition," and packages both the forcing theorem and the proof that the kernel is an equivalence.
Sibling targets separate related claims: completeness iff the family separates points; one Boolean coordinate is not complete; composing recognizers refines the quotient.
proof idea
One-line abbreviation. The body is exactly the upstream certificate observerFromRecognitionCert, whose fields are the theorem that non-trivial recognition forces a primitive observer and the lemma that the recognizer kernel is an equivalence relation. No local proof work; pure re-export for the public API.
why it matters
Listed among the module's public citation targets: non-trivial recognition forces a primitive observer. It anchors the T0/T4 story that the recognizer layer already supplies the observer structure before logic, lattice, or composition laws are derived.
The next sibling (recognizer_induces_logic) strengthens the same thread: a recognizer supplies the three definitional Aristotelian conditions plus the primitive observer automatically on its event space. Downstream of that sit the multiplicative composition law (d'Alembert form on the multiplicative event space) and the first recognition lattice from kernel classes.
No used_by edges are recorded at this aggregator name; consumers are expected to cite this symbol rather than the Foundation path. It does not itself touch T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, or T8 $D=3$; those sit later in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.