InducesPreorder
plain-language theorem explainer
The structure defines when a comparative recognizer on configurations and events yields a preorder via the induced not-greater-than relation. It requires the recognizer's equal event to lie outside the greater-than set and the relation to be transitive. Researchers deriving order and metric approximations from qualitative comparisons in Recognition Geometry cite this result. The declaration is a bare structure definition that packages the two axioms with no additional proof steps.
Claim. A comparative recognizer $R$ on configurations $C$ and events $E$, together with a set $gt$ of greater-than events, induces a preorder when the equal event of $R$ is excluded from $gt$ and the relation $c_1$ not greater than $c_2$ (defined by the comparison event of $(c_1,c_2)$ lying outside $gt$) is transitive: for all $c_1,c_2,c_3$, if $c_1$ not greater than $c_2$ and $c_2$ not greater than $c_3$ then $c_1$ not greater than $c_3$.
background
Recognition Geometry starts from comparative recognizers that detect only qualitative pairwise relations rather than absolute distances. Such a recognizer consists of a comparison map from pairs of configurations to events together with a distinguished equal event returned on self-comparison. The module shows how preorder, partial-order, and eventually metric structure can be extracted from collections of these detectors, mirroring how physical instruments (balances, clocks, interferometers) operate by comparison alone.
proof idea
Structure definition that directly encodes the two preorder axioms: exclusion of the equal event from the greater-than set and transitivity of the induced not-greater-than relation. No lemmas or tactics are invoked; the declaration serves as the axiomatic package.
why it matters
The declaration supplies the preorder conditions used to construct the induced Preorder instance on configurations and to prove that comparative equivalence is an equivalence relation. It occupies the RG7 step of extracting order from comparative recognition, consistent with the framework's derivation of geometry from recognition rather than from an a-priori metric. Downstream results apply it to obtain reflexivity and transitivity of equivalence, to descend orders to quotients, and to define order-compatible recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.