InducesPartialOrder
plain-language theorem explainer
InducesPartialOrder specifies the antisymmetry condition that turns a preorder induced by a comparative recognizer into a partial order on configurations. Researchers deriving order and metrics from qualitative pairwise comparisons cite this when moving from recognition events to structured relations. The structure directly extends InducesPreorder by adding the requirement that mutual non-greater relations force equality.
Claim. Let $R$ be a comparative recognizer on configurations $C$ with events $E$, and let $gt_events$ be a subset of $E$. Then $R$ induces a partial order if it induces a preorder (equal event not in $gt_events$, and not-greater relation transitive) and satisfies antisymmetry: for all $c_1, c_2$, if $c_1$ is not greater than $c_2$ and $c_2$ is not greater than $c_1$, then $c_1 = c_2$.
background
Recognition Geometry starts from comparative recognizers that detect only qualitative relations between pairs of configurations, without presupposing distances. A ComparativeRecognizer supplies a compare map from $C times C$ to $E$, a distinguished eq_event for self-comparisons, and the axiom that compare(c,c) equals eq_event. The auxiliary notGreaterThan predicate holds precisely when the comparison event lies outside the chosen gt_events set. InducesPreorder packages reflexivity of notGreaterThan (via eq_not_gt) together with transitivity of that relation. The module treats these induced relations as the primary objects from which metric approximations later emerge, consistent with physical examples such as phase comparisons or balance-scale readings.
proof idea
This is a structure definition that extends InducesPreorder by adjoining a single antisymmetry field on the notGreaterThan relation. No lemmas or tactics are applied; the declaration simply records the preorder data plus the antisymmetry axiom.
why it matters
The definition supplies the final axiom needed to obtain a partial order from comparative data, which inducedPartialOrder then packages into an explicit PartialOrder instance on C. It advances the RG7 program of extracting order structure directly from recognizers, supporting later steps toward metric emergence. The comparative_status summary lists it among the core results of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.