recognition_necessary
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the recognition structure.
- Does not quantify any associated recognition cost.
- Does not address continuous or infinite-dimensional state spaces.
- Does not invoke the J-cost function or phi-ladder.
Lean usage
theorem use_recognition_necessary (S : Type) (obs : Observable S) (h : ∃ s₁ s₂, obs.value s₁ ≠ obs.value s₂) : ∃ R₁ R₂, Nonempty (Recognition.Recognize R₁ R₂) := recognition_necessary S obs hformal statement (Lean)
154theorem recognition_necessary (S : Type) (obs : Observable S)
155 (h : ∃ s₁ s₂, obs.value s₁ ≠ obs.value s₂) :
156 ∃ (R₁ R₂ : Type), Nonempty (Recognition.Recognize R₁ R₂) := by
proof body
Term-mode proof.
157 obtain ⟨s₁, s₂, _⟩ := h
158 exact ⟨S, S, ⟨⟨s₁, s₂⟩⟩⟩
159
160/-- **MASTER THEOREM: Recognition Forcing Complete** -/