comparative_status
plain-language theorem explainer
Comparative status assembles a fixed report string summarizing completion of comparative recognizer constructions in Recognition Geometry. A researcher deriving metric structure from qualitative pairwise comparisons would reference this summary when auditing RG7 results. The definition performs direct string concatenation of status lines for induced preorders, partial orders, equivalence relations, and metric compatibility.
Claim. The status report for comparative recognizers is the string formed by concatenating messages that the comparative recognizer is defined, that induced relations yield a preorder and a partial order, that comparative equivalence forms an equivalence relation, that order is compatible with standard recognizers, that order descends to the quotient, that separating families exist, that comparisons respect a metric, and that a pseudometric arises from recognition.
background
Recognition Geometry begins with comparative recognizers that output only qualitative relations such as ≤ or > between pairs of configurations, rather than absolute labels. From the module documentation, the core constructions are the comparative recognizer itself, the preorder induced when comparisons satisfy reflexivity and transitivity, the partial order obtained when antisymmetry also holds, and the metric approximation obtained from families of such recognizers. RecognitionDistance is the structure that packages a pseudometric derived from any such family, with the four axioms of non-negativity, zero self-distance, symmetry, and the triangle inequality.
proof idea
The definition builds the report by direct concatenation of eleven fixed status lines followed by a completion banner. No lemmas are applied; the body is a single expression that assembles the string literal and terminates with an #eval directive.
why it matters
This definition closes the comparative recognizers section (RG7) of the Recognition Geometry module. It records that order structure and pseudometrics can be extracted from purely comparative data, supporting the broader claim that geometry emerges from recognition rather than being presupposed. The module documentation notes that most physical measurements, such as phase comparisons in interference or mass comparisons on a balance, are fundamentally comparative, so the constructions here supply the formal bridge to derived metrics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.