ComparisonMechanism
plain-language theorem explainer
A comparison mechanism on a state space relative to an observable is a reflexive, symmetric Boolean pairing that returns false whenever the observable takes different real values. Anyone proving that measurable distinction forces recognition structure cites this bundle. It is a pure structure definition packing the three axioms used in the necessity chain.
Claim. Fix a type $S$ of states and an observable $O:S\to\mathbb{R}$. A comparison mechanism for $O$ is a map $c:S\times S\to\{\mathrm{true},\mathrm{false}\}$ such that (i) $c(s,s)=\mathrm{true}$ for all $s$, (ii) $c(s_1,s_2)=c(s_2,s_1)$, and (iii) if $O(s_1)\neq O(s_2)$ then $c(s_1,s_2)=\mathrm{false}$.
background
The module RecognitionNecessity shows that any framework extracting observables must carry a recognition structure: the ability to distinguish and identify states. The strategy is three steps: observables imply distinction, distinction requires comparison, and comparison without external reference is self-recognition. The Meta Principle then forbids empty recognition.
An observable on a state space $S$ is simply a real-valued extraction map $O:S\to\mathbb{R}$. The sibling notion CanDistinguish packages the claim that some pair of states yields unequal observable values. ComparisonMechanism is the intermediate object that turns that distinction into an explicit Boolean pairing with the algebraic properties needed downstream.
The surrounding verification layer imports the Recognition API and the exclusivity Framework; the present definition stays elementary and does not itself invoke J-cost, the phi ladder, or the forcing chain T0–T8.
proof idea
No proof body: this is a structure declaration. The four fields are the data and axioms. The map compare is the pairing; compare_refl and compare_symm are the usual equality-like laws; distinguishes_obs ties the pairing to the given observable by forcing false on unequal measured values. Downstream constructions (for example distinction_requires_comparison) inhabit the structure by defining compare from equality of O values and discharging the three fields by rewriting.
why it matters
This structure is Step 2 of the module strategy: distinction requires comparison. It is the carrier type for distinction_requires_comparison and distinction_requires_comparison_capability, which produce an inhabitant from CanDistinguish. ComparisonMechanismIsRecognition turns any such mechanism (plus a nonempty state space) into an explicit recognition event in the minimal pairing model. InternalComparison extends it by a no-external-reference field, and zero_params_forces_internal_comparison shows every comparison mechanism can be viewed as internal.
In the broader Recognition Science verification story, the point is necessity: frameworks that report observables cannot avoid a recognition-like comparison layer. That feeds the exclusivity argument that recognition structure is forced rather than optional. The definition itself is complete; main theorems above it remain modulo deeper measurement-theory results noted in the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.