recognition_necessary
plain-language theorem explainer
If an observable on a state space S takes at least two distinct real values, then there exist types R1 and R2 admitting a nonempty recognition pairing Recognize R1 R2. Recognition theorists cite this to show that measurement distinctions force recognition structures in the cost foundation. The proof is a direct term construction that reuses S for both recognizer and recognized types and instantiates the pairing from the given state witnesses.
Claim. Let $S$ be a type and let $obs$ be an observable on $S$ such that there exist states $s_1,s_2$ with $obs.value(s_1)≠obs.value(s_2)$. Then there exist types $R_1,R_2$ such that the recognition pairing Recognize $R_1$ $R_2$ is inhabited.
background
The RecognitionForcing module proves that recognition structures are forced by the underlying cost foundation. An Observable on a type S is the structure supplying a value function S → ℝ that extracts real-valued measurements. The Recognize structure (imported from the Recognition module) is the minimal pairing of a recognizer type A with a recognized type B.
proof idea
The proof is a term-mode construction. It obtains the witnessing states s1 and s2 from the non-constancy hypothesis, then returns the tuple ⟨S, S, ⟨⟨s1, s2⟩⟩⟩ that directly supplies the required Recognize instance.
why it matters
This lemma feeds the master theorem recognition_forcing_complete, which assembles the full forcing statement that non-constant observables compel recognition. It supplies the existence half of the argument that distinctions in observable values necessitate recognition relations, consistent with the module's goal of deriving recognition from cost minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.