nonempty_of_distinct_values
plain-language theorem explainer
If an observable on a state space takes two distinct real values, the state space is inhabited. Anyone building the recognition-necessity chain cites this to discharge the nonempty side-condition before constructing a recognition event. The proof is a one-line existential unpack: the first witness state is the inhabitant.
Claim. Let $S$ be a type and $O : S \to \mathbb{R}$ an observable. If there exist $s_1, s_2$ with $O(s_1) \neq O(s_2)$, then $S$ is nonempty.
background
This module shows that any framework extracting observables must carry recognition structure: the capacity to distinguish and identify states. The strategy is three-step: observables imply distinction, distinction requires 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: a quantity that can be extracted or measured from a state. Non-constancy of that map (two states with unequal values) is the standing non-triviality hypothesis throughout the necessity chain.
The lemma sits at the base of that chain. Before one can speak of a recognition event between recognizer and recognized types, the ambient state space must be inhabited; non-constant observables supply that witness for free.
proof idea
Tactic proof in two steps. Destructure the existential hypothesis to obtain a concrete state $s_1$ (the second state and the inequality are discarded). Package $s_1$ as the witness for Nonempty StateSpace. No lemmas are invoked; it is pure existential elimination.
why it matters
Feeds the main theorem observables_require_recognition: observable extraction requires recognition structure. That theorem takes a non-trivial observable (two states with unequal values) and produces inhabited recognizer and recognized types together with a recognition relation between them. This lemma is the first discharge of inhabitedness inside that argument.
In the module's three-step strategy it closes the trivial gap between "there exist distinct measured values" and "the state space is not empty," so later steps (distinction requires comparison; comparison is recognition; MP forbids empty recognition) can proceed without a separate nonempty hypothesis. It is scaffolding-free and fully proved; no open measurement-theory obligations attach to it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.