distinction_requires_comparison_capability
plain-language theorem explainer
If an observable can separate states by unequal real values, a comparison mechanism for that observable must exist and be reflexive on every state. Anyone chaining observables to recognition structure cites this as Step 2 of the necessity argument. The proof unpacks the prior distinction-requires-comparison lemma and re-exports its built-in reflexivity.
Claim. Let $S$ be a state space and $\mathrm{obs}: S \to \mathbb{R}$ an observable. Suppose that whenever $\mathrm{obs}(s_1) \neq \mathrm{obs}(s_2)$ there exists a Boolean distinguisher returning true on $(s_1,s_2)$. Then there exists a comparison mechanism for $\mathrm{obs}$ (a Boolean binary relation that is reflexive, symmetric, and returns false on pairs with unequal observable values) such that $\mathrm{compare}(s,s)=\mathrm{true}$ for every $s \in S$.
background
This module shows that any framework extracting observables must carry recognition structure: the ability to distinguish and identify states. The strategy is three steps: observables force distinction, distinction forces comparison, and comparison without external reference is self-recognition. The Meta Principle then rules out empty recognition.
An observable here is simply a real-valued map on the state space. Distinguishability means that unequal observable values are witnessed by some Boolean predicate on pairs of states. A comparison mechanism packages a Boolean compare map with reflexivity, symmetry, and the requirement that unequal observable values compare false.
Step 2 sits between those definitions: once distinguishability is assumed, a full comparison mechanism is available, and in particular every state compares equal to itself. That reflexivity is the bridge into treating comparison as internal recognition.
proof idea
One-line unpacking of the sibling lemma that distinction requires comparison. Destructure that lemma's existential to obtain a comparison mechanism together with its reflexivity proof; re-package the same mechanism and discharge the pointwise reflexivity goal by simplifying with the extracted reflexivity hypothesis. No new algebraic content is introduced.
why it matters
Feeds the module's main theorem: observable extraction requires recognition structure (existence of nonempty Recognizer/Recognized types with a Recognize relation), under a nontriviality hypothesis that two states take different observable values. That main result combines distinction, comparison, and the identification of internal comparison with recognition.
In the module's three-step outline this is explicitly Step 2 (distinction requires comparison capability). Step 3 then treats any such mechanism as internal; the Meta Principle forbids trivial empty recognition and forces nontrivial structure. Within Recognition Science this is verification-side necessity, not a forcing-chain landmark (T5–T8), but it underwrites why frameworks that claim observables cannot avoid a recognition layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.