mem_unorderedEdgeSupport_iff
plain-language theorem explainer
An unordered pair of planar points lies in the unordered edge support of a finite ordered edge set exactly when some ordered pair from that set maps to it. Anyone selecting support representatives or comparing ordered and unordered edge data cites this. The proof is a one-line classical simplification of the support definition.
Claim. Let $E$ be a finite set of ordered pairs of points in $\mathbb{R}^2$, and let $u$ be an unordered pair of such points. Then $u$ belongs to the unordered edge support of $E$ if and only if there exists $e\in E$ whose associated unordered pair equals $u$.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances, ordered multiplicity is twice the classical unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Points are planar Euclidean points (Point2 as $\mathbb{R}^2$). An ordered edge set $E$ is a finite set of ordered pairs. The unordered edge support collects the distinct unordered pairs (symmetric products) realized by members of $E$, via the map that forgets order on each ordered pair. This lemma is the membership characterization of that support set.
proof idea
Classical reasoning is opened, then simp unfolds the definition of the unordered edge support. The biconditional is definitional: membership means the image of the ordered-to-unordered map on $E$ contains $u$, which is exactly existence of an ordered representative in $E$.
why it matters
This is the workhorse membership rewrite for the unordered support layer. Downstream, the chosen ordered representative of a support edge is obtained by classical choice on the forward direction; membership and unordered-class correctness of that choice are immediate from the choice specification. The same rewrite feeds the diameter-support simple-representative certificate (lifting ordered meeting data to support edges), equality of unordered support under the chosen ordered support, and the Conway-thrackle missing-edge argument for geometrically disjoint segments. In the RS reading of Erdős #132, it keeps ordered bookkeeping interchangeable with unordered shell geometry without changing occupancy counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.