recognition_unique
plain-language theorem explainer
The declaration shows that every observable extraction mechanism on a set S determines a recognition structure on S in which two elements are recognized exactly when the mechanism assigns them identical real values. Workers on the forcing chain from cost structures to recognition would reference this uniqueness result. The argument proceeds by direct construction of the structure via the extraction map followed by an immediate verification of the equivalence.
Claim. Let $S$ be a type and let $M$ be an observable extraction mechanism on $S$, consisting of a function extract$: S → ℝ$ that is non-constant. Then there exists a recognition structure $R$ on $S$ such that for all $s_1, s_2 ∈ S$, $M$.extract$(s_1) = M$.extract$(s_2)$ if and only if $R$ recognizes $s_1$ and $s_2$.
background
The module establishes that recognition structures are forced by the cost foundation, importing LawOfExistence and LedgerForcing to connect extraction mechanisms to prior cost axioms. An observable extraction mechanism on $S$ is a map extract$: S → ℝ$ together with a witness that it is non-constant. A recognition structure on $S$ is a reflexive and symmetric relation recognizes$: S → S → Prop$ on the elements of $S$ (see the sibling RecognitionStructure definition). The upstream recognition_from_extraction constructs such a structure by setting recognizes to equality of the extracted reals, with reflexivity and symmetry following immediately from equality properties.
proof idea
The proof is a term-mode one-liner. It applies the upstream recognition_from_extraction to the given mechanism M to obtain the required structure, then supplies the trivial proof that the biconditional holds by reflexivity of logical equivalence.
why it matters
This theorem occupies the RecognitionForcing module whose module doc states that recognition is forced by the cost foundation. It supplies the uniqueness direction of the claim that recognition is the unique extraction mechanism. The result closes the direct link between extraction maps and recognition relations before the module turns to cost minima coinciding with recognition, completing one segment of the chain that begins in LawOfExistence and LedgerForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.