preorder_refl
plain-language theorem explainer
Reflexivity of the induced not-greater-than relation follows immediately once a comparative recognizer is assumed to induce a preorder. Order theorists and physicists modeling comparative measurements cite this when deriving preorders from qualitative detectors. The proof reduces directly to the self-comparison axiom and the eq_not_gt clause of the induction hypothesis.
Claim. Let $R$ be a comparative recognizer on configurations $C$ with events $E$, and let $S$ be the set of greater-than events. If $R$ induces a preorder on $S$, then for every configuration $c$, the comparison of $c$ with itself lies outside $S$.
background
Recognition Geometry starts from comparative recognizers rather than metrics. A ComparativeRecognizer supplies a compare map from pairs of configurations to events together with a distinguished equal event that self-comparison must return. The notGreaterThan predicate then declares $c_1$ not greater than $c_2$ precisely when their comparison event lies outside the chosen greater-than set $S$ of events.
proof idea
The proof is a short term-mode reduction. It unfolds notGreaterThan, rewrites the self-comparison via the recognizer's compare_self axiom to obtain the equal event, and closes with the eq_not_gt field of the InducesPreorder hypothesis.
why it matters
This supplies the reflexivity axiom for inducedPreorder and inducedPartialOrder, and is used by comparativeEquiv_refl. It realizes the first concrete step of RG7: preorder structure on configuration space emerges from any comparative recognizer satisfying the induction conditions, without presupposing distances. The module frames the result as the starting point for extracting metric approximations from families of such recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.