IsOrderCompatible
A definition establishing order compatibility between a standard recognizer R and a comparative recognizer R_cmp: any pair indistinguishable under R must be comparatively equivalent under R_cmp. Researchers deriving order structure in Recognition Geometry (RG7) cite it when proving descent to quotients. The definition consists of a direct universal quantification linking the indistinguishability predicate to the comparative equivalence predicate.
claimLet $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 and let $hp$ be the hypothesis that $R_{cmp}$ induces a preorder on $gt$. Then $R$ is order-compatible with $R_{cmp}$ if, for all configurations $c_1,c_2$, whenever $c_1$ and $c_2$ are indistinguishable under $R$ they are comparatively equivalent under $R_{cmp}$ with respect to $gt$.
background
Recognition Geometry begins with comparative recognizers that map pairs of configurations to comparison events, including a distinguished equality event for self-comparisons. The InducesPreorder structure requires that this equality event lies outside the greater-than set and that the induced not-greater-than relation is transitive. A standard recognizer supplies an indistinguishability relation on configurations; the module treats comparative detection as primary, with metric-like structure (including preorders) emerging from it, as occurs in physical comparisons such as balance scales or phase interference.
proof idea
This is a definition whose body is the single universal statement that indistinguishability under R implies comparative equivalence under R_cmp. It functions as a one-line wrapper that directly encodes the compatibility condition using the predicates Indistinguishable and comparativeEquiv.
why it matters in Recognition Science
The definition is invoked by the theorem order_descends_to_quotient, which establishes that order descends to the quotient once compatibility holds. It supplies the RG7 link between standard and comparative recognizers, supporting the framework claim that absolute metrics are derived from qualitative comparative relations. No open scaffolding is closed here; the definition simply records the required preservation property.
scope and limits
- Does not assert existence of any recognizer satisfying the compatibility condition.
- Does not construct or prove properties of the comparative equivalence relation.
- Does not address antisymmetry or passage to partial orders.
- Does not derive metric approximations or numerical distances.
formal statement (Lean)
141def IsOrderCompatible (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
142 (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events) : Prop :=
proof body
Definition body.
143 ∀ c₁ c₂, Indistinguishable R c₁ c₂ → comparativeEquiv R_cmp gt_events c₁ c₂
144
145/-- If R is order-compatible, the order descends to the quotient -/