CanDistinguish
plain-language theorem explainer
CanDistinguish asserts that whenever an observable takes unequal real values on two states, there exists a Boolean classifier that marks those states as distinct. It is the Step-1 interface in the recognition-necessity chain: any nontrivial measurable quantity forces a distinction capability. The body is a pure Prop definition, not a proved theorem.
Claim. For a state space $S$ and an observable $\mathrm{obs}: S\to\mathbb{R}$, the predicate $\mathrm{CanDistinguish}(S,\mathrm{obs})$ holds when, for every pair of states $s_1,s_2$ with $\mathrm{obs}(s_1)\neq\mathrm{obs}(s_2)$, there exists a Boolean map $d:S\times S\to\{\mathrm{true},\mathrm{false}\}$ such that $d(s_1,s_2)=\mathrm{true}$.
background
The module RecognitionNecessity argues that any framework extracting observables must carry a recognition structure: the ability to distinguish and identify states. The strategy is three-step: (1) observables force distinction, (2) distinction forces comparison, (3) comparison without external reference is self-recognition; the Meta Principle then rules out empty recognition.
An Observable on a state space $S$ is simply a map $\mathrm{value}:S\to\mathbb{R}$. Upstream, the foundation layer already treats distinction as a binary predicate $K\to K\to\mathrm{Prop}$ (canonical case: inequality), and parallel Observable structures appear in RecognitionForcing and measurement cores with the same real-valued signature.
CanDistinguish packages the minimal operational content of Step 1: unequal measured values must be separable by some Boolean classifier on pairs of states.
proof idea
There is no proof obligation. The declaration is a def whose body is a Prop: universal quantification over state pairs with unequal observable values, asserting existence of a Boolean distinguisher that returns true on that pair. Downstream theorems either inhabit this Prop (from a nontriviality hypothesis) or take it as a hypothesis and build a comparison mechanism.
why it matters
This definition is the hinge for the module's Step 1 and Step 2. observables_require_distinction shows that any observable with two unequal values satisfies CanDistinguish. distinction_requires_comparison and distinction_requires_comparison_capability then consume that hypothesis to produce a ComparisonMechanism that is reflexive on the diagonal.
In the broader Recognition Science forcing picture, observables are not free data: extracting real values already commits the framework to distinction, hence to comparison, hence (absent external reference) to recognition structure. That is the necessity half of the exclusivity argument: frameworks that report measurements cannot avoid recognition. The definition itself is complete; the surrounding main theorems remain conditional on deeper measurement-theory lemmas noted in the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.