comparativeEquiv_symm
plain-language theorem explainer
Symmetry of the comparative equivalence relation follows immediately from its definition as mutual non-greater-than. Researchers constructing order structures from qualitative recognizers cite this when verifying that the induced relation is an equivalence. The proof is a one-line term that swaps the two conjuncts of the hypothesis.
Claim. Let $R$ be a comparative recognizer on configurations $C$ with event type $E$, and let $Ssubseteq E$ be the set of greater-than events. If neither $c_1$ is greater than $c_2$ nor $c_2$ is greater than $c_1$ under $R$ and $S$, then the same holds with $c_1$ and $c_2$ interchanged.
background
Recognition Geometry starts from comparative recognizers that detect only pairwise relations such as greater-than or equal, rather than absolute values. The structure ComparativeRecognizer supplies a compare map from pairs of configurations to events together with a distinguished equal event that appears on self-comparison. The relation comparativeEquiv is then the conjunction of notGreaterThan in both directions, encoding that neither configuration is superior to the other. This construction appears inside the module's development of RecognitionPreorder and RecognitionPartialOrder, which extract preorder and partial-order structure from such recognizers. The upstream definition of the event cardinality E counts the edges of a D-dimensional cube, supplying the discrete event space in which the comparisons take place.
proof idea
The proof is the term that constructs the target conjunction by swapping the two notGreaterThan components already present in the hypothesis. No additional lemmas are invoked; the step relies only on the definition of comparativeEquiv as a symmetric conjunction.
why it matters
The lemma supplies the symmetry axiom required to show that comparativeEquiv forms an equivalence relation, completing the trio with the reflexivity and transitivity results in the same module. It thereby advances the module's central claim that metric-like structure emerges from purely comparative data, as illustrated by the physical examples of phase comparison in interference and mass comparison on a balance. The result sits downstream of the ComparativeRecognizer structure and feeds the preorder extraction theorems that follow in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.