SeparatesPoints
plain-language theorem explainer
A family of comparative recognizers separates points when every pair of distinct configurations is distinguished by at least one member of the family. Arguments deriving metrics from qualitative comparisons cite this property to ensure the resulting distance is non-degenerate. The definition encodes the condition directly as a universal quantification over configuration pairs with an existential witness for separation.
Claim. A family of comparative recognizers $(R_i)_{i∈I}$, each paired with a set of distinguishing events $G_i$, separates points when for all distinct configurations $c_1,c_2$ there exists an index $i$ such that $R_i$ distinguishes $c_1$ from $c_2$ via an event in $G_i$.
background
Recognition Geometry starts from comparative recognizers instead of presupposed metrics. Each recognizer maps a pair of configurations to a comparison event, with a fixed equality event returned on self-comparison, and thereby induces relations such as preorder or partial order on the configuration space. The module shows how collections of such recognizers can recover metric-like structure. Upstream results supply the concrete types for configurations and events, including the active-edge count per tick and the spectral edge count of the D-cube that fix the physical setting for C and E.
proof idea
The definition is the direct statement of the separation predicate. It consists of a single universal quantifier over distinct pairs together with an existential quantifier over the family index, with no auxiliary lemmas or reductions required.
why it matters
The definition supplies the separation hypothesis in the theorem metric_from_comparisons, which concludes that a compatible family yields a genuine metric. It occupies the RG7 slot in which metric structure is shown to emerge from comparative data alone, consistent with the framework's derivation of D=3 and the phi-ladder from the forcing chain. It closes the gap between qualitative recognition events and quantitative distances used in later mass and spectral constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.