ComparativeRecognizer
plain-language theorem explainer
A ComparativeRecognizer equips a configuration type C with a map from pairs to events in E plus a fixed equal event returned on every self-comparison. Recognition Geometry researchers cite the structure as the base object from which preorders and metrics are derived without assuming distances in advance. The declaration is a direct structure with three fields and no additional proof obligations.
Claim. A comparative recognizer on configuration space $C$ and event space $E$ consists of a function compare $: C times C to E$, a distinguished element eq_event in $E$, and the axiom that compare$(c,c)=$ eq_event for every $c in C$.
background
Recognition Geometry starts from qualitative detectors rather than metrics. A comparative recognizer supplies a map from configuration pairs to events together with a distinguished equal event that self-comparisons always return; this matches physical instruments such as balance scales or clocks that register only relative order. The module presents the construction as RG7 and shows how the not-greater-than relation induced by chosen greater-than events yields a preorder on $C$ when the recognizer satisfies the listed axioms.
proof idea
The declaration is the structure definition itself. No lemmas or tactics are invoked; the three fields directly record the comparison map, the equal event, and the self-comparison property.
why it matters
The structure is the root object of the Comparative module and is instantiated by downstream definitions such as comparativeEquiv, inducedPreorder, and inducedPartialOrder. It occupies the RG7 position in Recognition Geometry by establishing comparative detection as primary and metric structure as derived. The construction supports the framework claim that repeated qualitative comparisons suffice to generate the eight-tick octave and spatial dimension D=3 once J-cost selection is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.