notGreaterThan
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not impose reflexivity or transitivity on the relation.
- Does not determine the choice of greater-than events.
- Does not guarantee antisymmetry.
- Does not connect to any specific physical measurement.
formal statement (Lean)
64def notGreaterThan (R : ComparativeRecognizer C E) (gt_events : Set E) (c₁ c₂ : C) : Prop :=
proof body
Definition body.
65 R.compare (c₁, c₂) ∉ gt_events
66
67/-- The "equivalent" relation: neither is greater than the other -/