inducedPreorder
plain-language theorem explainer
inducedPreorder equips the configuration space C with a preorder whose relation c1 ≤ c2 holds precisely when the comparison event produced by recognizer R lies outside the designated greater-than set. Workers deriving order from qualitative detectors in recognition geometry cite this construction to obtain reflexivity and transitivity without presupposing a metric. The definition supplies the le field directly from notGreaterThan and discharges the two preorder axioms by invoking preorder_refl together with the transitivity clause inside the h:
Claim. Let $R$ be a comparative recognizer from pairs of configurations in $C$ to events in $E$, and let $gt_events$ be a subset of $E$. If $R$ satisfies the InducesPreorder conditions (its equal event lies outside $gt_events$ and the induced not-greater relation is transitive), then the binary relation on $C$ defined by $c_1 ≤ c_2$ whenever the event $R(c_1,c_2)$ is not in $gt_events$ is a preorder.
background
Recognition Geometry begins with comparative recognizers rather than metrics. A ComparativeRecognizer consists of a map sending each ordered pair of configurations to an event in $E$, together with a distinguished equal event that is returned on self-comparison. The auxiliary structure InducesPreorder records two further facts: the equal event is never classified as greater, and the relation “comparison event not in gt_events” is transitive. These two properties are exactly the data needed to turn the recognizer into a preorder on $C$. The surrounding module shows how such recognizers arise from physical comparisons (phase, mass, duration) and how metric structure is recovered later.
proof idea
The declaration is a structure definition that instantiates Preorder C. It sets the le field to the notGreaterThan predicate supplied by the recognizer and the event set. Reflexivity is obtained by a direct call to the sibling preorder_refl, which uses the eq_not_gt clause of h. Transitivity is obtained by applying the trans field of h to the three configurations.
why it matters
This definition supplies the RecognitionPreorder step inside the Recognition Geometry development. It shows that any comparative recognizer obeying the two InducesPreorder axioms yields a preorder without additional structure, thereby grounding the later passage to partial orders and metric approximations. The construction sits between the qualitative detector (ComparativeRecognizer) and the order-theoretic results (InducesPartialOrder, MetricApproximation) listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.