recognition_from_extraction
plain-language theorem explainer
Researchers establishing the forcing of recognition structures from observable extraction mechanisms cite this definition to construct the recognizes relation directly from equality of extracted real values. It supplies the concrete RecognitionStructure instance needed for uniqueness and completeness theorems in the Recognition Forcing module. The definition populates the three required fields by setting recognizes to extract-equality, self-recognition to reflexivity, and symmetry to equality symmetry.
Claim. Let $M$ be an observable extraction mechanism on a set $S$, consisting of a map $extract : S → ℝ$ that is not constant. Define the recognition structure $R$ on $S$ by declaring that $s_1$ is recognized by $s_2$ precisely when $extract(s_1) = extract(s_2)$. This satisfies reflexivity because equality is reflexive and symmetry because equality is symmetric.
background
In the Recognition Forcing module, which shows that recognition structures arise necessarily from cost foundations, two key structures are introduced. An observable extraction mechanism on $S$ provides a real-valued function extract together with the guarantee that it distinguishes at least two elements. A recognition structure on $S$ is a binary relation recognizes that is reflexive and symmetric. This definition bridges the two by inducing the relation from equality of extracted values. Upstream, the Chain module supplies a minimal RecognitionStructure stub used for standalone compilation, while the module itself defines the full version with the three axioms.
proof idea
The definition directly constructs the RecognitionStructure by specifying its three fields. The recognizes relation is defined as equality of the extract values from the input mechanism. Self-recognition follows from reflexivity of equality, and symmetry from its symmetry. No external lemmas are invoked; the construction is immediate from the definitions of the structures.
why it matters
This definition supplies the concrete instance required by the uniqueness theorem recognition_unique and feeds into the master theorem recognition_forcing_complete, which asserts that every observable extraction mechanism yields a recognition structure. It forms part of the chain demonstrating that recognition is forced by the cost foundation in Recognition Science, specifically linking extraction mechanisms to the recognition relation without additional assumptions. It touches the open question of whether all recognition structures arise this way from cost minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.