InducesPartialOrder
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not construct the PartialOrder instance; that occurs in inducedPartialOrder.
- Does not specify how gt_events are selected from physical observations.
- Does not guarantee existence of recognizers satisfying the antisymmetry condition.
- Does not address total orders or linear extensions.
formal statement (Lean)
103structure InducesPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
104 extends InducesPreorder R gt_events : Prop where
105 /-- Antisymmetry -/
106 antisymm : ∀ c₁ c₂, notGreaterThan R gt_events c₁ c₂ →
107 notGreaterThan R gt_events c₂ c₁ → c₁ = c₂
108
109/-- The induced partial order relation -/