comparativeEquiv
plain-language theorem explainer
The declaration defines the symmetric equivalence relation induced by any comparative recognizer: two configurations stand in this relation precisely when the recognizer reports neither as greater than the other. Workers on Recognition Geometry cite it when constructing the preorder and partial-order layers that precede metric emergence. The definition is a direct conjunction of the two directed not-greater-than predicates.
Claim. Let $R$ be a comparative recognizer that assigns to each ordered pair of configurations an event in $E$, and let $gt_events$ be the subset of events interpreted as strict greater-than. For configurations $c_1$ and $c_2$, write $c_1$ equivalent to $c_2$ when $R$ does not place $c_1$ in $gt_events$ relative to $c_2$ and does not place $c_2$ in $gt_events$ relative to $c_1$.
background
Recognition Geometry begins with comparative recognizers instead of metrics. A comparative recognizer is a map from ordered pairs of configurations to events together with a distinguished equal event that is returned on every self-comparison. The module shows how the qualitative output of such a map can be turned into order-theoretic structure. The present definition isolates the symmetric fragment of the induced comparison relation. Upstream results supply the active-edge count $A$ and the edge-count function $E(D)$ that later calibrate the numerical scale once the order is in place.
proof idea
The declaration is a one-line definition that conjoins the two directed not-greater-than conditions supplied by the sibling predicate notGreaterThan. No lemmas are invoked; the conjunction is the entire content.
why it matters
This definition supplies the equivalence relation that the three theorems comparativeEquiv_refl, comparativeEquiv_symm and comparativeEquiv_trans turn into an equivalence. It therefore sits at the base of the RecognitionPreorder and RecognitionPartialOrder constructions listed in the module documentation. In the larger Recognition Science chain it marks the transition from qualitative recognition events to the preorder that later yields the J-cost function and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.