no_observables_without_recognition
plain-language theorem explainer
If a framework admits no recognition events between any pair of types, every observable on any state space is constant. Verification and exclusivity arguments cite this to force recognition structure into any non-trivial physics. The proof is a short contradiction: a non-constant observable yields a recognition witness via the main necessity lemma, which the no-recognition hypothesis immediately rules out.
Claim. Let $S$ be any state space and let $O:S\to\mathbb{R}$ be an observable (a real-valued extraction from states). Suppose that for all types $R_1,R_2$ there is no recognition event between $R_1$ and $R_2$. Then $O(s_1)=O(s_2)$ for every pair of states $s_1,s_2\in S$.
background
This module shows that any framework that extracts observables must carry a recognition structure: the ability to distinguish and identify states or events. An observable on a state space $S$ is simply a map $O:S\to\mathbb{R}$; the intended reading is a measurable quantity pulled from the state.
The module strategy is three-step. First, non-trivial observable extraction requires distinguishing states that take different values. Second, distinction requires a comparison mechanism. Third, comparison without an external reference is self-recognition. The Meta Principle then forbids empty recognition, so non-trivial structure is forced.
The present result is the contrapositive packaging of that chain: assume recognition is impossible for every pair of types, and conclude that every observable is constant. It sits downstream of the sibling that turns a pair of unequal observable values into an explicit recognition witness.
proof idea
Fix states $s_1,s_2$ and argue by contradiction. Assume $O(s_1)\neq O(s_2)$. Package that inequality as an existence statement: there exist states on which the observable takes distinct values. Apply the upstream necessity lemma that any such non-constant observable produces types $R_1,R_2$ and a non-empty recognition event between them. The global no-recognition hypothesis applied to those same types yields a contradiction. Hence the values must agree.
why it matters
In the Recognition Science verification layer this is the clean negative statement: without recognition events there is no non-trivial physics of observables. The module doc frames the Meta Principle as essential for non-trivial physics precisely because empty recognition is forbidden and, by this theorem, empty recognition collapses every observable to a constant.
It closes the necessity arc begun by the sibling results on distinction, comparison, and recognition-of-states: observables require distinction, distinction is comparison, comparison without external reference is recognition. Together they underwrite exclusivity claims that competing frameworks cannot derive measurable content while denying recognition structure. No further downstream consumers are wired yet; the result is a terminal lemma in the necessity module, ready for exclusivity and framework-comparison arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.