diameter_ordered_edge_data
plain-language theorem explainer
Membership in the ordered diameter-edge set unpacks to four facts: both endpoints lie in the finite planar set A, they are distinct, and their Euclidean distance equals the shell value Δ. Diameter-shell and Conway-thrackle arguments cite this as the basic edge certificate. The proof is pure Finset filter and product elimination, no geometry.
Claim. Let $A$ be a finite set of points in the plane and $\Delta \in \mathbb{R}$. If an ordered pair $e=(p,q)$ belongs to the ordered diameter edges of $A$ at distance $\Delta$, then $p \in A$, $q \in A$, $p \neq q$, and $\mathrm{dist}(p,q)=\Delta$.
background
The module Distance Shell Multiplicity records the Recognition Science reading of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. The development works with ordered pairs for Lean simplicity: for positive distance, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Points are the planar type Point2 imported from the bipartite distance spectrum. An ordered diameter edge is an ordered pair drawn from $A \times A$, filtered to be off-diagonal and to realize distance exactly $\Delta$, and further restricted so that $\Delta$ is a diameter shell of $A$ (every pairwise distance is at most $\Delta$). This lemma is the elementary membership unpacker for that filtered product set.
proof idea
Term-mode classical proof by nested membership elimination. Apply Finset.mem_filter.mp to the hypothesis to split the outer filter into the inner event membership and the equality dist e.1 e.2 = Δ. Apply mem_filter.mp again to recover product membership plus the off-diagonal inequality. Finally Finset.mem_product.mp yields the two endpoint memberships. Package the four conjuncts with a single constructor. No metric or combinatorial lemma is invoked beyond Finset API.
why it matters
This is the local edge certificate used throughout the diameter-shell development. Downstream, diameter_ordered_edges_cross_distances_le bundles the four cross-distances between two ordered diameter edges and re-asserts both edge lengths equal Δ; the present lemma supplies the endpoint and length facts for each edge. The same unpacking feeds diameter_conway_bound_from_support_conway, which lifts a support-level Conway thrackle bound to a diameter-specific ordered multiplicity bound, and endpoint_disjoint_two_point_intersection_forces_collinear, the affine incidence certificate that two endpoint-disjoint diameter representatives sharing two points must be collinear.
In the RS framing these diameter edges are the extremal two-body recognition shells; controlling their ordered multiplicity is the discrete step toward the Erdős #132 physicalization. The lemma itself is pure bookkeeping, but every geometric bound on the diameter shell begins here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.