inducedPartialOrder
plain-language theorem explainer
A definition that turns a comparative recognizer satisfying antisymmetry into an explicit partial order on its domain of configurations. Workers on order emergence from qualitative comparisons cite the construction when moving from recognition to geometry. It assembles the order by designating the non-greater relation and confirming the three partial-order axioms from the given hypothesis and supporting preorder facts.
Claim. Suppose $R$ is a comparative recognizer from pairs of configurations in $C$ to events in $E$, and $S$ is a set of greater-than events. If $R$ induces a partial order relative to $S$, then the binary relation on $C$ that holds precisely when the comparison event of the pair lies outside $S$ constitutes a partial order on $C$.
background
Recognition Geometry treats comparative recognizers as primary: these structures map pairs of configurations to events that signal which is larger, with a fixed equal event returned on self-comparison. The module documentation emphasizes that physical measurements are often comparative, as in clocks comparing durations or scales comparing masses, and that absolute metrics arise later.
proof idea
The definition builds the PartialOrder record by assigning the le relation to the non-greater comparison derived from the recognizer. Reflexivity is obtained by invoking the preorder reflexivity lemma on the preorder extension of the hypothesis. Transitivity and antisymmetry are read off directly from the corresponding fields of the InducesPartialOrder hypothesis.
why it matters
This definition realizes the RecognitionPartialOrder step in the module, supplying the concrete partial order that later constructions use to approximate metrics from multiple comparative recognizers. It embodies the core insight that order structure can be extracted from qualitative recognition without presupposing distances. No open questions are directly closed here, but it removes a scaffolding layer for order-based geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.