IsOrderCompatible
plain-language theorem explainer
IsOrderCompatible defines compatibility between a recognizer R and a comparative recognizer R_cmp: indistinguishability under R must imply comparative equivalence under R_cmp. Researchers building Recognition Geometry (RG7) cite it when proving that qualitative comparisons induce orders that descend to quotients. The definition is a direct universal quantification linking the two relations with no auxiliary lemmas.
Claim. Let $R$ be a recognizer on configurations $C$ and events $E$, and let $R_{cmp}$ be a comparative recognizer on $C$ and events $E'$. Let $gt$ be a set of greater-than events such that $R_{cmp}$ induces a preorder on $gt$. Then $R$ is order-compatible with $R_{cmp}$ when, for all configurations $c_1,c_2$, if $c_1$ and $c_2$ are indistinguishable under $R$ then $c_1$ and $c_2$ are comparatively equivalent under $R_{cmp}$ with respect to $gt$.
background
Recognition Geometry starts from comparative recognizers that output only qualitative relations between pairs of configurations rather than absolute labels. A ComparativeRecognizer consists of a compare map from $C×C$ to events together with a distinguished equality event that is returned on self-comparison. InducesPreorder adds the requirements that the equality event lies outside the greater-than set and that the induced not-greater-than relation is transitive, thereby producing a preorder on configurations.
proof idea
The declaration is a definition whose body is exactly the stated universal quantification. No tactics or upstream lemmas are invoked; the body directly encodes the compatibility condition given in the doc-comment.
why it matters
The definition is invoked by the theorem order_descends_to_quotient, which establishes that order relations descend to the quotient when compatibility holds. It supplies the RG7 bridge from comparative recognition to preorder structure, consistent with the module's emphasis on deriving metric-like geometry from qualitative comparisons such as phase interference or mass balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.