observables_require_distinction
plain-language theorem explainer
Non-trivial observables force a distinction capability: whenever two states yield different measured values, some Boolean comparator must mark them distinct. Anyone proving that measurement implies recognition structure cites this as Step 1 of the necessity chain. The proof builds the comparator directly from the observable's value map via decidable inequality of reals.
Claim. Let $S$ be a state space and $O:S\to\mathbb{R}$ an observable. If there exist $s_1,s_2\in S$ with $O(s_1)\neq O(s_2)$, then for every pair of states with unequal observable values there exists a Boolean map $d:S\times S\to\{\mathrm{true},\mathrm{false}\}$ such that $d(s_1,s_2)=\mathrm{true}$.
background
This module shows that any framework extracting observables must carry recognition structure: the ability to distinguish and identify states. The strategy has three steps: (1) observables require distinction, (2) distinction requires comparison, (3) internal comparison is self-recognition; the Meta Principle then forbids empty recognition.
An observable on a state space $S$ is a real-valued map $O:S\to\mathbb{R}$. The distinction predicate asserts that whenever $O(s_1)\neq O(s_2)$, some Boolean distinguisher returns true on that pair. Upstream, PrimitiveDistinction supplies the general notion of a distinction predicate $K\to K\to\mathrm{Prop}$, with equality as the canonical case; the present result specializes that idea to measurement values.
proof idea
The non-triviality hypothesis supplies some pair with unequal values; the goal is the universal claim that every value-differing pair admits a distinguisher. Introduce such a pair $s_1,s_2$ with $O(s_1)\neq O(s_2)$. Witness the existential by the concrete Boolean map $(a,b)\mapsto\mathrm{decide}(O(a)\neq O(b))$. Decidable inequality of reals then yields true on the given pair via decide_eq_true_iff, closing the goal. No external lemmas beyond that decidability fact are required.
why it matters
This is Step 1 of the Recognition Structure Necessity chain. Its sole downstream consumer is the main theorem observables_require_recognition: non-trivial observable extraction forces nonempty Recognizer and Recognized types with a Recognition.Recognize relation. Combined with the later steps (distinction requires comparison; internal comparison is self-recognition) and the Meta Principle ban on empty recognition, it closes the necessity argument that measurement frameworks cannot avoid recognition. On the verification side of RS, any physical theory that reports real observables is already committed to distinction, hence to the recognition calculus that underwrites the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.