comparativeEquiv_refl
plain-language theorem explainer
Comparative equivalence is reflexive for any recognizer that induces a preorder. Researchers deriving order and metric structure from qualitative comparisons cite the result when verifying that the induced relation meets the reflexive axiom of an equivalence. The proof is a direct term that applies the preorder reflexivity lemma to both directions of the equivalence definition.
Claim. Let $R$ be a comparative recognizer on configuration space $C$ with event space $E$, and let $gt_events$ be the set of greater-than events. If $R$ induces a preorder with respect to $gt_events$, then for every configuration $c$ the comparative equivalence relation holds between $c$ and itself.
background
A comparative recognizer is a structure that supplies a comparison function from pairs of configurations to events together with a distinguished equal event returned on self-comparison. The predicate InducesPreorder requires that this equal event lies outside the greater-than set and that the induced not-greater-than relation is transitive. Comparative equivalence between two configurations holds precisely when neither is greater than the other under the recognizer.
proof idea
The proof is a one-line term that constructs the required pair by applying the preorder reflexivity lemma twice, once for each direction of the equivalence definition.
why it matters
The declaration supplies the reflexive leg of the statement that comparative equivalence is an equivalence relation. It is invoked by the sibling theorems that establish symmetry and transitivity, completing the equivalence structure announced in the module documentation. Within Recognition Geometry this reflexive base supports the later extraction of partial orders and metric approximations from purely comparative data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.