notGreaterThan
plain-language theorem explainer
notGreaterThan defines the induced non-strict order from a comparative recognizer by declaring c1 not greater than c2 exactly when the recognizer's comparison event for the pair falls outside the greater-than set. Recognition geometers cite this when building preorders and partial orders from qualitative comparisons in RG7. The definition is a direct membership test on the output of the compare function supplied by the recognizer.
Claim. Let $R$ be a comparative recognizer with comparison map $compare : C × C → E$. For a set $gt ⊆ E$ of greater-than events, $c_1 ≤ c_2$ holds if and only if $compare(c_1, c_2) ∉ gt$.
background
Recognition Geometry (RG7) begins with comparative recognizers that output qualitative events for pairs of configurations instead of presupposing distances. The ComparativeRecognizer structure supplies a compare function, an equality event, and the axiom that self-comparison yields the equality event. notGreaterThan extracts the ≤ relation by excluding the greater-than events from the recognizer's output. This construction appears in the module's treatment of induced preorders, where reflexivity and transitivity are imposed separately via InducesPreorder.
proof idea
One-line definition that applies the recognizer's compare function to the pair and checks non-membership in the greater-than event set.
why it matters
This definition supplies the le relation for the inducedPreorder and inducedPartialOrder constructions in the same module. It realizes the core step of Recognition Geometry by deriving order from comparative recognition events, consistent with the module's emphasis on metrics emerging from many such recognizers. It supports the framework's derivation of structure from qualitative comparisons without prior metrics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.