order_descends_to_quotient
plain-language theorem explainer
When a recognizer is order-compatible with a comparative recognizer, the not-greater-than relation descends to the quotient by indistinguishability. Researchers formalizing recognition geometry cite this result to confirm that comparative orders are well-defined on equivalence classes. The proof is a term-mode reduction that invokes preorder transitivity twice after substituting via the compatibility hypothesis.
Claim. Let $R$ be a recognizer from configurations $C$ to events $E$ and $R_{cmp}$ a comparative recognizer from $C$ to events $E'$. Let $gt_events$ be a set of greater-than events and suppose $hp$ shows that $R_{cmp}$ induces a preorder. If $R$ is order-compatible with $R_{cmp}$ under $hp$, then for configurations $c_1,c_2,c_1',c_2'$ with $c_1$ indistinguishable from $c_1'$ and $c_2$ from $c_2'$ under $R$, $c_1$ not greater than $c_2$ under $R_{cmp}$ implies $c_1'$ not greater than $c_2'$ under $R_{cmp}$.
background
Recognition Geometry (RG7) starts from comparative recognizers that detect qualitative relations between pairs of configurations rather than assigning absolute labels. A ComparativeRecognizer supplies a compare map from $C×C$ to events together with an eq_event returned on self-comparison. The notGreaterThan predicate holds precisely when the comparison event lies outside the designated greater-than set. InducesPreorder packages reflexivity of the equal event and transitivity of notGreaterThan. IsOrderCompatible requires that configurations indistinguishable under the ordinary recognizer $R$ are comparatively equivalent under $R_{cmp}$, i.e., neither is greater than the other. Indistinguishable itself is the kernel equivalence of any recognizer: two configurations are related when they produce identical events. The module develops these notions to show how metric structure can emerge from purely comparative data.
proof idea
The proof is a term-mode reduction. After introducing the four configurations and the three hypotheses, it applies the compatibility assumption twice to obtain comparative equivalence statements. These supply the missing inequalities $c_1'≤c_1$ and $c_2≤c_2'$. The preorder transitivity hypothesis is then invoked twice to chain $c_1'≤c_1≤c_2≤c_2'$ into the desired $c_1'≤c_2'$.
why it matters
The lemma guarantees that the preorder induced by comparative recognition is well-defined on the quotient by indistinguishability, a prerequisite for extracting partial orders or metrics. It is invoked directly by the comparative_status summary of the RG7 development. In the Recognition Science framework it supports the emergence of order from qualitative comparisons, aligning with the physical fact that measurements such as balances and clocks are fundamentally comparative. It closes one step toward metric approximation without invoking the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.