InducesPartialOrder
plain-language theorem explainer
A comparative recognizer induces a partial order on configurations precisely when the preorder it generates is antisymmetric under the not-greater-than relation. Workers extracting order from qualitative comparisons cite the definition when moving from preorders to partial orders. The declaration is realized as a structure that extends the preorder axioms by a single antisymmetry clause.
Claim. Let $R$ be a comparative recognizer mapping pairs of configurations in $C$ to events in $E$, and let $gt_events$ be a subset of $E$. Then $R$ induces a partial order if the induced not-greater-than relation is reflexive and transitive (the preorder condition) and satisfies antisymmetry: $c_1$ not greater than $c_2$ together with $c_2$ not greater than $c_1$ forces $c_1=c_2$.
background
Recognition Geometry begins with comparative recognizers that output only qualitative relations between pairs of configurations rather than absolute labels. A comparative recognizer consists of a comparison map from $C×C$ to events $E$ together with a distinguished equal event that is returned on self-comparison. The not-greater-than relation is defined by declaring $c_1$ not greater than $c_2$ precisely when the comparison event lies outside the chosen set of greater-than events. InducesPreorder packages the two axioms that turn this relation into a preorder: the equal event is never greater, and the relation is transitive.
proof idea
The declaration is a structure definition. It inherits the two fields of InducesPreorder (eq_not_gt and trans) and adds a single new field, antisymm, whose statement is exactly the antisymmetry condition on the not-greater-than relation.
why it matters
The structure supplies the hypothesis required by inducedPartialOrder, which constructs an instance of PartialOrder on the configuration type. It thereby completes the RecognitionPartialOrder step listed in the module documentation, showing how antisymmetric comparative relations produce partial orders. This step sits between the preorder construction and the later metric-approximation results that derive distances from families of such recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.