comparativeEquiv_trans
plain-language theorem explainer
Transitivity of comparative equivalence follows directly from the preorder transitivity axiom supplied by InducesPreorder. Researchers deriving order structures from qualitative recognizers would cite this when chaining pairwise comparisons into an equivalence relation. The proof is a one-line term that applies the transitivity operation twice, once forward and once in the swapped direction.
Claim. Let $R$ be a comparative recognizer on configurations $C$ with events $E$, and let $G$ be the set of greater-than events. If $R$ induces a preorder with respect to $G$, and if $c_1$ is comparatively equivalent to $c_2$ while $c_2$ is comparatively equivalent to $c_3$, then $c_1$ is comparatively equivalent to $c_3$.
background
A comparative recognizer consists of a map sending pairs of configurations to events together with a distinguished equality event that is returned on self-comparison. InducesPreorder packages two conditions: the equality event lies outside the greater-than set, and the not-greater-than relation is transitive. Comparative equivalence is the symmetric closure of not-greater-than, i.e., the conjunction of both directions.
proof idea
The proof is a one-line term that constructs the required pair by invoking the transitivity field of the InducesPreorder hypothesis twice: once to obtain not-greater-than from $c_1$ to $c_3$ and once after swapping the arguments to obtain the reverse direction.
why it matters
The result verifies that comparative equivalence is transitive and therefore an equivalence relation, supplying the missing step for the induced partial order constructed later in the same module. It advances the Recognition Geometry program of extracting preorder and partial-order structure from comparative recognizers before metric approximation is addressed. The declaration aligns with the module's goal of showing that qualitative comparison relations are primary and that metric-like structure emerges from them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.