orderedPairEvents
plain-language theorem explainer
Defines the finite set of ordered pairs of distinct points drawn from a finite planar point set A. Downstream distance-shell and diameter arguments cite it as the ambient event set whose images and filters yield spectra and multiplicities. The body is the Cartesian product of A with itself, filtered by inequality of coordinates.
Claim. For a finite set $A$ of points in the Euclidean plane $\mathbb{R}^2$, write $\mathrm{orderedPairEvents}(A)$ for the finite set of ordered pairs $(p,q)\in A\times A$ with $p\neq q$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean distance set; physically it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Points live in Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$ (via the bipartite distance-spectrum layer).
Ordered pairs are used for Lean bookkeeping. For any positive distance the ordered multiplicity is exactly twice the usual unordered multiplicity, so classical thresholds of the form $\le n$ become $\le 2n$. This definition supplies the raw non-diagonal pair universe on which spectra and shell filters act.
proof idea
Definitional, not a proof. Under classical choice one forms the Cartesian product $A\times A$ as a finset and retains only those pairs whose two components are unequal. No lemmas are applied beyond finset product and filter.
why it matters
This is the ambient event set for the whole distance-shell stack. Immediate consumers include the ordered distance spectrum (image of pairs under Euclidean distance), ordered shell multiplicity, and the ordered diameter-edge set (pairs at a fixed diameter value $\Delta$). Those feed diameter bounds from thrackle components, existence of a diameter shell for large enough cardinality, the inequality that every pairwise distance is at most the diameter, and the four-point crossing bridge to endpoint-disjoint local meetings. In the RS reading, each ordered pair is a two-body recognition event whose distance labels a recognition-energy shell; the definition therefore anchors the combinatorial side of the Erdős #132 physicalization without yet imposing sparsity or thrackle hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.