ComparisonIsRecognition
plain-language theorem explainer
Internal comparison of states, with no external reference, is already a recognition event: the comparing state is the recognizer and the compared state is the recognized. Anyone arguing that zero-parameter observable frameworks force recognition structure would cite this bridge. The proof is a short inhabitance argument: pick any state and apply the two-state recognition constructor on the state space itself.
Claim. Let $S$ be a nonempty state space equipped with an observable $v : S \to \mathbb{R}$ and an internal comparison mechanism (comparison of states that uses only the states themselves, with no external reference). Then there exist types $R$ and $D$ such that the minimal recognition pairing $\mathrm{Recognize}(R,D)$ is inhabited.
background
This module shows that any framework extracting observables must carry a recognition structure: the ability 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 a real-valued extraction $v : S \to \mathbb{R}$ from a state space. Internal comparison extends a comparison mechanism by the constraint that compare$(s_1,s_2)$ equals some $f(s_1,s_2)$ built only from the states, so there is no outside yardstick. Recognition is the minimal pairing structure $\mathrm{Recognize}(A,B)$ with a recognizer in $A$ and a recognized in $B$.
Upstream, the same Observable shape appears in recognition-forcing and bridge cores as a real display on states; the recognition structure is the primitive pairing that the Meta Principle constrains (nothing cannot recognize itself).
proof idea
Short inhabitance proof. From nonemptiness of the state space, obtain a concrete state $s$. Instantiate both the recognizer type and the recognized type as the state space itself. Discharge the existence goal by the sibling constructor that builds a recognition event from any two states, applied to $(s,s)$. The internal-comparison hypothesis is present only to mark the zero-parameter setting; it is not unfolded in the body.
why it matters
This definition is the explicit bridge in Step 3 of the module strategy: comparison without external reference equals self-recognition. It sits among the necessity lemmas that turn observable extraction into a forced recognition structure, and it feeds the subsequent Meta Principle block that forbids empty or trivial recognition and therefore forces nontrivial structure.
In the broader Recognition Science chain, that forced recognition structure is what later carries cost (J-cost / magnitude of mismatch) and the forcing landmarks T5–T8. No downstream uses are wired yet in the graph, so the declaration presently closes a local definitional gap rather than a named parent theorem. Status note in the module: core definitions are complete; main necessity theorems remain modulo deeper measurement results, with no axioms beyond MP.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.